Coding Assignment 3: SMT

Due: Friday, May 8 at 5:00 PM | 150 points

Coding Assignment 3 is structured as a menu of options. Choose any combination of options whose point values sum to at least 120 points, and complete those plus the short reflection at the end. If your choice of options exceeds 120 points, the autograder will grade them in the listed order, and will stop grading after reaching 120 or more total possible points. For example, you get full credit by earning 30/60 on #2 and 90/90 on #5a, but not by earning 30 points each on 4 different questions. Details for each option will be embedded in starter code in the course repo.

Pick at most one of Options 5a and 5b. The two problems are similar.

Reflection (30 points): Complete a short reflection (~100–200 words total) answering the following questions. You don't need to answer all of them, just pick a few that feel relevant. For this part only, apply the same course AI policy as for reading reflections, not the course AI policy for code. * Why did you choose to complete the options that you did? Do they hold any particular significance to you, or is there any reason you found them particularly interesting? * This week's homework focused primarily on puzzles - next week will focus more on program verification, which will be a key application. Still, did you learn any skills in this homework that you think may be useful for you in the future? * Did you enjoy this homework assignment? If so, what broader lessons did you take away from it, besides learning to solve these specific problems? If not, what kinds of problems would more useful to you?

You will submit the following to Gradescope:

• One Python file per option you chose, containing all of your source code for that option. The expected filename is fixed per option (see the starter code). Do not use Python packages except Z3 and other built-in packages. Do not import more things from Z3 that are not already imported for you. Do not submit additional code files.
• If you select Problem 5b, also include a PDF containing the requested chart.
• A Markdown (.md) or text (.txt) file containing your reflection response.

The autograder will automatically grade Options 1–5a and the correctness/timing portion of Option 5b. The chart PDF for Option 5b is reviewed manually. The autograder will run your code on a larger number of tests compared to what we have provided you in the starter code, and you will be able to immediately see the results. You may resubmit as many times as you like while submissions are open.

Reminder: The full course collaboration and AI policy may be found in the syllabus. To summarize: You may discuss problems at a high level with classmates, but do not share solutions, code, or detailed derivations with other students. You may use AI tools (Copilot, ChatGPT, Claude, etc.) as part of your workflow, but you must include a short attribution note in your submission listing which tools you used and how.

Problem 1: Magic square solver

A magic square of order $N$ is an $N \times N$ grid filled with the integers $1, 2, \ldots, N^2$, each used exactly once, such that every row, every column, and both main diagonals sum to the same constant. That constant is $N(N^2+1)/2$: all the integers together are $N^2(N^2+1)/2$, so each of the $N$ rows must be $N(N^2+1)/2$.

A sample Z3 program that finds a magic square of size $N$ is given to you in the starter code. However, it is too slow, timing out for all $N > 4$ (on most machines). The sample program uses the first encoding that you might think of: representing each cell with a Int variable and asserting distinctness with the built-in Distinct predicate.

Your task is to rewrite this program so that at least all $N \le 8$ works within about 10 seconds. There are a few things to change:

• Instead of integers, try using bit vectors! This allows the solver to desugar the program into a pure SAT query, which is faster than integer reasoning. Also, our integers are all relatively small: how large do bit vectors need to be in order to fit the necessary calculations without overflowing?
• Z3 treats the Distinct predicate at a high level and tries to reason with it directly. For this problem, you might also want to try replacing it with a lower-level custom implementation of distinctness.
• Please use the custom BitBlastSolver provided rather than the default Solver. The only difference is that we're telling Z3 to eagerly bit-blast your bit vectors into pure SAT queries before solving, instead of doing its default preprocessing which is making it slow.

Problem 2: Sliding puzzle solver

The sliding puzzle is played on an $N \times N$ grid containing tiles $1, 2, \ldots, N^2 - 1$ and one empty cell, called the blank. A move slides any tile that shares an edge with the blank into the blank's position; equivalently, the blank swaps places with one of its (up to four) neighbors. Starting from a given configuration of tiles, you want to reach a given target configuration by a sequence of such moves.

You will be given a starting configuration start, a target configuration goal, and a step count $K$. Your task is to decide whether goal is reachable from start in exactly $K$ moves, and if so, to return a witness — for example, the sequence of blank positions produced by the moves. If no such sequence exists, return None.

Hint: Consider representing a board state as a Z3 Array from cell index to tile, where each move involves Store/Select at a symbolic index.

