Abandoning Prenex Clausal Normal Form in QBF Solving

  • Martina Seidl | Vienna University of Technology

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.

Speaker Details

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.

    • Portrait of Jeff Running

      Jeff Running

Watch Next