Simulating Strong Practical Proof Systems with Extended Resolution
journal contribution
posted on 2023-11-29, 18:07authored byBenjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule, Armin Biere
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 extended-resolution 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.
History
Preferred Citation
Benjamin Kiesl, Adrián Rebola-Pardo, Marijn Heule and Armin Biere. Simulating Strong Practical Proof Systems with Extended Resolution. In: Journal of Automated Reasoning. 2020.
Primary Research Area
Reliable Security Guarantees
Legacy Posted Date
2020-12-09
Journal
Journal of Automated Reasoning
Open Access Type
Gold
Sub Type
Article
BibTeX
@article{cispa_all_3325,
title = "Simulating Strong Practical Proof Systems with Extended Resolution",
author = "Kiesl, Benjamin and Rebola-Pardo, Adrián and Heule, Marijn J. H. and Biere, Armin",
journal="{Journal of Automated Reasoning}",
year="2020",
}