Lesson 1

A common scenario of using SAT solvers for verification is as follows: we write down a CNF formula which is satisfiable if and only if something went wrong (a circuit produced an incorrect result, the system ended up in a forbidden state, etc.). If the SAT solver proves that the formula is unsatisfiable, then we can be sure that our system behaves as intended. Suppose we run a SAT solver and it says that the formula is unsatisfiable. Can it also produce a certificate of its unsatisfiability? (Note that a certificate of satisfiability is simply a satisfying assignment.)