"Extracting and Validating Skolem/Herbrand Function-Based QBF Certificates"
, Johannes Kepler University Linz, Linz, 5-2012
Extracting and Validating Skolem/Herbrand Function-Based QBF Certificates
Sprache des Titels:
Quantified Boolean Formulas (QBF) allow succinct representations of many
real-world problems, e.g., in formal verification, artificial intelligence, or
computer-aided design of integrated circuits. Hence, for many practical instances
of QBF efficient decision procedures are highly requested. However,
in many applications of QBF, it is not sufficient to "just" solve problems
but necessary to provide additional valuable information also denoted as
certificates. Given a problem formulated in QBF, it is possible to extract
In this thesis, we present the tools QRPcert and CertCheck for extracting
and validating Skolem/Herbrand function-based QBF certificates of (un)satisfiability,
which we obtain from Q-resolution proofs and traces. We discuss
the process of certificate extraction as implemented in QRPcert in detail and
further describe the validation of those certificates by means of CertCheck
and a SAT solver.
We applied our tools to the benchmark sets of the QBF competitions
2008 and 2010 and provide an extensive evaluation of the results. As a base
for QBF certificate extraction, we used Q-resolution traces recorded by the
state-of-the-art QBF solver DepQBF. The results of our experiments show
that the employed extraction technique is a promising approach for a unified
certification framework for QBF.
Finally, we discuss open problems and ideas for extending our tools in
order to improve the certification workflow as employed in our experiments.