Verified QBF Solving

Axel Bergström and Tjark Weber. Archive of Formal Proofs, March 2024. Formal proof development.

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.}

Download

The original publication is available at https://www.isa-afp.org/entries/QBF_Solver_Verification.html.

BibTeX

@article{bergstrom24verified,
  author   = {Axel Bergstr{\"{o}}m and Tjark Weber},
  title    = {Verified {QBF} Solving},
  journal  = {Archive of Formal Proofs},
  month    = mar,
  year     = {2024},
  note     = {\url{https://www.isa-afp.org/entries/QBF_Solver_Verification.html}, Formal proof development}
}