Mini-Project Milestone

Due: Friday, May 29 at 5:00 PM | 50 points

The milestone is due Friday May 29 at 17:00 and is worth 50 points. You submit a working prototype and a one-page doc.

The milestone checks three things: you have picked a tractable problem, you have a real Z3 encoding running on at least one input, and you have a clear path to the final. It is not a rehearsal for the final, and it is not graded as one.

What to submit

Submit two things on Gradescope (group submission if you have a partner):

• Code. A repo or zip containing your Z3 code that runs on at least one concrete input end-to-end. Hardcoding and hacks are fine, and the tool does not need to be finished. What we are checking is that you can drive Z3 on a real instance of your problem.
• One-page doc. Plain PDF or markdown. The three sections below.

What goes in the doc

Problem statement (10 points). One paragraph. What are you solving? What are the inputs? What are the outputs? Why is a solver the right tool?

Working prototype (25 points). Point at the file in your code that runs the end-to-end example. Describe what input it takes, what output it produces, and what part of the encoding is doing the real work.

Plan for the final (15 points). One paragraph. What will you add between now and the final? What will your "beats naive" story be? Name what the solver will do that a naive approach can't.

Grading

Each section is graded in three tiers: full credit, partial, or zero. The milestone is largely pass-fail. If you have a working prototype on one input and a clear plan, you will get most of the points.

Standard grace window: Monday June 1 08:00.

Stuck?

If you don't have a working prototype on milestone day, come to office hours that week. Don't wait for the milestone grade.