2026-08-16T22:48:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16689 2024-03-06T10:58:03Z ddc:004 open_access

Weighted Model Counting with Twin-Width Ganian, Robert Pokrývka, Filip Schidler, André Simonov, Kirill Szeider, Stefan Weighted model counting twin-width parameterized complexity SAT 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Robert Ganian and Filip Pokrývka and André Schidler and Kirill Simonov and Stefan Szeider 2022 Is Part Of LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2022.15 urn:nbn:de:0030-drops-166896 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.15 eng https://creativecommons.org/licenses/by/4.0/legalcode