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

- Computer science/Algorithms
- Logic/General logic/Classical propositional logic

### Session QBF_Solver_Verification

- NaiveSolver
- PCNF
- Parser
- SearchSolver
- SolverExport

## Cite

×

QBF_Solver_Verification-AFP

    @article{QBF_Solver_Verification-AFP,
      author  = {Axel Bergström and Tjark Weber},
      title   = {Verified QBF Solving},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/QBF_Solver_Verification.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest