New Width Parameters for Model Counting

D 2017

New Width Parameters for Model Counting

GANIAN, Robert a Stefan SZEIDER

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

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"

Odkazy

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

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ěněno: 28. 4. 2020 12:17, Mgr. Michal Petr

Anotace

V originále

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.

Citovat

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.

@inproceedings{1414045,
   author = {Ganian, Robert and Szeider, Stefan},
   address = {Nemecko},
   booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings},
   doi = {http://dx.doi.org/10.1007/978-3-319-66263-3_3},
   editor = {Serge Gaspers and Toby Walsh},
   keywords = {Treewidth; Model Counting; SAT; Parameterized Complexity},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Nemecko},
   isbn = {978-3-319-66262-6},
   pages = {38-52},
   publisher = {Springer},
   title = {New Width Parameters for Model Counting},
   url = {https://link.springer.com/chapter/10.1007/978-3-319-66263-3_3#citeas},
   year = {2017}
}

TY  - JOUR
ID  - 1414045
AU  - Ganian, Robert - Szeider, Stefan
PY  - 2017
TI  - New Width Parameters for Model Counting
PB  - Springer
CY  - Nemecko
SN  - 9783319662626
KW  - Treewidth
KW  - Model Counting
KW  - SAT
KW  - Parameterized Complexity
UR  - https://link.springer.com/chapter/10.1007/978-3-319-66263-3_3#citeas
L2  - https://link.springer.com/chapter/10.1007/978-3-319-66263-3_3#citeas
N2  - 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.
ER  -

GANIAN, Robert a Stefan SZEIDER. New Width Parameters for Model Counting. Online. In Serge Gaspers and Toby Walsh. \textit{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.

Podrobný výpis o publikaci