FERPModels: A Certification Framework for Expansion-Based QBF Solving

Roderick Bloem, Vedad Hadzic, Ankit Shukla, Martina Seidl

Publikation: Beitrag in Buch/Bericht/KonferenzbandBeitrag in einem KonferenzbandBegutachtung

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 ∀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.
Originalspracheenglisch
TitelProceedings - 2022 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2022
Seiten80-83
Seitenumfang4
DOIs
PublikationsstatusVeröffentlicht - 2022
Veranstaltung24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing: SYNASC 2022 - Johannes-Kepler-Univ. Linz, Hybrider Event, Linz, Österreich
Dauer: 12 Sept. 202215 Sept. 2022

Konferenz

Konferenz24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
KurztitelSYNASC 2022
Land/GebietÖsterreich
OrtHybrider Event, Linz
Zeitraum12/09/2215/09/22

Fingerprint

Untersuchen Sie die Forschungsthemen von „FERPModels: A Certification Framework for Expansion-Based QBF Solving“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren