Marijn Heule
A Unified Proof System for QBF Preprocessing
ACL2 Seminar, May 16, 2014

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.

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.