Weighted Model Counting with Twin-Width

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

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

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

ISBN

978-3-95977-242-6

ISSN

DOI

http://dx.doi.org/10.4230/LIPIcs.SAT.2022.15

Klíčová slova anglicky

Weighted model counting;twin-width;parameterized complexity;SAT

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 28. 3. 2023 11:54, RNDr. Pavel Šmerk, Ph.D.

Anotace

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

Citovat

GANIAN, Robert, Filip POKRÝVKA, André SCHIDLER, Kirill SIMONOV a Stefan SZEIDER. Weighted Model Counting with Twin-Width. Online. In Meel, Kuldeep S. and Strichman, Ofer. 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum fur Informatik, 2022, s. "15:1"-"15:17", 17 s. ISBN 978-3-95977-242-6. Dostupné z: https://dx.doi.org/10.4230/LIPIcs.SAT.2022.15.

@inproceedings{2215105,
   author = {Ganian, Robert and Pokrývka, Filip and Schidler, André and Simonov, Kirill and Szeider, Stefan},
   address = {Dagstuhl, Germany},
   booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
   doi = {http://dx.doi.org/10.4230/LIPIcs.SAT.2022.15},
   editor = {Meel, Kuldeep S. and Strichman, Ofer},
   keywords = {Weighted model counting;twin-width;parameterized complexity;SAT},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Dagstuhl, Germany},
   isbn = {978-3-95977-242-6},
   pages = {"15:1"-"15:17"},
   publisher = {Schloss Dagstuhl - Leibniz-Zentrum fur Informatik},
   title = {Weighted Model Counting with Twin-Width},
   year = {2022}
}

TY  - JOUR
ID  - 2215105
AU  - Ganian, Robert - Pokrývka, Filip - Schidler, André - Simonov, Kirill - Szeider, Stefan
PY  - 2022
TI  - Weighted Model Counting with Twin-Width
PB  - Schloss Dagstuhl - Leibniz-Zentrum fur Informatik
CY  - Dagstuhl, Germany
SN  - 9783959772426
KW  - Weighted model counting;twin-width;parameterized complexity;SAT
N2  - 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.
ER  -

GANIAN, Robert, Filip POKRÝVKA, André SCHIDLER, Kirill SIMONOV a Stefan SZEIDER. Weighted Model Counting with Twin-Width. Online. In Meel, Kuldeep S. and Strichman, Ofer. \textit{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}. Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum fur Informatik, 2022, s.~''15:1''-''15:17'', 17 s. ISBN~978-3-95977-242-6. Dostupné z: https://dx.doi.org/10.4230/LIPIcs.SAT.2022.15.

Podrobný výpis o publikaci