Vorträge und Posterpräsentationen (ohne Tagungsband-Eintrag):
M. Seidl:
"Abandoning Prenex Clausal Normal Form in QBF Solving";
Vortrag: Dagstuhl Seminar "Algorithms and Applications for Next Generation SAT Solvers",
Schloss Dagstuhl (eingeladen);
08.11.2009
- 13.11.2009.
Kurzfassung englisch:
In the last decades, a wealth of successful QSAT solvers has 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.
We briefly discuss the disadvantages of prenex conjunctive normal form and describe an alternative way to process QBFs without the drawbacks of the normal form transformations. We briefly describe our 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. Especially, we generalize well-known pruning concepts to the non-clausal case. In order to prove properties of the algorithms generalized to non-clausal form, we use a sequent-style reconstruction of DPLL.