Solution Validation and Extraction for QBF Preprocessing

In the context of reasoning on quantified Boolean formulas (QBFs), the extension of propositional logic with existential and universal quantifiers, it is beneficial to use preprocessing for solving QBF encodings of real-world problems. Preprocessing applies rewriting techniques that preserve (satisfiability) equivalence and that do not destroy the formula’s CNF structure. In many cases, preprocessing either solves a formula directly or modifies it such that information helpful to solvers becomes better visible and irrelevant information is hidden. The application of a preprocessor, however, prevented the extraction of proofs for the original formula in the past. Such proofs are required to independently validate the correctness of the preprocessor’s rewritings and the solver’s result as well as for the extraction of solutions in terms of Skolem functions. In particular for the important technique of universal expansion efficient proof checking and solution generation was not possible so far. This article presents a unified proof system with three simple rules based on quantified resolution asymmetric tautology (\(\mathsf {QRAT}\)). In combination with an extended version of universal reduction, we use this proof system to efficiently express current preprocessing techniques including universal expansion. Further, we develop an approach for extracting Skolem functions. We equip the preprocessor bloqqer with \(\mathsf {QRAT}\) proof logging and provide a proof checker for \(\mathsf {QRAT}\) proofs which is also able to extract Skolem functions.