What a Difference a Variable Makese

Marijn Heule; Armin Biere

What a Difference a Variable Makese

Marijn Heule, Armin Biere

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

We present an algorithm and tool to convert derivations from the powerful recently proposed PR proof system into the widely used DRAT proof system. The PR proof system allows short proofs without new variables for some hard problems, while the DRAT proof system is supported by top-tier SAT solvers. Moreover, there exist eﬃcient, formally veriﬁed checkers of DRAT proofs. Thus our tool can be used to validate PR proofs using these veriﬁed checkers. Our simulation algorithm uses only one new Boolean variable and the size increase is at most quadratic in the size of the propositional formula and the PR proof. The approach is evaluated on short PR proofs of hard problems, including the well-known pigeon-hole and Tseitin formulas. Applying our tool to PR proofs of pigeon-hole formulas results in short DRAT proofs, linear in size with respect to the size of the input formula, which have been certiﬁed by a formally veriﬁed proof checker.

Original language	English
Title of host publication	Proc. 24th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18)
Publisher	Springer
Pages	75-92
Number of pages	18
Volume	vol. 10806
Publication status	Published - 2018

Publication series

Name	Lecture Notes in Computer Science (LNCS)

Fields of science

102 Computer Sciences
102001 Artificial intelligence
102011 Formal languages
102022 Software development
102031 Theoretical computer science
603109 Logic
202006 Computer hardware

JKU Focus areas

Computation in Informatics and Mathematics

Cite this

@inproceedings{6ae97b3042f542a585c5508abd5b817e,

title = "What a Difference a Variable Makese",

abstract = "We present an algorithm and tool to convert derivations from the powerful recently proposed PR proof system into the widely used DRAT proof system. The PR proof system allows short proofs without new variables for some hard problems, while the DRAT proof system is supported by top-tier SAT solvers. Moreover, there exist eﬃcient, formally veriﬁed checkers of DRAT proofs. Thus our tool can be used to validate PR proofs using these veriﬁed checkers. Our simulation algorithm uses only one new Boolean variable and the size increase is at most quadratic in the size of the propositional formula and the PR proof. The approach is evaluated on short PR proofs of hard problems, including the well-known pigeon-hole and Tseitin formulas. Applying our tool to PR proofs of pigeon-hole formulas results in short DRAT proofs, linear in size with respect to the size of the input formula, which have been certiﬁed by a formally veriﬁed proof checker.",

author = "Marijn Heule and Armin Biere",

year = "2018",

language = "English",

volume = "vol. 10806",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "75--92",

booktitle = "Proc. 24th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18)",

}

TY - GEN

T1 - What a Difference a Variable Makese

AU - Heule, Marijn

AU - Biere, Armin

PY - 2018

Y1 - 2018

N2 - We present an algorithm and tool to convert derivations from the powerful recently proposed PR proof system into the widely used DRAT proof system. The PR proof system allows short proofs without new variables for some hard problems, while the DRAT proof system is supported by top-tier SAT solvers. Moreover, there exist eﬃcient, formally veriﬁed checkers of DRAT proofs. Thus our tool can be used to validate PR proofs using these veriﬁed checkers. Our simulation algorithm uses only one new Boolean variable and the size increase is at most quadratic in the size of the propositional formula and the PR proof. The approach is evaluated on short PR proofs of hard problems, including the well-known pigeon-hole and Tseitin formulas. Applying our tool to PR proofs of pigeon-hole formulas results in short DRAT proofs, linear in size with respect to the size of the input formula, which have been certiﬁed by a formally veriﬁed proof checker.

AB - We present an algorithm and tool to convert derivations from the powerful recently proposed PR proof system into the widely used DRAT proof system. The PR proof system allows short proofs without new variables for some hard problems, while the DRAT proof system is supported by top-tier SAT solvers. Moreover, there exist eﬃcient, formally veriﬁed checkers of DRAT proofs. Thus our tool can be used to validate PR proofs using these veriﬁed checkers. Our simulation algorithm uses only one new Boolean variable and the size increase is at most quadratic in the size of the propositional formula and the PR proof. The approach is evaluated on short PR proofs of hard problems, including the well-known pigeon-hole and Tseitin formulas. Applying our tool to PR proofs of pigeon-hole formulas results in short DRAT proofs, linear in size with respect to the size of the input formula, which have been certiﬁed by a formally veriﬁed proof checker.

M3 - Conference proceedings

VL - vol. 10806

T3 - Lecture Notes in Computer Science (LNCS)

SP - 75

EP - 92

BT - Proc. 24th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18)

PB - Springer

ER -