Problem 3: Family-tree puzzle

In a family-tree puzzle, you are given a partial description of a small family — some people, some parent-child relationships, and a few facts about their ages — and asked to determine whether the description is consistent and, if so, to fill in the missing details.

Concretely, each puzzle instance specifies:

• A finite collection of named people (e.g. Alice, Bob, Carol, ...).
• A list of age facts: assertions such as "Alice is 8 years old," "Bob is older than Eve," or "Dave is at most 60."
• A list of parent facts: either of type "Alice's parent is Bob" or "Carol and Dave share the same parent." Note that in "Carol and Dave share the same parent," the name of the parent is unspecified, but must be one of the people in the finite domain.

In addition, every puzzle is governed by a generation gap rule: a parent must be at least 16 years older than their child. This rule applies automatically to every parent-child pair the puzzle declares.

Your task is to decide whether some assignment of ages (and of any parent relationships not explicitly named) is consistent with all of these constraints. If so, return a valid assignment of ages for everyone in the puzzle. If not — for example, because a chain of parent inferences would force someone to be older than themselves — return None.

Hint: Consider using EUF to encode the parent and age functions.

Problem 4: Cutting plywood

Suppose you have a single piece of plywood of length $W$ and height $H$, and a customer requests that you cut out a list of rectangular pieces of various real-valued sizes $(w_i, h_i)$. Because the wood has a specific grain direction, rotations of the pieces are not allowed. Your job is to determine if it is possible to cut out all the pieces. If so, return the bottom-left coordinates of each rectangle. If no packing exists, return None.

Hint: Certainly you'll want to use SMT with LRA. The key challenge is encoding that the rectangular pieces are occupying disjoint regions of the plywood. How can you encode this within the syntax of SMT with LRA?

Problem 5: Thinking about SMT with LIA

In class, we discussed the DPLL(T) algorithm and how that allows us to combine SAT with other theories. Theoretically though, both LIA and SMT with LIA are NP-complete, just like SAT. In other words, if a problem has a polynomial size encoding in SMT with LIA, it also has a polynomial size encoding in LIA itself, and also in SAT itself!

The following options for this problem think through how this works.

Option A: Reducing to LIA

In a Boolean CNF formula (conjunctive normal form, the input to SAT), recall that the entire formula is an AND of ORs of literals. For example, $(x \lor \lnot y) \land (y \lor z)$. Just like how Boolean expressions of any shape can be rewritten into a Boolean CNF, assume that the same as been already done for SMT with LIA.

Specifically, the input is a CNF, but instead of literals, we have linear inequalities. For example, $([x + y \le 3] \lor [y - 2z \le -1]) \land [z \le 5]$. Note that you can assume that there is no negation and no $=, \neq, \ge, <, >$. (You can get rid of $\ge$ by multiplying both sides by $-1$, etc.)

Your goal is to write a pure LIA query (just an AND of linear inequalities, no ORs) that is satisfiable if and only if the original LIA query is satisfiable.

Hint 1: You might want to introduce auxiliary variables, kind of like a Tseitin encoding. Create one variable for each original inequality, and write equations constraining it to be 1 when the inequality is satisfied and 0 when the inequality is not satisfied. Then, rewrite each clause as an equation using your new variables.

Hint 2: You may want to use the following fact: Suppose a system of $m$ linear inequalities in $n$ variables has a solution, and suppose all coefficients and constants are at most $k$ in absolute value. Then in particular, there is a solution $(x_1, \dots, x_n)$ where each $|x_i| \le n(mk)^{2m+1}$.

Option B: N-queens with regions, reprise

You do not need to have completed the N-queens option on the previous homework to complete this option.

In the previous homework, you solved the N-queens with regions puzzle using SAT solving. See the previous assignment for details on how the problem works.

In this problem, you will re-solve the same problem using SMT and pure LIA. Arguably, SMT is a more natural encoding of this problem - allowing encoding of diagonal constraints as a mathematical relation rather than a hard-coded set of squares. For a pure LIA encoding, you might find Hint 1 for the previous option useful for you, though you shouldn't need to use Hint 2. (You certainly could use it, but the situation is greatly simplified by using the actual equations that you need, instead of assuming some general unknown equations.)

A SAT-based solution, like what you were asked to do in the previous homework, is provided to you. Run all three solutions and time them on the suite of test instances by running bench_opt5b.py, which outputs a CSV. Then provide a PDF chart that compares and answers: which encoding is fastest for N-queens?