Document Open Access Logo

Dynamic Blocked Clause Elimination for Projected Model Counting

Authors Jean-Marie Lagniez , Pierre Marquis , Armin Biere

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.21.pdf
  • Filesize: 0.85 MB
  • 17 pages

Document Identifiers

Author Details

Jean-Marie Lagniez
  • Univ. Artois, CNRS, CRIL, France
Pierre Marquis
  • Univ. Artois, CNRS, CRIL, IUF, France
Armin Biere
  • University Freiburg, Germany

Funding

This work has benefited from the support of the AI Chair EXPEKCTATION (ANR-19-CHIA-0005-01) of the French National Research Agency.

Cite AsGet BibTex

Jean-Marie Lagniez, Pierre Marquis, and Armin Biere. Dynamic Blocked Clause Elimination for Projected Model Counting. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.SAT.2024.21

Abstract

In this paper, we explore the application of blocked clause elimination for projected model counting. This is the problem of determining the number of models ‖∃ X . Σ‖ of a propositional formula Σ after eliminating a given set X of variables existentially. Although blocked clause elimination is a well-known technique for SAT solving, its direct application to model counting is challenging as in general it changes the number of models. However, we demonstrate, by focusing on projected variables during the blocked clause search, that blocked clause elimination can be leveraged while preserving the correct model count. To take advantage of blocked clause elimination in an efficient way during model counting, a novel data structure and associated algorithms are introduced. Our proposed approach is implemented in the model counter d4. Our experiments demonstrate the computational benefits of our new method of blocked clause elimination for projected model counting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Projected model counting
  • blocked clause elimination
  • propositional logic

Metrics

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

Supplementary Materials

