Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere,
"Resolution-Based Certificate Extraction for QBF"
: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT 2012), Serie Lecture Notes in Computer Science (LNCS), Vol. 7317, Springer, Seite(n) 430 - 435, 2012, ISBN: 978-3-642-31611-1
Original Titel:
Resolution-Based Certificate Extraction for QBF
Sprache des Titels:
Englisch
Original Buchtitel:
Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT 2012)
Original Kurzfassung:
A certificate of (un)satisfiability for a quantified Boolean formula (QBF) represents sets of assignments to the variables, which act as witnesses for its truth value. Certificates are highly requested for practical applications of QBF like formal verification and model checking. We present an integrated set of tools realizing resolution-based certificate extraction for QBF in prenex conjunctive normal form. Starting from resolution proofs produced by the solver DepQBF, we describe the workflow consisting of proof checking, certificate extraction, and certificate checking. We implemented the steps of that workflow in stand-alone tools and carried out comprehensive experiments. Our results demonstrate the practical applicability of resolution-based certificate extraction.