A Verified CEGAR-based QBF Solver


Quantified Boolean Formulas are formulas that, in addition to Boolean variables and the usual connectives of propositional logic (i.e., logical and, or, negation), may contain existential and universal quantifiers that range over Booleans. For instance, this is an example of a QBF:

∀x ∃y ∃z ((x ∨ z) ∧ y)

This particular formula is equivalent to true. (We can choose y and z to be true, then the formula evaluates to true both when x is true and when x is false.) In general, a QBF without free variables is equivalent either to true or to false.

A software tool that decides whether a given QBF is equivalent to true is called a QBF solver.

The goal of this project is to implement a QBF solver based on counter-example guided abstraction refinement (CEGAR) in the interactive proof assistant Isabelle, and to prove that its answers are correct. The CEGAR-based algorithm is described here.

This project will allow you to become familiar with Isabelle, one of the world's leading software tools to assist with the development of formal proofs.

Work environment:
Isabelle (Windows/macOS/Linux)
Useful knowledge/skills:
Basic mathematics, first-order logic, functional programming
Contact:
Tjark Weber

Last modified: 2024-05-15