Reducing Treewidth for SAT-Related Problems Using Simple Liftings

Tree decompositions are a powerful tool to obtain parameterized algorithms, in particular to solve different variants of the satisfiability problem. Most algorithms are based on a tree decomposition of the so called primal graph. Variants of the satisfiability problem that allow parameterized algorithms in the treewidth of the primal graph are for example Model Counting, MaxSat or QBF. To obtain efficient algorithms in practice, reducing the size of the instance by preprocessing is a very important technique and hence is highly investigated. In this paper, we investigate how preprocessing techniques can be used to reduce the parameter of a parameterized algorithm other than the size of the instance. In particular, we look at satisfiability and related problems and try to preprocess the formula in order to reduce the treewidth of the resulting primal graph. To the best of our knowledge, this is the first such approach. We show how to compute a set of auxiliary variables and an equisatisfiable (w.r.t. the original variables) formula using those such that the treewidth of the resulting primal graph is minimal under all sets of auxiliary variables. To reach this goal, we restrict our attention to auxiliary variables such that their value has to be the value of a subclause of the formula for each satisfying truth assignment. We implemented our approach and evaluated it on standard benchmark instances. While our approach is able to reduce the treewidth of around \(10\%\) of the instances, there is no clear improvement in the running time when solving the formula, due to the dependence of the practical efficiency of the solver on the structure of the formula.