University of Cambridge > > Microsoft Research Cambridge, public talks > Abandoning Prenex Clausal Normal Form in QBF Solving

Abandoning Prenex Clausal Normal Form in QBF Solving

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.

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


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