Preprocessing for quantified Boolean formulas

Abstract

This thesis presents a new preprocessor qbfMax for quantified boolean formulas (QBFs) in prenex conjunctive normal form (PCNF). Such formulas are successfully used to represent many different problems (e.g. planning, scheduling, verification etc.).<br />The preprocessor qbfMax simplifies formulas with many different simplification techniques (such as pure literal elimination, unit propagation, equivalence reduction, subsumption and the elimina- tion of variables using resolution) to shorten the input formulas wrt.<br />the number of clauses and the number of variables time efficient. The hypothesis this work is based on is that these simplifications support a QBF solver to perform the task of solving faster or even make it possible in the first place. To understand how a preprocessor can improve the solving capabilities of a solver it is important to know how todays solver work which is also presented in this work.<br />I obtained different benchmark families from the QBFLIB and ran tests on preQuel, proverbox and my preprocessor qbfMax to see how they work in comparison.<br />The prepro- cessors preQuel and proverbox are well known and available online. The new preprocessed formulas were then solved both with search-based QBF solvers (e.g.<br />sKizzo and QuBE) and a resolution-based solver (e.g. Quantor). The results of these tests demonstrate how my preprocessor assists the solver in decreasing the overall time needed to complete the benchmark set and in increasing the number of instances which where possible to solve within a given time limit. The results show that in comparison with the other tested pre- processors my preprocessor can shorten the length of the formulas most and is even able to solve most instances on its own. The main solvers then try to solve the original and all the preprocessed formulas. Here qbfMax could increase the number of solvable instances in comparison to the original instances although preQuel performed slightly better. This shows that even though the elimination of variables and clauses is an important factor when it comes to solving, it is also important not to destroy the structural information of the original formula.