Search Results

Documents authored by Heisinger, Maximilian


Document
Validation of QBF Encodings with Winning Strategies

Authors: Irfansha Shaik, Maximilian Heisinger, Martina Seidl, and Jaco van de Pol

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)


Abstract
When using a QBF solver for solving application problems encoded to quantified Boolean formulas (QBFs), mainly two things can potentially go wrong: (1) the solver could be buggy and return a wrong result or (2) the encoding could be incorrect. To ensure the correctness of solvers, sophisticated fuzzing and testing techniques have been presented. To ultimately trust a solving result, solvers have to provide a proof certificate that can be independently checked. Much less attention, however, has been paid to the question how to ensure the correctness of encodings. The validation of QBF encodings is particularly challenging because of the variable dependencies introduced by the quantifiers. In contrast to SAT, the solution of a true QBF is not simply a variable assignment, but a winning strategy. For each existential variable x, a winning strategy provides a function that defines how to set x based on the values of the universal variables that precede x in the quantifier prefix. Winning strategies for false formulas are defined dually. In this paper, we provide a tool for validating encodings using winning strategies and interactive game play with a QBF solver. As the representation of winning strategies can get huge, we also introduce validation based on partial winning strategies. Finally, we employ winning strategies for testing if two different encodings of one problem have the same solutions.

Cite as

Irfansha Shaik, Maximilian Heisinger, Martina Seidl, and Jaco van de Pol. Validation of QBF Encodings with Winning Strategies. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 24:1-24:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{shaik_et_al:LIPIcs.SAT.2023.24,
  author =	{Shaik, Irfansha and Heisinger, Maximilian and Seidl, Martina and van de Pol, Jaco},
  title =	{{Validation of QBF Encodings with Winning Strategies}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{24:1--24:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.24},
  URN =		{urn:nbn:de:0030-drops-184863},
  doi =		{10.4230/LIPIcs.SAT.2023.24},
  annote =	{Keywords: QBF, Validation, Winning Strategy, Equivalence, Certificates}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail