Problem Set 5

SAT

Before you start this problem set

Please fill out a survey about the time you spent on Problem Set 4.

Download

• pset05_definitions.dfy
• pset05.dfy
• pset05_validator.dfy

The structure here follows that of previous psets: read pset05_definitions.dfy to see our supporting definitions on Boolean satisfiability, complete pset05.dfy with your proofs of the requested functions and lemmas, and use pset05_validator.dfy to confirm you’re done.

Dafny VS Code settings

As the problem sets get more complex, there are are two configuration options you may want to change. The links below might jump you directly to the relevant settings, or you can find them in VSCode Settings → Extensions → Dafny extension configuration:

• Set Verification Time Limit to 10 seconds (Dafny’s default is 20). This is the amount of time Dafny will spend per lemma, function, etc. trying to verify correctness. For the problem sets, a verification that takes longer than a few seconds is unlikely to succeed given 10× more time, so the extra wait just slows you down.

• And if you prefer to have Dafny wait until you save your edits before attempting to verify them, set Automatic Verification to “onsave” instead of “onchange.”

Timeouts and {:isolate_assertions}

When verification of a lemma is timing out, it can be hard to tell which pieces Dafny was able to prove and which ones still need work.

• Using assert false, as we have see a few times in class, is a crucial incremental proving technique. It can help you check whether a proof is working up to a particular point, or whether it works assuming some case or sub-proof were completed.

• Another tool you can try is to add the {:isolate_assertions} annotation to your lemma (cf. {:induction false}) which asks Dafny to prove each assertion independently instead of batched together. This adds undesirable overhead you don’t want in the finished proof, but it may help you understand where a timeout is occurring.

And finally a note about partial credit

If you do not finish the problem set, the autograder will attempt to give you partial credit for the parts you did complete, but it can only do that if your code passes verification. That may require commenting out some of your work so that the remaining parts are all-green.

In the case of a submitted lemma with no body, the autograder will inject requires false and an empty body so that dafny audit can check for other issues, but you also cannot use that lemma in other proofs. If you don’t understand your autograder report, please visit office hours or post privately on Piazza, but be sure to do this ahead of the deadline.

Do not wait until the last minute to submit your work. While we recommend using VS Code to write your solutions, see instructions in Problem Set 3 for how to check your work on the command-line.