Informace o publikaci
New Width Parameters for Model Counting
| Autoři | |
|---|---|
| Rok publikování | 2017 |
| Druh | Článek ve sborníku |
| Konference | Theory and Applications of Satisfiability Testing - {SAT} 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings |
| Fakulta / Pracoviště MU | |
| Citace | |
| www | https://link.springer.com/chapter/10.1007/978-3-319-66263-3_3#citeas |
| Doi | http://dx.doi.org/10.1007/978-3-319-66263-3_3 |
| Klíčová slova | Treewidth; Model Counting; SAT; Parameterized Complexity |
| Popis | 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. |