Verified QBF Solving

Axel Bergström 📧 and Tjark Weber 📧

March 6, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

A Quantified Boolean Formula (QBF) extends propositional logic with quantification over Boolean variables. We formalise two simple QBF solvers and prove their correctness. One solver is based on naive quantifier expansion, while the other utilises a search-based algorithm. Additionally, we formalise a parser for the QDIMACS input format and use Isabelle's code generation feature to obtain executable versions of both solvers.

License

BSD License

Topics

Session QBF_Solver_Verification