Abandoning Prenex Clausal Normal Form in QBF Solving

Опубликовано 17 августа 2016, 20:45

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.