Document Open Access Logo

Pedant: A Certifying DQBF Solver

Authors Franz-Xaver Reichl, Friedrich Slivovsky

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.20.pdf
  • Filesize: 0.58 MB
  • 10 pages

Document Identifiers

Author Details

Franz-Xaver Reichl
  • TU Wien, Austria
Friedrich Slivovsky
  • TU Wien, Austria

Funding

Supported by the Vienna Science and Technology Fund (WWTF) under grant ICT19-060, and the Austrian Science Fund (FWF) under grant W1255.

Cite As Get BibTex

Franz-Xaver Reichl and Friedrich Slivovsky. Pedant: A Certifying DQBF Solver. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 20:1-20:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.SAT.2022.20

Abstract

Pedant is a solver for Dependency Quantified Boolean Formulas (DQBF) that combines propositional definition extraction with Counterexample-Guided Inductive Synthesis (CEGIS) to compute a model of a given formula. Pedant 2 improves upon an earlier version in several ways. We extend the notion of dependencies by allowing existential variables to depend on other existential variables. This leads to more and smaller definitions, as well as more concise repairs for counterexamples. Additionally, we reduce counterexamples by determining minimal separators in a conflict graph, and use decision tree learning to obtain default functions for undetermined variables. An experimental evaluation on standard benchmarks showed a significant increase in the number of solved instances compared to the previous version of our solver.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • DQBF
  • DQBF Solver
  • Decision Procedure
  • Certificates

Metrics

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

Supplementary Materials

References

  1. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In Craig Boutilier, editor, IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, pages 399-404, 2009. Google Scholar
  2. Armin Biere. PicoSAT Essentials. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 4(2-4):75-97, 2008. URL: https://doi.org/10.3233/sat190039.
  3. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pages 51-53. University of Helsinki, 2020. Google Scholar
  4. Armin Biere, Keijo Heljanko, and Siert Wieringa. AIGER 1.9 and beyond. Technical Report 11/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria, 2011. Google Scholar
  5. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009. Google Scholar
  6. Yuri Boykov and Vladimir Kolmogorov. An experimental comparison of min-cut/max-flow algorithms for energy minimization in vision. IEEE Transactions on Pattern Analysis and Machine Intelligence, 26:1124-1137, September 2004. URL: http://www.csd.uwo.ca/~yuri/Abstracts/pami04-abs.shtml.
  7. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, pages 502-518, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  8. Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe, and Leander Tentrup. Encodings of bounded synthesis. In Axel Legay and Tiziana Margaria, editors, Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, volume 10205 of Lecture Notes in Computer Science, pages 354-370, 2017. Google Scholar
  9. Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda. SAT competition 2020. Artificial Intelligence, 301:103572, 2021. URL: https://doi.org/10.1016/j.artint.2021.103572.
  10. Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, and Bernd Becker. Equivalence checking of partial designs using dependency quantified Boolean formulae. In IEEE 31st International Conference on Computer Design, ICCD 2013,, pages 396-403. IEEE Computer Society, 2013. Google Scholar
  11. Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, and Bernd Becker. Solving DQBF through quantifier elimination. In Wolfgang Nebel and David Atienza, editors, Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, DATE 2015, pages 1617-1622. ACM, 2015. Google Scholar
  12. Priyanka Golia, Subhajit Roy, and Kuldeep S. Meel. Manthan: A data-driven approach for Boolean function synthesis. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, volume 12225 of Lecture Notes in Computer Science, pages 611-633. Springer, 2020. Google Scholar
  13. Marijn J. H. Heule, Matti Järvisalo, and Martin Suda. SAT competition 2018. J. Satisf. Boolean Model. Comput., 11(1):133-154, 2019. Google Scholar
  14. Marijn J.H. Heule, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Race 2019: Solver and Benchmark Descriptions, volume B-2019-1 of Department of Computer Science Report Series B. Department of Computer Science, University of Helsinki, Finland, 2019. Google Scholar
  15. Geoff Hulten, Laurie Spencer, and Pedro Domingos. Mining time-changing data streams. In Proceedings of the Seventh ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD '01, pages 97-106, New York, NY, USA, 2001. Association for Computing Machinery. URL: https://doi.org/10.1145/502512.502529.
  16. Susmit Jha and Sanjit A. Seshia. A theory of formal synthesis via inductive learning. Acta Informatica, 54(7):693-726, 2017. Google Scholar
  17. Daniel Kroening. Software verification. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, chapter 16, pages 505-532. IOS Press, Amsterdam, 2009. Google Scholar
  18. Jérôme Lang and Pierre Marquis. On propositional definability. Artif. Intell., 172(8-9):991-1017, 2008. URL: https://doi.org/10.1016/j.artint.2007.12.003.
  19. G. Peterson, J. Reif, and S. Azhar. Lower bounds for multiplayer noncooperative games of incomplete information. Computers & Mathematics with Applications, 41(7):957-992, 2001. Google Scholar
  20. Luca Pulina and Martina Seidl. The 2016 and 2017 QBF solvers evaluations (qbfeval'16 and qbfeval'17). Artif. Intell., 274:224-248, 2019. Google Scholar
  21. Markus N. Rabe. A resolution-style proof system for DQBF. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017, volume 10491 of Lecture Notes in Computer Science, pages 314-325. Springer, 2017. Google Scholar
  22. Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider. Certified DQBF solving by definition extraction. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021, pages 499-517, Cham, 2021. Springer International Publishing. Google Scholar
  23. Jussi Rintanen. Planning and sat. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, chapter 15, pages 483-504. IOS Press, Amsterdam, 2009. Google Scholar
  24. Olivier Roussel. Controlling a solver execution with the runsolver tool. J. Satisf. Boolean Model. Comput., 7(4):139-144, 2011. Google Scholar
  25. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified Boolean formulas. In ICTAI, pages 78-84. IEEE, 2019. Google Scholar
  26. Juraj Síč. Satisfiability of DQBF using binary decision diagrams. Master’s thesis, Masaryk University, Brno, Czech Republic, 2020. Google Scholar
  27. Friedrich Slivovsky. Interpolation-based semantic gate extraction and its applications to QBF preprocessing. In CAV (1), volume 12224 of Lecture Notes in Computer Science, pages 508-528. Springer, 2020. Google Scholar
  28. Friedrich Slivovsky and Stefan Szeider. Soundness of Q-resolution with dependency schemes. Theor. Comput. Sci., 612:83-101, 2016. Google Scholar
  29. Armando Solar-Lezama, Christopher Grant Jones, and Rastislav Bodík. Sketching concurrent data structures. In Rajiv Gupta and Saman P. Amarasinghe, editors, Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, pages 136-148. ACM, 2008. Google Scholar
  30. Armando Solar-Lezama, Liviu Tancau, Rastislav Bodík, Sanjit A. Seshia, and Vijay A. Saraswat. Combinatorial sketching for finite programs. In John Paul Shen and Margaret Martonosi, editors, Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006, pages 404-415. ACM, 2006. Google Scholar
  31. Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time: Preliminary report. In Alfred V. Aho, Allan Borodin, Robert L. Constable, Robert W. Floyd, Michael A. Harrison, Richard M. Karp, and H. Raymond Strong, editors, Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA, pages 1-9. ACM, 1973. Google Scholar
  32. Yakir Vizel, Georg Weissenbacher, and Sharad Malik. Boolean satisfiability solvers and their applications in model checking. Proc. IEEE, 103(11):2021-2035, 2015. Google Scholar
  33. Ralf Wimmer, Christoph Scholl, Karina Wimmer, and Bernd Becker. Dependency schemes for DQBF. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016, volume 9710 of Lecture Notes in Computer Science, pages 473-489. Springer, 2016. 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