Project

Your chance to use a solver in anger. Pick a problem, build a Z3-based tool that solves it, demonstrate it works, and explain your encoding.

Timeline

• Milestone, Friday May 29 at 17:00: working prototype plus a one-page doc. 50 points. See the milestone page for specifics.
• Demo Day, Tuesday June 2 in class: optional live demos.
• Final, Friday June 5 at 17:00: code, write-up, and demo recording. 150 points. See the final page for specifics.

Standard grace window: submit by Monday 08:00 with no penalty.

The "beats naive" rule

Your project should demonstrate something a naive approach can't do. That might be an optimization, an exhaustive verification, a synthesis, or a counterexample. Whatever it is, the write-up should name it and the demo should show it.

"If you get the reduction wrong, the solver gives you a correct answer to the wrong question." The project asks you to get the reduction right.

Kinds of projects

Pick a problem you care about. The only rule is that a solver does real work in the solution. The kinds below are common starting points.

Verification. You have a system (program, protocol, configuration, design) and a property you want to be sure of. You encode both and ask Z3 whether the property holds, or to find a counterexample.

Synthesis. You want Z3 to find something for you: a program fragment, a configuration, a structure, a rule. You write down what counts as correct, and Z3 produces a candidate.

Analysis and optimization. You have a real problem with constraints on resources, conflicts, or preferences. You want a feasible or optimal answer. The hard work is encoding the problem; the solver does the search.

Bring your own. You bring a constraint-shaped problem from your work or life. If it touches anything proprietary, build a simplified, IP-free model and encode that instead. Do not paste internal code or confidential data into your write-up, demo, or Ed posts.

Working with a partner

Partners are encouraged but not required. Pairs submit jointly on Gradescope and receive one shared grade. Scope expectations are the same as for solo work. A partner is there to think with, not to enable a bigger project. Triples are allowed if you ask first.

If your partnership runs into trouble, email staff.

AI policy

The course AI policy applies: AI tools are fine to use, attribution is required. The write-up's "what I learned" section is where attribution goes.

Getting stuck

The milestone is a forcing function, not a rescue point. Grading takes us time, and there is only a week between milestone and final. You will not get useful feedback fast enough to recover from a bad direction.

If you are stuck on scope, on encoding, or on whether your problem is a fit for Z3, come to office hours early. It is much easier to help you pivot in Week 8 than to triage at the milestone.