Solving QBF by Counterexample-Guided Abstraction Refinement

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

• Mikoláš Janota, INESC-ID, Lisbon
• Friday 20 February 2015, 09:00-10:00
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

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 http://research.microsoft.com. 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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.