文献学习-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].

译文：然而，如果SAT问题没有解，则需要用不满足证明来验证该结果。

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

译文：自SAT解算结果验证开始以来，不可满足索赔的证明日志建立在两种方法上:解析证明和条款证明。

译文：2003年zChaff[69]讨论了决议证明，要求学习子句(引理)具有先行词列表。

译文：另一方面，对于子句证明，如Berkmin在2003[32]中所描述的，证明检查器需要找到引理的前例。

译文：因此，分解证明比分句证明大得多，而分解证明比分句证明更容易、更快地验证。

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].

Proof logging support became widespread in state-of-the-art solvers, such as Lingeling [13], Glucose [7], and CryptoMiniSAT [57], since SAT Competition 2013 made unsatisfiability proofs mandatory for solvers participating in the unsatisfiability tracks. About half the solvers that participated in recent SAT Competitions can emit clausal proofs, including the strongest solvers around, for example the three solvers mentioned above. However, very few solvers support emitting resolution proofs.

译文：因为2013年SAT竞赛对参与不满足轨道的求解者强制要求不满足证明。

The lack of support for resolution proofs is due to the difficulty to represent some techniques used in contemporary SAT solvers in terms of resolution. One such technique is conflict clause minimization [58], which requires several modifications of the solver in order to express it using resolution steps [62]. In contrast, emitting a clausal proof from SAT solvers such as MiniSAT [28] and Glucose requires only small changes to the code3 .