Lesson 5

Most modern SAT solvers are based on backtracking. It can be shown that from the execution tree of such an algorithm on an unsatisfiable formula one can construct a resolution proof of the unsatisfiability of this formula.

Thus, if a SAT solver has run and proved that the formula is unsatisfiable, one can also ask it to output a proof of unsatisfiability (usually controlled by a separate flag). Current formats of such proofs allow them to be verified very simply (almost mechanically). For example, the resolution inference rule is checked very easily: one just needs to ensure that the resolvent of two given clauses is constructed correctly.

However, there are no guarantees that the proof will be short! In practice, proofs of unsatisfiability are often huge.