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

  Browse A-Z

Log in

University Account External (via Google)

๐Ÿ” Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

โ„น๏ธ Information

Solving QBF by Counterexample-Guided Abstraction Refinement

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 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:

Note that ex-directory lists are not shown.

Other lists

LGBTQ+@Cam Hybrid seminar: Clinical School Seminar Room 2 & on Zoom (see Abstract for link) Anglia Ruskin University - online

Other talks

Sheref Mansy, topic TBA LMB Seminar - Mechanisms of mRNA packaging and export Using numerical simulations for solving spectral geometry problems The organisational management of traumatic stress Together Now: Cooperation and Collaboration in Social Art Practice CUSCRS and Renal Medicine
 

ยฉ 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity