BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Solving QBF by Counterexample-Guided Abstraction Refinement - Miko
 láš Janota\, INESC-ID\, Lisbon
DTSTART:20150220T090000Z
DTEND:20150220T100000Z
UID:TALK57941@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Quantified Boolean formulas (QBFs)\, as a PSPACE-complete prob
 lem\, 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 ex
 pands the formula into a SAT problem and uses a SAT solver in a blackbox-f
 ashion. In the second part of the talk we will look at some theoretical as
 pects of this algorithm\, which let us understand the significant improvem
 ents in performance on a number of instances in comparison to traditional 
 CDCL solving. This second part of the talk builds on results from proof th
 eory and circuit complexity and therefore we hope that the talk will be in
 teresting both for practitioners as well as theoretitians.
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR