UNSAT 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. 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.
- Clauses extension: This
extension adds a new clause constructor to represent certain
clauses more efficiently.
- FRAT extension:
The FRAT proof
format combines the efficiency of checking (in standard
tools) of LRAT with the efficiency of generating proofs of DRAT.
This extension covers the RUP portion of FRAT and defines both
checking of the initial proof and elaboration to an LRAT proof
containing only the necessary portion of the clauses for
checking the proof is valid.
