GANIAN, Robert a Stefan SZEIDER. New Width Parameters for Model Counting. Online. In Serge Gaspers and Toby Walsh. Theory and Applications of Satisfiability Testing - {SAT} 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings. Nemecko: Springer, 2017, s. 38-52. ISBN 978-3-319-66262-6. Dostupné z: https://dx.doi.org/10.1007/978-3-319-66263-3_3.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název New Width Parameters for Model Counting
Autoři GANIAN, Robert (203 Česká republika, garant, domácí) a Stefan SZEIDER (40 Rakousko).
Vydání Nemecko, Theory and Applications of Satisfiability Testing - {SAT} 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, od s. 38-52, 15 s. 2017.
Nakladatel Springer
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10200 1.2 Computer and information sciences
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
Forma vydání elektronická verze "online"
WWW URL
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/17:00100552
Organizační jednotka Fakulta informatiky
ISBN 978-3-319-66262-6
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-66263-3_3
UT WoS 000455337600003
Klíčová slova anglicky Treewidth; Model Counting; SAT; Parameterized Complexity
Štítky core_A, firank_A
Změnil Změnil: Mgr. Michal Petr, učo 65024. Změněno: 28. 4. 2020 12:17.
Anotace
We study the parameterized complexity of the propositional model counting problem #SAT for CNF formulas. As the parameter we consider the treewidth of the following two graphs associated with CNF formulas: the consensus graph and the conflict graph. Both graphs have as vertices the clauses of the formula; in the consensus graph two clauses are adjacent if they do not contain a complementary pair of literals, while in the conflict graph two clauses are adjacent if they do contain a complementary pair of literals. We show that #SAT is fixed-parameter tractable for the treewidth of the consensus graph but W[1]-hard for the treewidth of the conflict graph. We also compare the new parameters with known parameters under which #SAT is fixed-parameter tractable.
VytisknoutZobrazeno: 4. 5. 2024 00:55