Preprocessing of Non-QCNF Prenex Formulas

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.