Extracting and Checking Q-Resolution Proofs from a State-Of-The-Art QBF-Solver

The logic of Quantified Boolean Formulas (QBF) is an extension of propositional logic and provides compact encodings of real world problems in various fields of application, e.g., formal verification, reasoning and artificial intelligence. In recent years, the development of efficient decision procedures for QBF has progressed considerably. However, most current state-of-the-art QBF-solvers return mere true/false answers to a given problem, which is often not sufficient. Hence, it is a highly requested feature for QBF-solvers to provide the possibility to extract so-called certificates of (un)satisfiability in order to give evidence of the correctness of a solver's result. Further, certificates enable the identification of concrete solutions for a given problem, which is one of the key requirements for real world problems in many fields of application. In this thesis, we provide the extraction and validation of resolution proofs of (un)satisfiability as part of the certification workflow for the state-of-the-art QBF-solver DepQBF. DepQBF is a dependency-aware search-based solver for QBF in prenex conjunctive normal form and placed first in the main track of the QBFEVAL competition in 2010. We give a brief overview of QBF solving as implemented in DepQBF and introduce the QRP format, a novel text-based format for resolutionbased traces and proofs. We then present the extension of DepQBF to record resolution-based traces in QRP format and introduce QRPcheck, a tool for extracting and validating the corresponding resolution proofs of (un)satisfiability, in detail. We apply tracing, proof extraction and proof checking on the benchmark sets of the QBFEVAL competitions 2008 and 2010 and present an extensive evaluation of the results. It shows that within given time and memory constraints, over 95% of all solved instances were validated successfully by QRPcheck. Further, all instances validated by QRPcheck proved to have been solved correctly by DepQBF.