Premium
Bridging the gap between easy generation and efficient verification of unsatisfiability proofs
Author(s) -
Heule Marijn J. H.,
Hunt Warren A.,
Wetzler Nathan
Publication year - 2014
Publication title -
software testing, verification and reliability
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.216
H-Index - 49
eISSN - 1099-1689
pISSN - 0960-0833
DOI - 10.1002/stvr.1549
Subject(s) - mathematical proof , computer science , satisfiability , bridging (networking) , preprocessor , automated proof checking , overhead (engineering) , theoretical computer science , embedding , programming language , algorithm , conjunctive normal form , model checking , mathematics , artificial intelligence , geometry , computer network
SUMMARY 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.