Learning to Solve Quantified Boolean Formulas (Research Project)
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.
- Unique: A preprocessor for (D)QBF that computes unique Skolem and Herbrand functions (GitHub).
- Pedant: A certifying DQBF solver based on definition extraction (GitHub).