CISPA
Browse

File(s) not publicly available

Simulating Strong Practical Proof Systems with Extended Resolution

journal contribution
posted on 2023-11-29, 18:07 authored by Benjamin 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", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC