Extracting and Validating Skolem/Herbrand Function-Based QBF Certificates

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 such certificates. 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.