Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. (3rd October 2014)

• Record Type: Journal Article
• Authors: Heule, Marijn J. H.; Hunt, Warren A.; Wetzler, Nathan; Brucker, Achim D.; Julliand, Jacques
• Is Part Of: Software testing, verification & reliability. Volume 24:Number 8(2014)
• Page Start: 593
• Page End: 607
• Publication Date: 2014-10-03
• Subjects: Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.1549
• Languages: English
• ISSNs: 0960-0833

Abstract

<abstract abstract-type="main" id="stvr1549-abs-0001"> <title>SUMMARY</title> <p id="stvr1549-para-0001">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 <monospace>Glucose</monospace> 2.1, the SAT 2012 challenge winner, and <monospace>SatELite</monospace>, a popular SAT‐problem preprocessor. Copyright © 2014 John Wiley &amp; Sons, Ltd.</p> </abstract>