Document Open Access Logo

QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas

Authors Andreas Plank , Martina Seidl

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.20.pdf
  • Filesize: 0.76 MB
  • 10 pages

Document Identifiers

Author Details

Andreas Plank
  • Johannes Kepler Universität Linz, Austria
Martina Seidl
  • Johannes Kepler Universität Linz, Austria

Funding

This work has been supported by the LIT AI Lab funded by the State of Upper Austria.

Cite AsGet BibTex

Andreas Plank and Martina Seidl. QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 20:1-20:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.20

Abstract

In this paper, we present QMusExt, a tool for the extraction of minimal unsatisfiable sets (MUS) from quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF). Our tool generalizes an efficient algorithm for MUS extraction from propositional formulas that analyses and rewrites resolution proofs generated by SAT solvers. In addition to extracting unsatisfiable cores from false formulas in PCNF, we apply QMusExt also to obtain satisfiable cores from Q-resolution proofs of true formulas in prenex disjunctive normal form (PDNF).

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Minimal Unsatisfiable Core
  • Quantified Boolean Formula

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. Nachum Dershowitz, Ziyad Hanna, and Alexander Nadel. A scalable algorithm for minimal unsatisfiable core extraction. In Proc. of the 9th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2006), volume 4121 of Lecture Notes in Computer Science, pages 36-41. Springer, 2006. URL: https://doi.org/10.1007/11814948_5.
  3. Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella. Clause/term resolution and learning in the evaluation of quantified boolean formulas. J. Artif. Intell. Res., 26:371-416, 2006. URL: https://doi.org/10.1613/jair.1959.
  4. Alexey Ignatiev, Mikolás Janota, and João Marques-Silva. Quantified maximum satisfiability. Constraints, 21(2):277-302, 2016. URL: https://doi.org/10.1007/s10601-015-9195-9.
  5. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified boolean formulas. Inf. Comput., 117(1):12-18, 1995. URL: https://doi.org/10.1006/inco.1995.1025.
  6. Hans Kleine Büning and Oliver Kullmann. Minimal unsatisfiability and autarkies. In Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 571-633. IOS Press, 2021. Google Scholar
  7. Hans Kleine Büning and Xishun Zhao. Minimal false quantified boolean formulas. In Armin Biere and Carla P. Gomes, editors, Proc. of the 9th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2006), volume 4121 of Lecture Notes in Computer Science, pages 339-352. Springer, 2006. Google Scholar
  8. Florian Lonsing and Uwe Egly. Incrementally computing minimal unsatisfiable cores of qbfs via a clause group solver API. In Proc. of the 18th Int. Conf. on Theory and Applications of Satisfiabily Testing (SAT 2015), volume 9340 of Lecture Notes in Computer Science, pages 191-198. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_14.
  9. Florian Lonsing and Uwe Egly. Depqbf 6.0: A search-based QBF solver beyond traditional QCDCL. In Proc. of the 26th Conf. on Automated Deduction (CADE 26), 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.
  10. Alexander Nadel. Boosting minimal unsatisfiable core extraction. In Proc. of 10th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD 2010), pages 221-229. IEEE, 2010. URL: https://ieeexplore.ieee.org/document/5770953/.
  11. Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, and Armin Biere. Resolution-based certificate extraction for QBF - (tool presentation). In Proc. of the 15th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2012), volume 7317 of Lecture Notes in Computer Science, pages 430-435. Springer, 2012. Google Scholar
  12. Andreas Niskanen, Jere Mustonen, Jeremias Berg, and Matti Järvisalo. Computing smallest muses of quantified boolean formulas. In Proc. of the 16th Int. Conf. on Logic Programming and Nonmonotonic Reasoning (LPNMR 2022), volume 13416 of Lecture Notes in Computer Science, pages 301-314. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15707-3_23.
  13. Yinlei Yu and Sharad Malik. Validating the result of a quantified boolean formula (QBF) solver: theory and practice. In Proc. of the 2005 Conf. on Asia South Pacific Design Automation, (ASP-DAC 2005), pages 1047-1051. ACM Press, 2005. 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 Imprint Privacy Contact