Incremental SAT Solving for Quantified Boolean Formulas

In this project, I would like to explore the landscape of SAT-based quantified formulas, with the aim of improving the efficiency of their solutions. The Boolean Satisfiability problem (SAT) is the problem of determining whether a given Boolean formula can be satisfied by an interpretation. Many problems in computer science can be reduced to a SAT formulation: for instance, graph coloring [2], scheduling [4, 6], function fitting for Neural Networks [7] and circuit synthesis [3, 5], to only name a few, have all been expressed and then solved as SAT formulation. Hence, the importance of the efficiency of SAT solvers cannot be overstated: every improvement in the performance of the solver is directly translated to improvements in all of the fields described above.

A Quantified Boolean formula (QBF) is a Boolean formula that contains quantifiers, and there is a particular interest, out of all possible Quantified Boolean formulas, in those that contain exactly two quantifiers; this is because, again, several problems in computer science can be expressed and solved by using just two quantifiers – these are called 2QBF problems. Solving problems expressed by formulas that contain quantifiers is tangibly harder than solving those that do not contain any: giving to the z3 [1] SMT solver a quantified formula in input to be solved, versus a non-quantified one of otherwise the same problem, can have an impact of an excruciatingly longer processing time.

In this proposal, and in my research visit to Prof. Constantinides’ laboratory at Imperial College London, we mean to develop new ways to solve 2QBF problems -- in particular to explore a novel algorithm to implement the forall functionality incrementally -- which scale better and more efficiently than state of the art alternatives.