Resolution-Based Certificate Extraction for QBF - (Tool Presentation)

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.

Authors

• Aina Niemetz
• Mathias Preiner
• Florian Lonsing
• Martina Seidl
• Armin Biere

Keywords

No keywords are indexed for this paper.