Marijn Heule, Armin Biere,
"Proofs for Satisfiability Problems"
: All about Proofs, Proofs for All (APPA), Mathematical Logic and Foundations, Serie College Publications 2015, Vol. 55, Seite(n) 1-22, 2015
Proofs for Satisfiability Problems
Sprache des Titels:
All about Proofs, Proofs for All (APPA), Mathematical Logic and Foundations
Satisfiability (SAT) solvers have become powerful tools to solve a wide range
of applications. In case SAT problems are satisfiable, it is easy to validate a
witness. However, if SAT problems have no solutions, a proof of unsatisfiability is
required to validate that result. Apart from validation, proofs of unsatisfiability
are useful in several applications, such as interpolation  and extracting a
minimal unsatisfiable set (MUS)  and in tools that use SAT solvers such as
theorem provers [4,65,66,67].
Since the beginning of validating the results of SAT solvers, proof logging of
unsatisfiability claims was based on two approaches: resolution proofs and clausal
proofs. Resolution proofs, discussed in zChaff in 2003 , require for learned
clauses (lemmas) a list of antecedents. On the other hand, for clausal proofs, as
described in Berkmin in 2003 , the proof checker needs to find the antecedents
for lemmas. Consequently, resolution proofs are much larger than clausal proofs,
while resolution proofs are easier and faster to validate than clausal proofs.
Both proof approaches are used in different settings. Resolution proofs are
often required in applications like interpolation  or in advanced techniques for
MUS extraction . Clausal proofs are more popular in the context of validating
results of SAT solvers, for example during the SAT Competitions or recently for
the proof of Erd}os Discrepancy Theorem . Recent works also use clausal
proofs for interpolation  and MUS extraction .