Document Open Access Logo

A New Exact Solver for (Weighted) Max#SAT

Authors Gilles Audemard , Jean-Marie Lagniez , Marie Miceli

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.28.pdf
  • Filesize: 0.97 MB
  • 20 pages

Document Identifiers

Author Details

Gilles Audemard
  • CRIL, Univ. Artois & CNRS, Lens, France
Jean-Marie Lagniez
  • CRIL, Univ Artois & CNRS, Lens, France
Marie Miceli
  • CRIL, Univ Artois & CNRS, Lens, France

Funding

This work has benefited from the support of the AI Chair EXPEcolor{orange}{KC}TATION (ANR-19-CHIA-0005-01) of the French National Research Agency. It was also partially supported by TAILOR, a project funded by EU Horizon 2020 research and innovation programme under GA No 952215.

Cite AsGet BibTex

Gilles Audemard, Jean-Marie Lagniez, and Marie Miceli. A New Exact Solver for (Weighted) Max#SAT. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.28

Abstract

We present and evaluate d4Max, an exact approach for solving the Weighted Max#SAT problem. The Max#SAT problem extends the model counting problem (#SAT) by considering a tripartition of the variables {X, Y, Z}, and consists in maximizing over X the number of assignments to Y that can be extended to a solution with some assignment to Z. The Weighted Max#SAT problem is an extension of the Max#SAT problem with weights associated on each interpretation. We test and compare our approach with other state-of-the-art solvers on the challenging task in probabilistic inference of finding the marginal maximum a posteriori probability (MMAP) of a given subset of the variables in a Bayesian network and on exist-random quantified SSAT benchmarks. The results clearly show the overall superiority of d4Max in term of speed and number of instances solved. Moreover, we experimentally show that, in general, d4Max is able to quickly spot a solution that is close to optimal, thereby opening the door to an efficient anytime approach.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Search methodologies
  • Software and its engineering → Software notations and tools
Keywords
  • Max#SAT
  • EMaj-SAT
  • Weighted Projected Model Counting
  • SSAT

Metrics

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

