FERPModels: A Certification Framework for Expansion-Based QBF Solving

Roderick Bloem, Vedad Hadzic, Ankit Shukla, Martina Seidl

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review


Modern expansion-based solvers for quantified Boolean formulas (QBFs) are successful in many applications. However, no such solver supports the generation of proofs needed to independently validate the correctness of the solving result and for the extraction of winning strategies which encode concrete solutions to the application problems.

In this paper, we present a complete tool chain for proof generation, result validation, and for universal winning strategy extraction in the context of expansion-based solving. In particular, we introduce a proof format for the ∀Exp-Res calculus on which expansion-based solving is founded, implement proof generation in a recent QBF solver, provide a checker for these proofs, and develop a new strategy extraction algorithm.
Original languageEnglish
Title of host publicationInternational Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) 2022
Number of pages4
Publication statusAccepted/In press - 12 Sep 2022
EventSYNASC 2022: 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing - Johannes-Kepler-Univ. Linz, Hybrider Event, Austria
Duration: 12 Sep 202215 Sep 2022


ConferenceSYNASC 2022
Abbreviated titleSYNASC 2022
CityHybrider Event


  • QBFs
  • ∀Exp-Res
  • proof generation
  • strategy extraction

Cite this