Mark Peyrer,
"Preprocessing of Non-QCNF Prenex Formulas"
, 2-2024
Original Titel:
Preprocessing of Non-QCNF Prenex Formulas
Sprache des Titels:
Englisch
Original Kurzfassung:
Many current solvers for Quantified Boolean Formulas (QBFs) heavily rely on the Quantified Conjunctive Normal Form (QCNF) representation. While those solvers produce good results, there are formulas in non-QCNF which have to be transformed in order to be solved. By doing so, we potentially lose information about the original structure.
In this thesis we present approaches for non-QCNF Prenex formulas trying to reduce complexity by preprocessing in order to solve them more efficiently. We furthermore implement a preprocessor called PreProQ and evaluate the impact on different solvers using current problem instances.
Forschungs-