Aina Niemetz,
"Extracting and Checking Q-Resolution Proofs from a State-Of-The-Art QBF-Solver"
, Johannes Kepler University Linz, Linz, 5-2012
Original Titel:
Extracting and Checking Q-Resolution Proofs from a State-Of-The-Art QBF-Solver
Sprache des Titels:
Englisch
Original Kurzfassung:
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.