Satisfiability of acyclic and almost acyclic CNF formulas

DOI10.1016/j.tcs.2012.12.039zbMath1291.68182OpenAlexW2141898804MaRDI QIDQ385062

Daniël Paulusma, Sebastian Ordyniak, Stefan Szeider

Publication date: 29 November 2013

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2012.12.039

zbMATH Keywords

acyclic hypergraphchordal bipartite graphDavis-Putnam resolution

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Hypergraphs (05C65) Classical propositional logic (03B05) Graph algorithms (graph-theoretic aspects) (05C85)

Related Items

Tractability in constraint satisfaction problems: a survey, On Compiling CNFs into Structured Deterministic DNNFs, Model counting for CNF formulas of bounded modular treewidth, Paradigms for parameterized enumeration, Complexity and approximability of parameterized MAX-CSPs, Grundy Distinguishes Treewidth from Pathwidth, On optimization problems in acyclic hypergraphs, Are hitting formulas hard for resolution?, Unnamed Item, On the complexity of binary polynomial optimization over acyclic hypergraphs, Backdoors for linear temporal logic, New width parameters for SAT and \#SAT, Unnamed Item, Parameterized Compilation Lower Bounds for Restricted CNF-Formulas, Strong Backdoors for Default Logic, Backdoors to planning, Tractability beyond \(\beta\)-acyclicity for conjunctive queries with negation and SAT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On finding solutions for extended Horn formulas
• Hypertree decompositions and tractable queries
• Chordal deletion is fixed-parameter tractable
• A partial k-arboretum of graphs with bounded treewidth
• Efficient graph representations
• On the parameterized complexity of the fixed alphabet shortest common supersequence and longest common subsequence problems
• Upper bounds to the clique width of graphs
• Algorithms for propositional model counting
• Solving \#SAT using vertex covers
• Counting truth assignments of formulas of bounded tree-width or clique-width
• Parametrized complexity theory.
• Approximating clique-width and branch-width
• Degrees of acyclicity for hypergraphs and relational database schemes
• Simple Linear-Time Algorithms to Test Chordality of Graphs, Test Acyclicity of Hypergraphs, and Selectively Reduce Acyclic Hypergraphs
• Graph Classes: A Survey
• Hypergraphs in Model Checking: Acyclicity and Hypertree-Width versus Clique-Width
• A Computing Procedure for Quantification Theory
• On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic