Unsatisfiability Proofs
SAT solvers determine whether formulas in conjunctive normal form
are satisfiable or not. If a formula is satisfiable, the solver
outputs a satisfying assignment, which can then be checked against
the original formula. If a formula is not satisfiable, the solver
can write a proof demonstrating that fact, again giving an
independent way to check the solver's solution is correct. This
language describes some such proof languages.
- LRAT proof format:
The LRAT
proof format is our host language on which the other
extensions build, defining what it means for a formula to be
satisfiable, the proof format, and a check for a given proof
being valid, proving the original formula is unsatisfiable if
the proof of its unsatisfiability checks out. Strictly
speaking, this only implements the RUP subset of the LRAT
format; adding the RAT portion is not extensibly interesting.
- DRAT extension:
The DRAT
proof format is the current standard for unsatisfiability
proofs, which does not contain proof hints like LRAT does. This
extension adds an extraction of LRAT proofs to DRAT proofs and a
check for a DRAT proof being valid. As before, this only
implements the RUP subset of the DRAT format, and proves the
extracted DRAT proof is valid if the original is.
- FRAT extension:
The FRAT
proof format is another format for unsatisfiability
proofs. It builds on the LRAT format, adding some more line
types, such as renumbering clauses. This extension adds some of
FRAT's line types to the proof format. It also defines the
first step of FRAT elaboration to transform FRAT proofs to plain
LRAT proofs, the first step being to remove unneeded lines. The
correctness of this transformation is also proven, that a
transformed proof is valid whenever the original proof is.
- Clauses extension: This
extension adds a new clause constructor to represent certain
clauses more efficiently.