References

  1. Handbook of Satisfiability, volume 185, 2009. Google Scholar
  2. Udi Apsel and Ronen I. Brafman. Lifted MEU by weighted model counting. In Proceedings of AAAI'12, 2012. Google Scholar
  3. Gilles Audemard, Jean-Marie Lagniez, Marie Miceli, and Olivier Roussel. Identifying soft core in propositional formulae. In Proceedings of ICAART'22, 2022. Google Scholar
  4. Peter Auer, Nicolò Cesa-Bianchi, and Paul Fischer. Finite-time analysis of the multiarmed bandit problem. Mach. Learn., 47(2-3):235-256, 2002. Google Scholar
  5. Peter Auer, Nicolò Cesa-Bianchi, Yoav Freund, and Robert E. Schapire. The nonstochastic multiarmed bandit problem. SIAM J. Comput., 32(1):48-77, 2002. Google Scholar
  6. Rehan Abdul Aziz, Geoffrey Chu, Christian J. Muise, and Peter J. Stuckey. #∃sat: Projected model counting. In Proceedings of SAT'15, volume 9340, pages 121-137, 2015. Google Scholar
  7. Anicet Bart, Frédéric Koriche, Jean-Marie Lagniez, and Pierre Marquis. Symmetry-driven decision diagrams for knowledge compilation. In Proceedings of ECAI'14, volume 263, pages 51-56, 2014. Google Scholar
  8. Anicet Bart, Frédéric Koriche, Jean-Marie Lagniez, and Pierre Marquis. An improved CNF encoding scheme for probabilistic inference. In Proceedings of ECAI'16, volume 285, pages 613-621, 2016. Google Scholar
  9. Elazar Birnbaum and Eliezer L. Lozinskii. The good old davis-putnam procedure helps counting models. J. Artif. Intell. Res., 10:457-477, 1999. Google Scholar
  10. Florent Capelli, Jean-Marie Lagniez, and Pierre Marquis. Certifying top-down decision-dnnf compilers. In Proceedings of AAAI'21, pages 6244-6253, 2021. Google Scholar
  11. Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. A scalable approximate model counter. In Proceedings of CP'13, volume 8124, pages 200-216, 2013. Google Scholar
  12. Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. Algorithmic improvements in approximate counting for probabilistic inference: From linear to logarithmic SAT calls. In Proceedings of IJCAI'16, pages 3569-3576, 2016. Google Scholar
  13. Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artif. Intell., 172(6-7):772-799, 2008. Google Scholar
  14. Mark Chavira, Adnan Darwiche, and Manfred Jaeger. Compiling relational bayesian networks for exact inference. Int. J. Approx. Reason., 42(1-2):4-20, 2006. Google Scholar
  15. Pei-Wei Chen, Yu-Ching Huang, and Jie-Hong R. Jiang. A sharp leap from quantified boolean formula to stochastic boolean satisfiability solving. In Proceedings of AAAI'21, pages 3697-3706, 2021. Google Scholar
  16. Adnan Darwiche. Decomposable negation normal form. J. ACM, 48(4):608-647, 2001. Google Scholar
  17. Adnan Darwiche. SDD: A new canonical representation of propositional knowledge bases. In Proceedings of IJCAI'11, pages 819-826, 2011. Google Scholar
  18. Adnan Darwiche and Pierre Marquis. A knowledge compilation map. J. Artif. Intell. Res., 17:229-264, 2002. Google Scholar
  19. Carmel Domshlak and Jörg Hoffmann. Fast probabilistic planning through weighted model counting. In Proceedings of ICAPS'06, pages 243-252, 2006. Google Scholar
  20. Jeffrey M. Dudek, Vu H. N. Phan, and Moshe Y. Vardi. Procount: Weighted projected model counting with graded project-join trees. In Proceedings of SAT'21, volume 12831, pages 152-170, 2021. Google Scholar
  21. Leonardo Dueñas-Osorio, Kuldeep S. Meel, Roger Paredes, and Moshe Y. Vardi. Counting-based reliability estimation for power-transmission grids. In Proceedings of AAAI'17, pages 4488-4494, 2017. Google Scholar
  22. Linus Feiten, Matthias Sauer, Tobias Schubert, Alexander Czutro, Eberhard Böhl, Ilia Polian, and Bernd Becker. #sat-based vulnerability analysis of security components - A case study. In Proceedings of DFT'12, pages 49-54, 2012. Google Scholar
  23. Daniel J. Fremont, Markus N. Rabe, and Sanjit A. Seshia. Maximum model counting. In Proceedings of AAAI'17, pages 3885-3892, 2017. Google Scholar
  24. John Gill. Computational complexity of probabilistic turing machines. SIAM J. Comput., 6(4):675-695, 1977. Google Scholar
  25. Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Near-uniform sampling of combinatorial spaces using XOR constraints. In Proceedings of NIPS'06, pages 481-488, 2006. Google Scholar
  26. Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Model counting. In Handbook of Satisfiability, volume 185, pages 633-654. IOS Press, 2009. Google Scholar
  27. Roberto J. Bayardo Jr. and Joseph Daniel Pehoushek. Counting models using connected components. In Proceedings of IAAI'00, pages 157-162, 2000. Google Scholar
  28. Kalev Kask, Rina Dechter, Javier Larrosa, and Fabio Cozman. Bucket-tree elimination for automated reasoning, 2001. Google Scholar
  29. Vladimir Klebanov, Norbert Manthey, and Christian J. Muise. Sat-based analysis and quantification of information flow in programs. In Proceedings of QEST'13, volume 8054 of Lecture Notes in Computer Science, pages 177-192, 2013. Google Scholar
  30. Tuukka Korhonen and Matti Järvisalo. Integrating tree decompositions into decision heuristics of propositional model counters (short paper). In Proceedings of CP'21, volume 210, pages 8:1-8:11, 2021. Google Scholar
  31. Frédéric Koriche, Jean-Marie Lagniez, Pierre Marquis, and Samuel Thomas. Knowledge compilation for model counting: Affine decision trees. In Proceedings of IJCAI'03, pages 947-953, 2013. Google Scholar
  32. Alexander V. Kozlov and Jaswinder Pal Singh. Computational complexity reduction for BN2O networks using similarity of states. In Proceedings of UAI'96, pages 357-364, 1996. Google Scholar
  33. Jean-Marie Lagniez and Pierre Marquis. An improved decision-dnnf compiler. In Proceedings of IJCAI'17, pages 667-673, 2017. Google Scholar
  34. Jean-Marie Lagniez and Pierre Marquis. A recursive algorithm for projected model counting. In Proceedings of AAAI'19, pages 1536-1543, 2019. Google Scholar
  35. Nian-Ze Lee, Yen-Shi Wang, and Jie-Hong R. Jiang. Solving exist-random quantified stochastic boolean satisfiability via clause selection. In Jérôme Lang, editor, Proceedings IJCAI'18, pages 1339-1345, 2018. Google Scholar
  36. Wei Li, Pascal Poupart, and Peter van Beek. Exploiting structure in weighted model counting approaches to probabilistic inference. J. Artif. Intell. Res., 40:729-765, 2011. Google Scholar
  37. Fangzhen Lin and Pierre Marquis. Causal theories of action: A computational core. In Proceedings of IJCAI'03, pages 1073-1078, 2003. Google Scholar
  38. Michael L. Littman, Judy Goldsmith, and Martin Mundhenk. The computational complexity of probabilistic planning. CoRR, 9:1-36, 1998. Google Scholar
  39. Michael L. Littman, Stephen M. Majercik, and Toniann Pitassi. Stochastic boolean satisfiability. J. Autom. Reason., 27(3):251-296, 2001. Google Scholar
  40. Sibylle Möhle and Armin Biere. Dualizing projected model counting. In Proceedings of ICTAI'18, pages 702-709, 2018. Google Scholar
  41. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of DAC'01, pages 530-535, 2001. Google Scholar
  42. Christian J. Muise, Sheila A. McIlraith, J. Christopher Beck, and Eric I. Hsu. Dsharp: Fast d-dnnf compilation with sharpsat. In Proceedings of AI'12, volume 7310, pages 356-361, 2012. Google Scholar
  43. Nina Narodytska, Aditya A. Shrotri, Kuldeep S. Meel, Alexey Ignatiev, and João Marques-Silva. Assessing heuristic machine learning explanations with model counting. In Proceedings of SAT'19, volume 11628 of Lecture Notes in Computer Science, pages 267-278, 2019. Google Scholar
  44. Héctor Palacios, Blai Bonet, Adnan Darwiche, and Hector Geffner. Pruning conformant plans by counting models on compiled d-dnnf representations. In Proceedings of ICAPS'05, pages 141-150, 2005. Google Scholar
  45. James D. Park. MAP complexity results and approximation methods. In Proceedings of UAI'02, pages 388-396, 2002. Google Scholar
  46. James D. Park and Adnan Darwiche. Solving MAP exactly using systematic search. In Proceedings of UAI'03, pages 459-468, 2003. Google Scholar
  47. James D. Park and Adnan Darwiche. Complexity results and approximation strategies for MAP explanations. J. Artif. Intell. Res., 21:101-133, 2004. Google Scholar
  48. Knot Pipatsrisawat and Adnan Darwiche. A new d-dnnf-based bound computation algorithm for functional E-MAJSAT. In Proceedings of IJCAI'09, pages 590-595, 2009. Google Scholar
  49. Daniel Russo and Benjamin Van Roy. An information-theoretic analysis of thompson sampling. J. Mach. Learn. Res., 17:68:1-68:30, 2016. Google Scholar
  50. Marko Samer and Stefan Szeider. Algorithms for propositional model counting. J. Discrete Algorithms, 8(1):50-64, 2010. Google Scholar
  51. Tian Sang, Fahiem Bacchus, Paul Beame, Henry A. Kautz, and Toniann Pitassi. Combining component caching and clause learning for effective model counting. In Proceedings of SAT'04, 2004. Google Scholar
  52. Tian Sang, Paul Beame, and Henry A. Kautz. Performing bayesian inference by weighted model counting. In Proceedings of AAAI'05, pages 475-482, 2005. Google Scholar
  53. Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. GANAK: A scalable probabilistic exact model counter. In Proceedings of IJCAI'19, pages 1169-1176, 2019. Google Scholar
  54. Mate Soos and Kuldeep S. Meel. BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In Proceedings of AAAI'19, pages 1592-1599, 2019. Google Scholar
  55. Larry J. Stockmeyer. The complexity of approximate counting (preliminary version). In Proceedings of STOC'83, pages 118-126, 1983. Google Scholar
  56. Marc Thurley. Sharpsat - counting models with advanced component caching and implicit BCP. In Proceedings of SAT'06, volume 4121, pages 424-429, 2006. Google Scholar
  57. Seinosuke Toda. PP is as hard as the polynomial-time hierarchy. SIAM J. Comput., 20(5):865-877, 1991. Google Scholar
  58. Jacobo Torán. Complexity classes defined by counting quantifiers. J. ACM, 38(3):753-774, 1991. Google Scholar
  59. Leslie G. Valiant. The complexity of enumeration and reliability problems. SIAM J. Comput., 8(3):410-421, 1979. Google Scholar
  60. Clément Viricel, David Simoncini, Sophie Barbe, and Thomas Schiex. Guaranteed weighted counting for affinity computation: Beyond determinism and structure. In Michel Rueher, editor, Proceedings ofCP'16, volume 9892 of Lecture Notes in Computer Science, pages 733-750. Springer, 2016. Google Scholar
  61. Stephan Wäldchen, Jan MacDonald, Sascha Hauch, and Gitta Kutyniok. The computational complexity of understanding binary classifier decisions. J. Artif. Intell. Res., 70:351-387, 2021. Google Scholar
  62. Jiong Yang, Supratik Chakraborty, and Kuldeep S. Meel. Projected model counting: Beyond independent support. CoRR, abs/2110.09171, 2021. Google Scholar
  63. Erik Peter Zawadzki, André Platzer, and Geoffrey J. Gordon. A generalization of SAT and #sat for robust policy evaluation. In Proceedings of IJCAI'13, pages 2583-2590, 2013. Google Scholar
  64. Hantao Zhang and Mark E. Stickel. An efficient algorithm for unit propagation. In Proceedings of AI-MATH’96, pages 166-169, 1996. 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