On finding short resolution refutations and small unsatisfiable subsets

DOI10.1016/j.tcs.2005.10.005zbMath1087.03035OpenAlexW2171456022WikidataQ57359981 ScholiaQ57359981MaRDI QIDQ820148

Michael R. Fellows, Stefan Szeider, Graham Wrightson

Publication date: 6 April 2006

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

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

zbMATH Keywords

parameterized complexityresolution complexity\(\text{W}[1\)-completeness]bounded local treewidthplanar formulas

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Complexity of computation (including implicit computational complexity) (03D15) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Complexity of proofs (03F20)

Related Items

Witnesses for Answer Sets of Logic Programs ⋮ Backdoors to Satisfaction ⋮ Analyzing read-once cutting plane proofs in Horn systems ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Elements of finite model theory.
• A simplified NP-complete satisfiability problem
• The intractability of resolution
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• A partial k-arboretum of graphs with bounded treewidth
• On the complexity of database queries
• A special planar satisfiability problem and a consequence of its NP- completeness
• Minimum propositional proof length is NP-hard to linearly approximate
• Deciding first-order properties of locally tree-decomposable structures
• Resolution Is Not Automatizable Unless W[P Is Tractable]
• Planar Formulae and Their Uses
• Theory and Applications of Satisfiability Testing
• On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic