Name
Title | ||
|---|---|---|
Bridging the gap between easy generation and efficient verification of unsatisfiability proofs |
Abstract | ||
|---|---|---|
AbstractSeveral 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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1002/stvr.1549 | Periodicals |
Keywords | Field | DocType |
satisfiability solving,verification,tool | Programming language,Embedding,Computer science,Satisfiability,Bridging (networking),Theoretical computer science,Preprocessor,Mathematical proof | Journal |
Volume | Issue | ISSN |
24 | 8 | 0960-0833 |
Citations | PageRank | References |
2 | 0.37 | 8 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marijn J. H. Heule | 1 | 605 | 49.51 |
| Warren A. Hunt, Jr. | 2 | 520 | 59.18 |
| Nathan Wetzler | 3 | 97 | 4.71 |