Coding Assignment 1: SAT Solving
Due: Friday, April 10 at 5:00 PM | 150 points
There is no Coding Assignment 01.
Coding Assignments
Four assignments across the quarter, each building on what you learn in lecture. You will write solver-aided code in Python using Z3, starting with SAT solving and working through theory solvers, SMT, and verification.
All coding assignments are individual work. You may discuss problems at a high level with classmates and use AI tools with attribution. See the Syllabus for the full collaboration policy.
Coding Assignment 2: Theory Solvers
Due: Friday, April 24 at 5:00 PM | 150 points
Coding Assignment 2 contains two parts. Here is an overview. Details will be provided embedded in starter code in the course repo.
- Part 1: (60 points) Choose one of the following SAT-based questions to solve.
- Option 1: Solving a puzzle involving placing queens on a chess board.
- Option 2: Creating a schedule for an event given many constraints.
- Option 3: Verifying that two digital circuits compute the same thing.
- Part 2: (60 points) Choose one of the following theory of EUF-based questions to solve.
- Option 1: Solving a puzzle involving category matching.
- Option 2: Verifying that two computer programs compute the same thing.
- Option 3: Verifying matrix multiplication identities.
- Part 3: (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?
- Can you draw any connections between problems in this homework assignment and your job, or your broader responsibilities? Can you imagine situations where you would personally use Z3? (If not yet, don't worry - we still have a lot of the course left to learn even more tools to unlock even broader applications!)
- 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?
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.
| # | Option | Points |
|---|---|---|
| 1 | Generate $N \times N$ magic squares | 30 |
| 2 | Solve sliding-tile puzzles | 60 |
| 3 | Solve a family-tree logic puzzle | 60 |
| 4 | Cutting pieces out of plywood | 60 |
| 5a | Converting SMT with LIA to pure LIA | 90 |
| 5b | N-queens via LIA and SMT | 90 |
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?
Coding Assignment 4: Verification
Due: Friday, May 22 at 5:00 PM | 150 points
Content will be posted before the assignment opens.