# 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).