Marijn Heule, Martina Seidl, Armin Biere,
"A Unified Proof System for QBF Preprocessing"
: Proc. 7th Joint Conf. on Automated Reasoning (IJCAR'14), Serie Lecture Notes in Computer Science (LNCS), Vol. 8562, Springer, Seite(n) 91-106, 2014
Original Titel:
A Unified Proof System for QBF Preprocessing
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 7th Joint Conf. on Automated Reasoning (IJCAR'14)
Original Kurzfassung:
For quantified Boolean formulas (QBFs), preprocessing is
essential to solve many real-world formulas. The application of a preprocessor,
however, prevented the extraction of proofs for the original
formula. Such proofs are required to independently validate correctness
of the preprocessor's rewritings and the solver's result. Especially for
universal expansion proof checking was not possible so far. In this paper,
we introduce a unified proof system based on three simple and elegant
quantified resolution asymmetric tautology (QRAT) rules. In combination
with an extended version of universal reduction, they are sufficient
to efficiently express all preprocessing techniques used in state-of-the-art
preprocessors including universal expansion. Moreover, these rules give
rise to new preprocessing techniques. We equip our preprocessor bloqqer
with QRAT proof logging and provide a proof checker for QRAT proofs.
Forschungs-