Games and Decisions for Rigorous Systems Engineering

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	15 Nov 2012
Event title	Dagstuhl Seminar 12461
Event type	Conference
Location	GermanyShow on map