Marijn Heule, Martina Seidl, Armin Biere,
"Solution Validation and Extraction for QBF Preprocessing"
, in Journal of Automated Reasoning, Vol. 58 (1), Springer, Seite(n) 97-125, 2017, ISSN: 0168-7433
Original Titel:
Solution Validation and Extraction for QBF Preprocessing
Sprache des Titels:
Englisch
Original Kurzfassung:
Inthecontextofreasoningonquanti?edBooleanformulas(QBFs),theextensionofpropositionallogicwithexistentialanduniversalquanti?ers,itisbene?cial tousepreprocessingforsolvingQBFencodingsofreal-worldproblems.Preprocessing applies rewriting techniques that preserve (satis?ability) equivalence and that do not destroy the formula?s CNF structure. In many cases, preprocessing either solves a formula directly or modi?es 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 ef?cient proof checking and solution generation was not possible so far. Thisarticlepresentsauni?edproofsystemwiththreesimplerulesbasedonquanti?ed resolution asymmetric tautology (QRAT). In combination with an extended version of universal reduction, we use this proof system to ef?ciently 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.
Forschungs-