University of Cambridge > > Microsoft Research Cambridge, public talks > Solving QBF by Counterexample-Guided Abstraction Refinement

Solving QBF by Counterexample-Guided Abstraction Refinement

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

Quantified Boolean formulas (QBFs), as a PSPACE -complete problem, represent a powerful formalism but also a computational challenge. In this talk we will look at how QBFs can be solved by the counterexample-guided abstraction refinement paradigm (CEGAR). The presented technique expands the formula into a SAT problem and uses a SAT solver in a blackbox-fashion. In the second part of the talk we will look at some theoretical aspects of this algorithm, which let us understand the significant improvements in performance on a number of instances in comparison to traditional CDCL solving. This second part of the talk builds on results from proof theory and circuit complexity and therefore we hope that the talk will be interesting both for practitioners as well as theoretitians.

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2022, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity