Weighted Model Counting with Twin-Width
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F22%3A00126576" target="_blank" >RIV/00216224:14330/22:00126576 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.4230/LIPIcs.SAT.2022.15" target="_blank" >http://dx.doi.org/10.4230/LIPIcs.SAT.2022.15</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.4230/LIPIcs.SAT.2022.15" target="_blank" >10.4230/LIPIcs.SAT.2022.15</a>
Alternative languages
Result language
angličtina
Original language name
Weighted Model Counting with Twin-Width
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA20-04567S" target="_blank" >GA20-04567S: Structure of tractable instances of hard algorithmic problems on graphs</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2022
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
ISBN
9783959772426
ISSN
1868-8969
e-ISSN
—
Number of pages
17
Pages from-to
„15:1“-„15:17“
Publisher name
Schloss Dagstuhl - Leibniz-Zentrum fur Informatik
Place of publication
Dagstuhl, Germany
Event location
Dagstuhl, Germany
Event date
Jan 1, 2022
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—