Information and Communication Technology 2019ICT19-060

Learning to Solve Quantified Boolean Formulas

Principal Investigator:
Project title:
Learning to Solve Quantified Boolean Formulas
Stefan Szeider (Vienna University of Technology) (Co-Principal Investigator)
Ongoing (01.05.2020 – 30.04.2023)
Funding volume:
€ 330,890


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.


We use cookies on our website. Some of them are technically necessary, while others help us to improve this website or provide additional functionalities. Further information