References

  1. Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of Databases. Addison-Wesley, 1995. URL: http://webdam.inria.fr/Alice/.
  2. Gilles Audemard, Jean-Marie Lagniez, and Marie Miceli. A new exact solver for (weighted) max#sat. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 of LIPIcs, pages 28:1-28:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.SAT.2022.28.
  3. Gilles Audemard, Jean-Marie Lagniez, Marie Miceli, and Olivier Roussel. Identifying soft cores in propositional formulæ. In Ana Paula Rocha, Luc Steels, and H. Jaap van den Herik, editors, Proceedings of the 14th International Conference on Agents and Artificial Intelligence, ICAART 2022, Volume 2, Online Streaming, February 3-5, 2022, pages 486-495. SCITEPRESS, 2022. URL: https://doi.org/10.5220/0010892700003116.
  4. Rehan Abdul Aziz, Geoffrey Chu, Christian J. Muise, and Peter J. Stuckey. #∃sat: Projected model counting. In Marijn Heule and Sean A. Weaver, editors, Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, volume 9340 of Lecture Notes in Computer Science, pages 121-137. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_10.
  5. Lee A. Barnett, David M. Cerna, and Armin Biere. Covered clauses are not propagation redundant. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, volume 12166 of Lecture Notes in Computer Science, pages 32-47. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51074-9_3.
  6. Armin Biere, Matti Järvisalo, and Benjamin Kiesl. Preprocessing in SAT solving. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 391-435. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200992.
  7. Jeffrey M. Dudek, Vu Phan, and Moshe Y. Vardi. ADDMC: weighted model counting with algebraic decision diagrams. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pages 1468-1476. AAAI Press, 2020. URL: https://doi.org/10.1609/AAAI.V34I02.5505.
  8. Jeffrey M. Dudek, Vu H. N. Phan, and Moshe Y. Vardi. DPMC: weighted model counting by dynamic programming on project-join trees. In Helmut Simonis, editor, Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedings, volume 12333 of Lecture Notes in Computer Science, pages 211-230. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_13.
  9. Johannes Klaus Fichte, Markus Hecher, Michael Morak, Patrick Thier, and Stefan Woltran. Solving projected model counting by utilizing treewidth and its limits. Artif. Intell., 314:103810, 2023. URL: https://doi.org/10.1016/J.ARTINT.2022.103810.
  10. Markus Hecher, Patrick Thier, and Stefan Woltran. Taming high treewidth with abstraction, nested dynamic programming, and database technology. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 343-360. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_25.
  11. Marijn Heule, Matti Järvisalo, and Armin Biere. Covered clause elimination. In Andrei Voronkov, Geoff Sutcliffe, Matthias Baaz, and Christian G. Fermüller, editors, Short papers for 17th International Conference on Logic for Programming, Artificial intelligence, and Reasoning, LPAR-17-short, Yogyakarta, Indonesia, October 10-15, 2010, volume 13 of EPiC Series in Computing, pages 41-46. EasyChair, 2010. URL: https://doi.org/10.29007/CL8S.
  12. Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, and Armin Biere. Clause elimination for SAT and QSAT. J. Artif. Intell. Res., 53:127-168, 2015. URL: https://doi.org/10.1613/JAIR.4694.
  13. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. J. Autom. Reason., 64(3):533-554, 2020. URL: https://doi.org/10.1007/S10817-019-09516-0.
  14. Marijn J. H. Heule and Hans van Maaren. Look-ahead based SAT solvers. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 183-212. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200988.
  15. Matti Järvisalo, Armin Biere, and Marijn Heule. Blocked clause elimination. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 129-144. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_10.
  16. Matti Järvisalo, Armin Biere, and Marijn Heule. Simulating circuit-level simplifications on CNF. J. Autom. Reason., 49(4):583-619, 2012. URL: https://doi.org/10.1007/S10817-011-9239-9.
  17. Matti Järvisalo, Marijn Heule, and Armin Biere. Inprocessing rules. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, volume 7364 of Lecture Notes in Computer Science, pages 355-370. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31365-3_28.
  18. Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, and Armin Biere. Blocked clauses in first-order logic. In Thomas Eiter and David Sands, editors, LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46 of EPiC Series in Computing, pages 31-48. EasyChair, 2017. URL: https://doi.org/10.29007/C3WQ.
  19. Vladimir Klebanov, Norbert Manthey, and Christian J. Muise. Sat-based analysis and quantification of information flow in programs. In Kaustubh R. Joshi, Markus Siegle, Mariëlle Stoelinga, and Pedro R. D'Argenio, editors, Quantitative Evaluation of Systems - 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, volume 8054 of Lecture Notes in Computer Science, pages 177-192. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40196-1_16.
  20. Oliver Kullmann. On a generalization of extended resolution. Discret. Appl. Math., 96-97:149-176, 1999. URL: https://doi.org/10.1016/S0166-218X(99)00037-2.
  21. Jean-Marie Lagniez, Florent Capelli, Andreas Plank, and Martina Seidl. A top-down tree model counter for quantified boolean formulas. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, 3rd-9th August 2024, Jeju, South Korea. ijcai.org, 2024. Google Scholar
  22. Jean-Marie Lagniez, Emmanuel Lonca, and Pierre Marquis. Definability for model counting. Artif. Intell., 281:103229, 2020. URL: https://doi.org/10.1016/J.ARTINT.2019.103229.
  23. Jean-Marie Lagniez and Pierre Marquis. Preprocessing for propositional model counting. In Carla E. Brodley and Peter Stone, editors, Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27 -31, 2014, Québec City, Québec, Canada, pages 2688-2694. AAAI Press, 2014. URL: https://doi.org/10.1609/AAAI.V28I1.9116.
  24. Jean-Marie Lagniez and Pierre Marquis. An improved decision-dnnf compiler. In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 667-673. ijcai.org, 2017. URL: https://doi.org/10.24963/IJCAI.2017/93.
  25. Jean-Marie Lagniez and Pierre Marquis. On preprocessing techniques and their impact on propositional model counting. J. Autom. Reason., 58(4):413-481, 2017. URL: https://doi.org/10.1007/S10817-016-9370-8.
  26. Jean-Marie Lagniez and Pierre Marquis. A recursive algorithm for projected model counting. In The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2019, Honolulu, Hawaii, USA, January 27 - February 1, 2019, pages 1536-1543. AAAI Press, 2019. URL: https://doi.org/10.1609/AAAI.V33I01.33011536.
  27. Jean-Marie Lagniez and Pierre Marquis. Boosting definability bipartition computation using SAT witnesses. In Sarah Alice Gaggl, Maria Vanina Martinez, and Magdalena Ortiz, editors, Logics in Artificial Intelligence - 18th European Conference, JELIA 2023, Dresden, Germany, September 20-22, 2023, Proceedings, volume 14281 of Lecture Notes in Computer Science, pages 697-711. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-43619-2_47.
  28. Jérôme Lang, Paolo Liberatore, and Pierre Marquis. Propositional independence: Formula-variable independence and forgetting. J. Artif. Intell. Res., 18:391-443, 2003. URL: https://doi.org/10.1613/JAIR.1113.
  29. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001, pages 530-535. ACM, 2001. URL: https://doi.org/10.1145/378239.379017.
  30. Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. GANAK: A scalable probabilistic exact model counter. In Sarit Kraus, editor, Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 1169-1176. ijcai.org, 2019. URL: https://doi.org/10.24963/IJCAI.2019/163.
  31. Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, and Bernd Becker. Preprocessing for DQBF. In Marijn Heule and Sean A. Weaver, editors, Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, volume 9340 of Lecture Notes in Computer Science, pages 173-190. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_13.
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