A New Approach to Quantified Boolean Formulas
Date:
Wednesday, April 5, 2017 17:00 - 18:00
Speaker:
Markus Rabe (UC Berkeley)
Location:
Mondi Seminar Room 2, Central Building
Series:
RiSE Seminar
Host:
Tom Henzinger
Contact:
BONVENTRE-DARTHE Astrid
Many of the challenging problems in verification and synthesis algorithms are naturally phrased in terms of quantified formulas. Our ability to solve these problems, however, is still unsatisfactory. Even when we take a look at the most basic logical theory with quantification, quantified boolean formulas (QBF), the most effective approach are CEGAR-style algorithms. But CEGAR is a generic algorithmic scheme, which means that we are not yet able to exploit the structure of quantified problems. In this talk I will discuss some of the fundamental limits of CEGAR-style algorithms and present a novel approach to solve quantified boolean formulas (currently restricted to one quantifier alternation, i.e. 2QBF). The algorithm adds new constraints to the formula until the constraints describe a unique Skolem function - or until the absence of a Skolem function is detected. Backtracking is required if the absence of Skolem functions depends on the newly introduced constraints. The algorithm can be best understood when compared to search algorithms for SAT. We will discuss how to lift propagation, decisions, and conflicts from values (SAT) to Skolem functions (QBF). The algorithm significantly improves over the state of the art in terms of the number of solved instances, solving time, and the size of certificates.