Learning to Solve Quantified Boolean Formulas (Research Project)
Funding Organisation: Vienna Science and Technology Fund, WWTF
Project Number: ICT19-060
Duration: 05/2020 - 04/2023
Project Team
Franz Xaver Reichl (PhD Student)
Leroy Chew (PostDoc)
Friedrich Slivovsky (PI)
Stefan Szeider (Co-PI)
Topic
Quantified Boolean Formulas (QBFs) can succinctly encode hard problems arising in planning, verification,
and synthesis, and the development of efficient procedures for evaluating QBFs (so-called QBF solvers)
will drive advances in all of these areas.
These applications require that QBF solvers not only decide whether a formula is true or false but also
output a witnessing strategy. For instance, when using QBF to solve a program synthesis problem, we
expect solvers to return the synthesized program. Our work on solver design and proof theory has
convinced us that strategies are at the heart of QBF research. However, the prevailing theoretical models of
QBF solvers as decision procedures or proof systems do not capture the fact that they need to compute
strategies. This project aims to develop a new, richer model of QBF solvers as strategy learning algorithms.
Software
- Unique: A preprocessor for (D)QBF that computes unique Skolem and Herbrand functions (GitHub).
- Pedant: A certifying DQBF solver based on definition extraction (GitHub).
