FERPModels: A Certification Framework for Expansion-Based QBF Solving

Roderick Bloem; Vedad Hadzic; Ankit Shukla; Martina Seidl

doi:10.1109/SYNASC57785.2022.00022

FERPModels: A Certification Framework for Expansion-Based QBF Solving

Roderick Bloem, Vedad Hadzic, Ankit Shukla, Martina Seidl

Institute of Applied Information Processing and Communications (7050)

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

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.

Original language	English
Title of host publication	Proceedings - 2022 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2022
Pages	80-83
Number of pages	4
DOIs	https://doi.org/10.1109/SYNASC57785.2022.00022
Publication status	Published - 2022
Event	24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing: SYNASC 2022 - Johannes-Kepler-Univ. Linz, Hybrider Event, Linz, Austria Duration: 12 Sept 2022 → 15 Sept 2022

Conference

Conference	24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
Abbreviated title	SYNASC 2022
Country/Territory	Austria
City	Hybrider Event, Linz
Period	12/09/22 → 15/09/22

Keywords

QBFs
∀Exp-Res
proof generation
strategy extraction

Access to Document

10.1109/SYNASC57785.2022.00022

synasc22Submitted manuscript, 201 KBLicence: CC BY-ND 4.0

Cite this

Bloem, R , Hadzic, V, Shukla, A & Seidl, M 2022, FERPModels: A Certification Framework for Expansion-Based QBF Solving. in Proceedings - 2022 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2022. pp. 80-83, 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Hybrider Event, Linz, Austria, 12/09/22. https://doi.org/10.1109/SYNASC57785.2022.00022

@inproceedings{3c58461830c7428a8606688864c8190d,

title = "FERPModels: A Certification Framework for Expansion-Based QBF Solving",

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.",

keywords = "QBFs, ∀Exp-Res, proof generation, strategy extraction",

author = "Roderick Bloem and Vedad Hadzic and Ankit Shukla and Martina Seidl",

year = "2022",

doi = "10.1109/SYNASC57785.2022.00022",

language = "English",

isbn = "978-166546545-8",

pages = "80--83",

booktitle = "Proceedings - 2022 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2022",

note = "24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing : SYNASC 2022, SYNASC 2022 ; Conference date: 12-09-2022 Through 15-09-2022",

}

TY - GEN

T1 - FERPModels: A Certification Framework for Expansion-Based QBF Solving

AU - Bloem, Roderick

AU - Hadzic, Vedad

AU - Shukla, Ankit

AU - Seidl, Martina

PY - 2022

Y1 - 2022

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

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

KW - QBFs

KW - ∀Exp-Res

KW - proof generation

KW - strategy extraction

U2 - 10.1109/SYNASC57785.2022.00022

DO - 10.1109/SYNASC57785.2022.00022

M3 - Conference paper

SN - 978-166546545-8

SP - 80

EP - 83

BT - Proceedings - 2022 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2022

T2 - 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing

Y2 - 12 September 2022 through 15 September 2022

ER -

FERPModels: A Certification Framework for Expansion-Based QBF Solving

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this