@inproceedings{5736368bc2284f9da13f809d8ced27e1,
title = "Resolution-Based Certificate Extraction for QBF",
abstract = "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.",
author = "Aina Niemetz and Mathias Preiner and Florian Lonsing and Martina Seidl and Armin Biere",
year = "2012",
language = "English",
isbn = "978-3-642-31611-1",
volume = "7317",
series = "Lecture Notes in Computer Science (LNCS)",
publisher = "Springer",
pages = "430 -- 435",
booktitle = "Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT 2012)",
}