Simulating Strong Practical Proof Systems with Extended Resolution
- PDF / 623,605 Bytes
- 21 Pages / 439.37 x 666.142 pts Page_size
- 57 Downloads / 176 Views
Simulating Strong Practical Proof Systems with Extended Resolution Benjamin Kiesl1
· Adrián Rebola-Pardo2 · Marijn J. H. Heule3 · Armin Biere4
Received: 17 April 2020 / Accepted: 20 April 2020 © The Author(s) 2020
Abstract Proof systems for propositional logic provide the basis for decision procedures that determine the satisfiability status of logical formulas. While the well-known proof system of extended resolution—introduced by Tseitin in the sixties—allows for the compact representation of proofs, modern SAT solvers (i.e., tools for deciding propositional logic) are based on different proof systems that capture practical solving techniques in an elegant way. The most popular of these proof systems is likely DRAT, which is considered the de-facto standard in SAT solving. Moreover, just recently, the proof system DPR has been proposed as a generalization of DRAT that allows for short proofs without the need of new variables. Since every extendedresolution proof can be regarded as a DRAT proof and since every DRAT proof is also a DPR proof, it was clear that both DRAT and DPR generalize extended resolution. In this paper, we show that—from the viewpoint of proof complexity—these two systems are no stronger than extended resolution. We do so by showing that (1) extended resolution polynomially simulates DRAT and (2) DRAT polynomially simulates DPR. We implemented our simulations as proof-transformation tools and evaluated them to observe their behavior in practice. Finally, as a side note, we show how Kullmann’s proof system based on blocked clauses (another generalization of extended resolution) is related to the other systems. Keywords Propositional logic · SAT · SAT solving · Proof complexity · Resolution · DRAT · PR · Blocked clauses
This work has been supported by the National Science Foundation under Grant CCF-1910438, by the Austrian Science Fund (FWF) under Project W1255-N23, by the Vienna Science and Technology Fund (WWTF) under Projects VRG11-005 and ICT15-103, and by Microsoft Research through its Ph.D. Scholarship Programme.
B
Benjamin Kiesl [email protected]
1
CISPA Helmholtz Center for Information Security, Saarbrücken, Germany
2
TU Wien, Vienna, Austria
3
Carnegie Mellon University, Pittsburgh, USA
4
Johannes Kepler University, Linz, Austria
123
B. Kiesl et al.
1 Introduction When we look at proof systems for propositional logic, we observe an interesting peculiarity: Even though extended resolution, invented by Tseitin in the sixties [30], is known to be highly expressive, the practitioners in SAT solving have come up with different proof systems on which they base their solvers. The most important of these proof systems is likely DRAT [35], which can be considered the de-facto standard in SAT solving: Not only are the solvers in the annual SAT competitions required to produce DRAT proofs but also the proofs of longstanding mathematical problems, including the Boolean Erd˝os Discrepancy Conjecture [21] and the Boolean Pythagorean Triples Problem [11], were provided in DRAT.
Data Loading...
