A Unified Proof System for QBF Preprocessing
Marijn Heule
ACL2 Seminar, Oct. 7, 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. In this talk, we present 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 the preprocessor bloqqer with QRAT proof logging and
provide a proof checker for QRAT proofs.