Document Open Access Logo

Validation of QBF Encodings with Winning Strategies

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

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.24.pdf
  • Filesize: 0.62 MB
  • 10 pages

Document Identifiers

Author Details

Irfansha Shaik
  • Aarhus University, Denmark
Maximilian Heisinger
  • Johannes Kepler Universität Linz, Austria
Martina Seidl
  • Johannes Kepler Universität Linz, Austria
Jaco van de Pol
  • Aarhus University, Denmark

Funding

  • Heisinger, Maximilian: Supported by the LIT AI Lab funded by the State of Upper Austria.
  • Seidl, Martina: Supported by the LIT AI Lab funded by the State of Upper Austria.

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.SAT.2023.24

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.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Artificial intelligence
  • Theory of computation → Logic and verification
Keywords
  • QBF
  • Validation
  • Winning Strategy
  • Equivalence
  • Certificates

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Formal Methods Syst. Des., 41(1):45-65, 2012. URL: https://doi.org/10.1007/s10703-012-0152-6.
  2. Marco Benedetti. Extracting certificates from quantified boolean formulas. In Proc. of the 19th International Joint Conference on Artificial Intelligence (IJCAI), pages 47-53. Professional Book Center, 2005. URL: http://ijcai.org/Proceedings/05/Papers/0985.pdf.
  3. Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, and Martina Seidl. Quantified Boolean Formulas. In Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 1177-1221. IOS Press, 2021. Google Scholar
  4. Roderick Bloem, Vedad Hadzic, Ankit Shukla, and Martina Seidl. Ferpmodels: A certification framework for expansion-based qbf solving. In Proc. of the International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) 2022, September 2022. Google Scholar
  5. Robert Brummayer, Florian Lonsing, and Armin Biere. Automated testing and debugging of SAT and QBF solvers. In Proc. of the 13th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2010), volume 6175 of Lecture Notes in Computer Science, pages 44-57. Springer, 2010. Google Scholar
  6. Alexandra Goultiaeva, Allen Van Gelder, and Fahiem Bacchus. A uniform approach for generating proofs and strategies for both true and false QBF formulas. In Proc. of the 22nd International Joint Conference on Artificial Intelligence (IJCAI 2011), pages 546-553. IJCAI/AAAI, 2011. Google Scholar
  7. Ryan B. Hayward and Bjarne Toft. Hex, the full story. AK Peters/CRC Press/Taylor Francis, 2019. Google Scholar
  8. Jesko Hecking-Harbusch and Leander Tentrup. Solving QBF by abstraction. In Proc. of the 9th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF), volume 277 of EPTCS, pages 88-102, 2018. URL: https://doi.org/10.4204/EPTCS.277.7.
  9. Charles Jordan, Will Klieber, and Martina Seidl. Non-CNF QBF solving with QCIR. In AAAI-16 Workshop on Beyond NP, February 2016. Google Scholar
  10. Florian Lonsing and Uwe Egly. Depqbf 6.0: A search-based QBF solver beyond traditional QCDCL. In CADE, volume 10395 of Lecture Notes in Computer Science, pages 371-384. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_23.
  11. Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, and Armin Biere. Resolution-based certificate extraction for QBF. In Proc. of the 15th Int. Conf. on the Theory and Applications of Satisfiability Testing (SAT), volume 7317 of Lecture Notes in Computer Science, pages 430-435. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_33.
  12. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Polynomial-time validation of QCDCL certificates. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Proc. of the 21st Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2018), volume 10929 of Lecture Notes in Computer Science, pages 253-269. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_16.
  13. Luca Pulina and Martina Seidl. The 2016 and 2017 QBF solvers evaluations (qbfeval'16 and qbfeval'17). Artif. Intell., 274:224-248, 2019. URL: https://doi.org/10.1016/j.artint.2019.04.002.
  14. Markus N. Rabe and Leander Tentrup. CAQE: A certifying QBF solver. In FMCAD, pages 136-143. IEEE, 2015. URL: https://www.react.uni-saarland.de/publications/RT15.pdf.
  15. Irfansha Shaik, Valentin Mayer-Eichberger, Jaco van de Pol, and Abdallah Saffidine. Implicit state and goals in QBF encodings for positional games (extended version). CoRR, abs/2301.07345, 2023. URL: https://doi.org/10.48550/arXiv.2301.07345.
  16. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A Survey on Applications of Quantified Boolean Formulas. In Proc. of the 31st IEEE International Conference on Tools with Artificial Intelligence (ICTAI), pages 78-84. IEEE, 2019. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact