Learning to Solve Quantified Boolean Formulas

Owing to the remarkable performance of modern satisfiability (SAT) solvers, propositional logic has established itself as the language of choice for encoding hard combinatorial problems arising in safety-critical ICT domains such as planning, verification, and synthesis. However, the complexity of these problems often exceeds the complexity of SAT, and so a propositional encoding can be exponentially larger than the original problem description. This imposes a limit on the problem instances that can be solved even with extremely efficient SAT solvers and has prompted research on more succinct languages such as Quantified Boolean Formulas (QBFs). QBFs extend propositional formulas with existential and universal quantification over truth values and can be exponentially smaller. The downside of this succinctness is that the satisfiability problem of QBFs is much harder than SAT, and despite of substantial progress, practically relevant instances remain hard to solve. The proposed project aims to reimagine QBF solvers as STRATEGY LEARNING ALGORITHMS. This involves the design of solvers that use strategy learning (Theme A), and the development of corresponding theory (Theme B). Specifically, we will A) augment existing solvers with strategy learning as well as design new solver architectures based on strategy learning, and B) perform a fine-grained complexity analysis of QBF solving as strategy learning and study properties of strategies that affect learnability.