Solution Validation and Extraction for QBF Preprocessing

InthecontextofreasoningonquantifiedBooleanformulas(QBFs),theextensionofpropositionallogicwithexistentialanduniversalquantifiers,itisbeneficial tousepreprocessingforsolvingQBFencodingsofreal-worldproblems.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 ofSkolemfunctions.Inparticularfortheimportanttechniqueofuniversalexpansion efficient proof checking and solution generation was not possible so far. Thisarticlepresentsaunifiedproofsystemwiththreesimplerulesbasedonquantified resolution asymmetric tautology (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 QRATproofloggingandprovideaproofcheckerforQRATproofswhichisalsoable to extract Skolem functions.