On finding short resolution refutations and small unsatisfiable subsets
DOI10.1016/J.TCS.2005.10.005zbMATH Open1087.03035DBLPjournals/tcs/FellowsSW06OpenAlexW2171456022WikidataQ57359981 ScholiaQ57359981MaRDI QIDQ820148FDOQ820148
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
Recommendations
- Parameterized and Exact Computation
- On the Parameterized Complexity of Finding Small Unsatisfiable Subsets of CNF Formulas and CSP Instances
- Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas
- Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
- Efficient arbitrary and resolution proofs of unsatisfiability for restricted tree-width
parameterized complexityresolution complexity\(\text{W}[1\)-completeness]bounded local treewidthplanar formulas
Analysis of algorithms and problem complexity (68Q25) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Complexity of proofs (03F20) Complexity of computation (including implicit computational complexity) (03D15)
Cites Work
- Title not available (Why is that?)
- A partial k-arboretum of graphs with bounded treewidth
- Planar Formulae and Their Uses
- Elements of finite model theory.
- A simplified NP-complete satisfiability problem
- Title not available (Why is that?)
- Theory and Applications of Satisfiability Testing
- A special planar satisfiability problem and a consequence of its NP- completeness
- Deciding first-order properties of locally tree-decomposable structures
- Title not available (Why is that?)
- On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic
- The intractability of resolution
- Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
- Title not available (Why is that?)
- Minimum propositional proof length is NP-hard to linearly approximate
- Resolution Is Not Automatizable Unless W[P] Is Tractable
- Title not available (Why is that?)
- On the complexity of database queries
- Title not available (Why is that?)
Cited In (9)
- Characterizing Tseitin-formulas with short regular resolution refutations
- Complete inference via knowledge Petri nets and resolution rules
- Parameterized and Exact Computation
- Witnesses for Answer Sets of Logic Programs
- Contradiction separation based dynamic multi-clause synergized automated deduction
- Backdoors to Satisfaction
- Analyzing read-once cutting plane proofs in Horn systems
- NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability
- Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas
This page was built for publication: On finding short resolution refutations and small unsatisfiable subsets
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q820148)
