Proofs for Satisfiability Problems

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 [64] and extracting a minimal unsatisfiable set (MUS) [49] 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 [69], require for learned clauses (lemmas) a list of antecedents. On the other hand, for clausal proofs, as described in Berkmin in 2003 [32], 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 [47] or in advanced techniques for MUS extraction [50]. 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 [41]. Recent works also use clausal proofs for interpolation [33] and MUS extraction [11].