Bridging the gap between easy generation and efficient verification of unsatisfiability proofs

摘要

Several proof formats have been used to verify refutations produced by satisfiability (SAT) solvers. Existing formats are either costly to check or hard to implement. This paper presents a practical approach that facilitates checking of unsatisfiability results in a time similar to proof discovery by embedding clause deletion information into clausal proofs. By exploiting this information, the proof-checking time is reduced by an order of magnitude on medium-to-hard benchmarks as compared to checking proofs using similar clausal formats. Proofs in a new format can be produced by making only minor changes to existing conflict-driven clause-learning solvers and their preprocessors, and the runtime overhead is negligible. This approach can easily be integrated into Glucose 2.1, the SAT 2012 challenge winner, and SatELite, a popular SAT-problem preprocessor. Copyright © 2014 John Wiley & Sons, Ltd.