Document Open Access Logo

Weighted Model Counting with Twin-Width

Authors Robert Ganian , Filip Pokrývka , André Schidler, Kirill Simonov, Stefan Szeider

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.15.pdf
  • Filesize: 0.81 MB
  • 17 pages

Document Identifiers

Author Details

Robert Ganian
  • Algorithms and Complexity Group, TU Wien, Austria
Filip Pokrývka
  • Masaryk University, Brno, Czech Republic
André Schidler
  • Algorithms and Complexity Group, TU Wien, Austria
Kirill Simonov
  • Algorithms and Complexity Group, TU Wien, Austria
Stefan Szeider
  • Algorithms and Complexity Group, TU Wien, Austria

Funding

  • Ganian, Robert: support by the Austrian Science Fund (FWF, project Y1329).
  • Pokrývka, Filip: supported by the Czech Science Foundation, project no. 20-04567S.
  • Simonov, Kirill: supported by the Austrian Science Fund (FWF, projects Y1329 and P31336).
  • Szeider, Stefan: supported by the Austrian Science Fund (FWF, project P32441) and by the Vienna Science and Technology Fund (WWTF, project ICT19-065).

Acknowledgements

The authors thank Édouard Bonnet for his helpful feedback regarding the relationship between signed twin-width and planar graphs.

Cite As Get BibTex

Robert Ganian, Filip Pokrývka, André Schidler, Kirill Simonov, and Stefan Szeider. Weighted Model Counting with Twin-Width. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.SAT.2022.15

Abstract

Bonnet et al. (FOCS 2020) introduced the graph invariant twin-width and showed that many NP-hard problems are tractable for graphs of bounded twin-width, generalizing similar results for other width measures, including treewidth and clique-width. In this paper, we investigate the use of twin-width for solving the propositional satisfiability problem (SAT) and propositional model counting. We particularly focus on Bounded-ones Weighted Model Counting (BWMC), which takes as input a CNF formula F along with a bound k and asks for the weighted sum of all models with at most k positive literals. BWMC generalizes not only SAT but also (weighted) model counting.
We develop the notion of "signed" twin-width of CNF formulas and establish that BWMC is fixed-parameter tractable when parameterized by the certified signed twin-width of F plus k. We show that this result is tight: it is neither possible to drop the bound k nor use the vanilla twin-width instead if one wishes to retain fixed-parameter tractability, even for the easier problem SAT. Our theoretical results are complemented with an empirical evaluation and comparison of signed twin-width on various classes of CNF formulas.

Subject Classification

ACM Subject Classification
  • Theory of computation → Parameterized complexity and exact algorithms
Keywords
  • Weighted model counting
  • twin-width
  • parameterized complexity
  • SAT

Metrics

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

Related Versions

Supplementary Materials

