D
2022
Weighted Model Counting with Twin-Width
GANIAN, Robert, Filip POKRÝVKA, André SCHIDLER, Kirill SIMONOV, Stefan SZEIDER et. al.
Základní údaje
Originální název
Weighted Model Counting with Twin-Width
Autoři
GANIAN, Robert (203 Česká republika),
Filip POKRÝVKA (703 Slovensko, domácí), André SCHIDLER, Kirill SIMONOV a Stefan SZEIDER
Vydání
Dagstuhl, Germany, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022), od s. "15:1"-"15:17", 17 s. 2022
Nakladatel
Schloss Dagstuhl - Leibniz-Zentrum fur Informatik
Další údaje
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Utajení
není předmětem státního či obchodního tajemství
Forma vydání
elektronická verze "online"
Kód RIV
RIV/00216224:14330/22:00126576
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
Weighted model counting;twin-width;parameterized complexity;SAT
Příznaky
Mezinárodní význam, Recenzováno
V originále
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.
Návaznosti
GA20-04567S, projekt VaV | Název: Struktura efektivně řešitelných případů těžkých algoritmických problémů na grafech | Investor: Grantová agentura ČR, Structure of tractable instances of hard algorithmic problems on graphs |
|
MUNI/A/1145/2021, interní kód MU | Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace XI. (Akronym: SV-FI MAV XI.) | Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace XI. |
|
MUNI/A/1230/2021, interní kód MU | Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 22 (Akronym: SKOMU) | Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 22 |
|
Zobrazeno: 31. 10. 2024 14:11