Download PDFOpen PDF in browser

FERPModels: a Certification Framework for Expansion-Based QBF Solving

EasyChair Preprint 9624

4 pagesDate: January 27, 2023

Abstract

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

Keyphrases: Function Extraction, Quantified Boolean Formulas, certification

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:9624,
  author    = {Vedad Hadžić and Roderick Bloem and Ankit Shukla and Martina Seidl},
  title     = {FERPModels: a Certification Framework for Expansion-Based QBF Solving},
  howpublished = {EasyChair Preprint 9624},
  year      = {EasyChair, 2023}}
Download PDFOpen PDF in browser