Scalable Certificate Extraction for QBF

Description

A certificate of (un)satisfiability for a quantified Boolean formula (QBF) represents concrete assignments to the variables of the formula. Certificates are not only witnesses for the truth value returned by a QBF solver, but also represent the solutions for practical applications of QBF like formal verification and model checking. Recently, an approach has been presented, which can be directly built on top of DPLL based QBF solvers. Starting from resolution proofs produced by the solver during clause and cube learning, the certificates are constructed by certain syntactic properties of the proof tree. Based on our integrated set of tools realizing resolution-based certificate extraction for QBFs in prenex conjunctive normal form, in this talk, we discuss the state-of-the-art of QBF certification and point out future challenges.

Period	30 Jun 2012
Event title	Joint SVARM & VERIFY Workshop 2012 affiliated with IJCAR 2012
Event type	Conference
Location	United KingdomShow on map