New Width Parameters for Model Counting

被引:8
|
作者
Ganian, Robert [1 ,2 ]
Szeider, Stefan [1 ]
机构
[1] TU Wien, Algorithms & Complex Grp, Vienna, Austria
[2] FI MU, Brno, Czech Republic
来源
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING (SAT 2017) | 2017年 / 10491卷
基金
奥地利科学基金会;
关键词
SOLVING NUMBER-SAT; ALGORITHMS; SATISFIABILITY; COMPLEXITY; CONFLICTS;
D O I
10.1007/978-3-319-66263-3_3
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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.
引用
收藏
页码:38 / 52
页数:15
相关论文
共 50 条
  • [21] Equivalence Checking of Quantum Circuits by Model Counting
    Mei, Jingyi
    Coopmans, Tim
    Bonsangue, Marcello
    Laarman, Alfons
    AUTOMATED REASONING, IJCAR 2024, PT II, 2024, 14740 : 401 - 421
  • [22] Integer Representation and Counting in the Bit Probe Model
    Rahman, M. Ziaur
    Munro, J. Ian
    ALGORITHMICA, 2010, 56 (01) : 105 - 127
  • [23] Model counting with error-correcting codes
    Dimitris Achlioptas
    Panos Theodoropoulos
    Constraints, 2019, 24 : 162 - 182
  • [24] Learning Branching Heuristics for Propositional Model Counting
    Vaezipoor, Pashootan
    Lederman, Gil
    Wu, Yuhuai
    Maddison, Chris
    Grosse, Roger B.
    Seshia, Sanjit A.
    Bacchus, Fahiem
    THIRTY-FIFTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, THIRTY-THIRD CONFERENCE ON INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE AND THE ELEVENTH SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2021, 35 : 12427 - 12435
  • [25] How Hard Is Counting Triangles in the Streaming Model?
    Braverman, Vladimir
    Ostrovsky, Rafail
    Vilenchik, Dan
    AUTOMATA, LANGUAGES, AND PROGRAMMING, PT I, 2013, 7965 : 244 - 254
  • [26] Model Counting for CNF Formulas of Bounded Modular Treewidth
    Daniel Paulusma
    Friedrich Slivovsky
    Stefan Szeider
    Algorithmica, 2016, 76 : 168 - 194
  • [27] Exploiting Treewidth for Projected Model Counting and Its Limits
    Fichte, Johannes K.
    Hecher, Markus
    Morak, Michael
    Woltran, Stefan
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2018, 2018, 10929 : 165 - 184
  • [28] Hardness of computing width parameters based on branch decompositions over the vertex set
    Saether, Sigve Hortemo
    Vatshelle, Martin
    THEORETICAL COMPUTER SCIENCE, 2016, 615 : 120 - 125
  • [29] The Complexity of Counting Cycles in the Adjacency List Streaming Model
    Kallaugher, John
    McGregor, Andrew
    Price, Eric
    Vorotnikova, Sofya
    PROCEEDINGS OF THE 38TH ACM SIGMOD-SIGACT-SIGAI SYMPOSIUM ON PRINCIPLES OF DATABASE SYSTEMS (PODS '19), 2019, : 119 - 133
  • [30] Understanding Model Counting for β-acyclic CNF-formulas
    Brault-Baron, Johann
    Capelli, Florent
    Mengel, Stefan
    32ND INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE (STACS 2015), 2015, 30 : 143 - 156