References

  1. Fahiem Bacchus, Shannon Dalmao, and Toniann Pitassi. Algorithms and complexity results for #SAT and Bayesian inference. In 44th Annual IEEE Symposium on Foundations of Computer Science (FOCS'03), pages 340-351, 2003. Google Scholar
  2. Édouard Bonnet, Colin Geniet, Eun Jung Kim, Stéphan Thomassé, and Rémi Watrigant. Twin-width II: small classes. In Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms, SODA 2021, pages 1977-1996. SIAM, 2021. Google Scholar
  3. Édouard Bonnet, Colin Geniet, Eun Jung Kim, Stéphan Thomassé, and Rémi Watrigant. Twin-width III: max independent set, min dominating set, and coloring. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 35:1-35:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.35.
  4. Édouard Bonnet, Eun Jung Kim, Amadeus Reinald, and Stéphan Thomassé. Twin-width VI: the lens of contraction sequences. In Proceedings of the 2022 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 1036-1056. SIAM, 2022. Google Scholar
  5. Édouard Bonnet, Eun Jung Kim, Stéphan Thomassé, and Rémi Watrigant. Twin-width I: tractable FO model checking. In 61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020, pages 601-612. IEEE, 2020. Google Scholar
  6. Marek Cygan, Fedor V. Fomin, Łukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, MichałPilipczuk, and Saket Saurabh. Parameterized algorithms. Springer, Cham, 2015. URL: https://doi.org/10.1007/978-3-319-21275-3.
  7. Reinhard Diestel. Graph Theory, 4th Ed, volume 173 of Graduate texts in Mathematics. Springer, 2012. Google Scholar
  8. Rodney G. Downey and Michael R. Fellows. Fundamentals of parameterized complexity. Texts in Computer Science. Springer Verlag, 2013. Google Scholar
  9. Jan Dreier, Jakub Gajarskỳ, Yiting Jiang, Patrice Ossona de Mendez, and Jean-Florent Raymond. Twin-width and generalized coloring numbers. Discrete Mathematics, 345(3):112746, 2022. Google Scholar
  10. E. Fischer, J. A. Makowsky, and E. R. Ravve. Counting truth assignments of formulas of bounded tree-width or clique-width. Discr. Appl. Math., 156(4):511-529, 2008. Google Scholar
  11. Jörg Flum and Martin Grohe. Parameterized Complexity Theory, volume XIV of Texts in Theoretical Computer Science. An EATCS Series. Springer Verlag, Berlin, 2006. Google Scholar
  12. Robert Ganian, Petr Hlinený, and Jan Obdrzálek. Better algorithms for satisfiability problems for formulas of bounded rank-width. Fund. Inform., 123(1):59-76, 2013. Google Scholar
  13. Robert Ganian, M. S. Ramanujan, and Stefan Szeider. Backdoor treewidth for SAT. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10491 of Lecture Notes in Computer Science, pages 20-37. Springer Verlag, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_2.
  14. Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Model counting. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185, pages 633-654. IOS Press, 2009. Google Scholar
  15. Georg Gottlob, Francesco Scarcello, and Martha Sideri. Fixed-parameter complexity in AI and nonmonotonic reasoning. Artificial Intelligence, 138(1-2):55-86, 2002. Google Scholar
  16. Marijn Heule and Stefan Szeider. A SAT approach to clique-width. ACM Trans. Comput. Log., 16(3):24, 2015. URL: https://doi.org/10.1145/2736696.
  17. Rolf Niedermeier. Invitation to Fixed-Parameter Algorithms. Oxford Lecture Series in Mathematics and its Applications. Oxford University Press, Oxford, 2006. Google Scholar
  18. Aykut Parlak. A SAT approach to clique-width of a digraph and an application on model counting problems. Master’s thesis, TU Wien, Algorithms and Complexity Group, 2016. Google Scholar
  19. Krzysztof Pietrzak. On the parameterized complexity of the fixed alphabet shortest common supersequence and longest common subsequence problems. J. of Computer and System Sciences, 67(4):757-771, 2003. Google Scholar
  20. Dan Roth. On the hardness of approximate reasoning. Artificial Intelligence, 82(1-2):273-302, 1996. Google Scholar
  21. Sigve Hortemo Sæther, Jan Arne Telle, and Martin Vatshelle. Solving MaxSAT and #SAT on structured CNF formulas. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of Lecture Notes in Computer Science, pages 16-31. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_3.
  22. Marko Samer and Stefan Szeider. Algorithms for propositional model counting. J. Discrete Algorithms, 8(1):50-64, 2010. Google Scholar
  23. Marko Samer and Stefan Szeider. Fixed-parameter tractability. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, 2nd Edition, chapter 17, pages 693-736. IOS Press, 2021. URL: https://www.ac.tuwien.ac.at/files/tr/ac-tr-21-004.pdf.
  24. Marko Samer and Helmut Veith. Encoding treewidth into SAT. In Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, pages 45-50. Springer Verlag, 2009. Google Scholar
  25. Tian Sang, Paul Beame, and Henry A. Kautz. Performing Bayesian inference by weighted model counting. In Proceedings, The Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference, July 9-13, 2005, Pittsburgh, Pennsylvania, USA, pages 475-482. AAAI Press / The MIT Press, 2005. Google Scholar
  26. André Schidler and Stefan Szeider. A SAT approach to twin-width. In Cynthia A. Phillips and Bettina Speckmann, editors, Proceedings of ALENEX 2022, the 24nd SIAM Symposium on Algorithm Engineering and Experiments, pages 67-77. SIAM, 2022. URL: https://doi.org/10.1137/1.9781611977042.6.
  27. L. G. Valiant. The complexity of computing the permanent. Theoretical Computer Science, 8(2):189-201, 1979. 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