Abandoning Prenex Clausal Normal Form in QBF Solving

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

• Martina Seidl - Vienna University of Technology
• Thursday 18 March 2010, 11:00-12:00
• Small public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

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

Abstract: In the last decades, numerous successful QSAT solvers have been developed. However, most of these solvers process formulas only in prenex conjunctive normal form (PCNF). As for many practical applications encodings into QBFs usually do not result in PCNF formulas, a further transformation step is necessary. This transformation often introduces new variables and disrupts the structure of the formula. In this talk, we discuss the disadvantages of prenex conjunctive normal form and describe an alternative way to process QBFs without the drawbacks of the normal form transformation. We briefly describe the solver qpro, which is able to handle formulas in negation normal form. To this end, we extend algorithms for QBFs to the non-normal form case and generalize well-known pruning concepts. For a concise description of the extended algorithms, we follow a sequent-style characterization approach.

Biography: Martina Seidl is researcher at the Institute of Software Technology and Interactive Systems, Vienna University of Technology, Austria. She received her doctoral degree in 2007 for the thesis “A Solver for Quantified Boolean Formulas in Negation Normal Form`. Her research interests include automated theorem proving with special focus on QBF solver construction and optimization techniques. Furthermore, she is involved in research on model-driven engineering, in particular on model versioning.

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)
• 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
• Small public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.