Marijn Heule, Armin Biere,
"What a Difference a Variable Makese"
: Proc. 24th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18), Serie Lecture Notes in Computer Science (LNCS), Vol. vol. 10806, Springer, Seite(n) 75-92, 2018
Original Titel:
What a Difference a Variable Makese
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 24th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18)
Original Kurzfassung:
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.
Sprache der Kurzfassung:
Englisch
Englische Kurzfassung:
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.
Forschungs-