CSCI 0190 · Fall 2026
Z3-Peat
1 What is This Assignment’s Purpose?
Three earlier assignments this semester were actually the same kind of problem: take a task, think of it in terms of some constraints, and solve them. LabAssign was very obviously that: you searched for a seating that respected availability and capacity, and we saw how to do it much more concisely and better using a constraint-solver. Requirements 1 was about searching for a way to match courses to requirements. Perhaps less obviously, MST was also that: given the constraints of minimum and spanning, find the lightest tree.
Each problem had its own, bespoke solution, sometimes one far less good than a solver could produce. In this assignment you’ll redo all three tasks with one unifying framework, the Z3 solver. You’ll integrate or compare the new solutions to the old ones, and thereby learn about tradeoffs in using solvers.
2 Theme Song
Oops!...I Did It Again by Britney Spears
3 Setup
You will use Z3 from Pyret through the pyret-z3 library. You must be online when you run, because the library downloads the solver the first time. If you are programming manually, you will likely want to use VSC; if you’re having Claude generate code, it will use the command-line interface (CLI): see Software.
4 Assignment
For all three -peat’ed parts below, the contracts are unchanged from the original assignments. What changes is primarily how you compute the answer. You are welcome to reuse anything and everything from your earlier submissions: graph generators, parsers, tests, and so on, so you can focus on the computation method. Of course, this is also a chance to strengthen any weaknesses in those submissions.
4.1 Manual Constraint Writing
Pick out a set of “simultaneous equations” or “system of equations”, of the kind you saw in school or the SAT. Work out the solution(s) by hand. Hand-write it in the constraint language. Run it, and confirm that the answer matches what you expected.
Pick out a logic puzzle to encode using Booleans. If you’re lost for one, think about a Sudoku board or, more specifically, a Latin square. Whatever you choose, hand-write it in the constraint language, run it, and confirm that the answer matches what you expected.
What follows is for the Latin square example:
You can think of each cell as having one Boolean for each possible value in the board, and then you constrain these to have the right relationships within a cell and across the cells.
Since this can get overwhelming, you could just do it for a 2x2 board to confirm your understanding.In the very special case of a 2x2 board, you don’t need two separate Boolean variables for each cell; one does the trick, precisely because there are only two possible values. But that doesn’t generalize, whereas having one per value does.
If you feel ambitious, think of how to generalize this for arbitrary NxN boards. But don’t get bogged down in this part, there’s more to do below!
4.2 LabAssign
Reimplement assign from LabAssign using Z3, under the same assumptions as before. The hard constraints are the ones you already know: every student sits in exactly one lab, nobody sits in a lab they are unavailable for, and no lab exceeds its capacity.
Then revisit your original analysis. You might have had, or can reimagine, different notions of goodness and fairness. This time, don’t just discuss them, but instead experiment with them. Come up with at least two different notions, have the solver implement each (or understand why it can’t be implemented), and compare. Summarize, with small examples, the differences between the two. (You may have multiple assigns to reflect this; make sure you give them different names, like assign-…, to reflect the different meanings.)
4.3 MST
Create a new implementation, mst-z3, which consumes a well-formed graph (in the sense of MST) and returns a minimum spanning tree of it, computed by Z3. This is neither Prim’s nor Kruskal’s algorithm; it is a statement of what a minimum spanning tree is, handed to the solver.
Just like in the lab assignment, we can think of a Boolean for each edge representing whether it’s in or out of the solution. The objective minimizes the weight of the chosen edges. The tricky part is saying “the chosen edges form a spanning tree” without ever saying “no cycles”, which is not a condition the solver can check edge by edge.Hint: think about how you would convince a skeptic that a set of edges is a tree without enumerating cycles. Pick a root. Every other vertex has exactly one chosen edge that is its “parent” edge. And every parent is strictly closer to the root than its child, for some notion of “closer” that you make the solver assign. Think about this carefully; it is the heart of this part.
Having built mst-z3, use it. In MST your sort-o-cle was a “sorta”-cle because it could not confirm minimality. Add mst-z3 to your testing of mst-prim and mst-kruskal to check whether they indeed produced minimal solutions. If not, fix them so that they do. Finally, time all three implementations on the same graphs, using your generate-input to make graphs of growing size, and keep going until something becomes uncomfortably slow (or the solver gives up).
4.4 Requirements
Reimplement check-reqs from Requirements 1 using Z3. You are welcome to use everything you learned from peer-review and Requirements 2.
Think of the requirements as a set of slots to be filled, and of each course on the roster as something that can fill at most one slot. The solver’s job is to decide whether the slots can be filled, and by what. Some things remain your job: detecting malformed input is a matter of parsing, not of solving, and deciding between all-necessary and has-unnecessary may take more than one query of the solver.
Use your most up-to-date tests from Requirements 2. Run that same tests.arr against your new implementation. Every disagreement is interesting: it is a bug in the old implementation, a bug in the new one, or a test that encoded a misreading of the requirements. Say which, for each.
5 Analysis
In addition to your code, write a short analysis (PDF) with the following parts. Keep it brief; a page or two in total is plenty.
Tell us the simultaneous equations and logic puzzle problems that you successfully encoded by hand.
LabAssign. State the notions that you defined, and summarize how they disagree. If you were unable to encode one of them in Z3, explain why not.
MST. Explain your encoding of “spanning tree” in a few sentences. Then explain what mst-z3 adds to your testing of Prim and Kruskal, and what it still might not check; say whether it actually caught a bug in either. Finally, report your timings as a small table: for each graph, its number of vertices and edges, and the time taken by each of the three implementations. Also provide a plot. Explain what you see.
Requirements. List the disagreements between your old and new check-reqs on your tests.arr, and for each say where the fault lies. If there were none, say so.
Overall. For each of the three problems, which was easier to write, the solver version or the original, and why? Where did the work go: did the solver remove it, or did it move it (into the encoding, into reading the model back out, into something else)? Did the solver ever surprise you, by being slow, by returning unknown, or by finding a solution you did not expect?
6 Built-Ins
In addition to the allowed functions in the general guidelines, you may use everything in the pyret-z3 library, plus whatever each original assignment permitted (for instance, immutable string dictionaries in the MST part).
7 AI
You are welcome to use Claude Code for this assignment. Indeed, you may find it daunting to do it by hand, whereas with Claude you can do the various experiments above relatively easily. But don’t just hand off the task to Claude; you will need to write up an analysis (in your own words!), and to do that, you need to know what happened.
One specific caution. The encodings are the whole point of this assignment, and the MST encoding in particular is the kind of thing an AI will happily produce automatically. If you let it do that, you will have learned nothing, and the analysis questions will be hard to answer. Try to first think about how to solve it. Discuss your proposal with Claude. Have it critique your proposal. Iteratively refine your suggestion until Claude thinks it sounds good. Only then have it code, and then see whether your design was indeed good.
If you use Claude, point it at the Pyret Z3 library’s documentation. It describes everything the library provides, and several pitfalls of using it that whoever or whatever writes the code needs to know.
8 Starter
Follow the instructions given for the Pyret Z3 library on GitHub (opens in a new tab). You can also refer to the previous assignments for their starter information.
9 Submission
labassign.arr, defining assign.
mst.arr, defining mst-z3.
check-reqs.arr and tests.arr, as in Requirements 1; as before, do not upload reqs-common.arr.
Your analysis, as a PDF, with a clear indication of where your answer to each part begins and ends.