On finding short resolution refutations and small unsatisfiable subsets
DOI10.1016/J.TCS.2005.10.005zbMATH Open1087.03035DBLPjournals/tcs/FellowsSW06OpenAlexW2171456022WikidataQ57359981 ScholiaQ57359981MaRDI QIDQ820148FDOQ820148
Authors: 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
- scientific article; zbMATH DE number 1324669 (Why is no real title available?)
- scientific article; zbMATH DE number 1161563 (Why is no real title available?)
- scientific article; zbMATH DE number 1361489 (Why is no real title available?)
- scientific article; zbMATH DE number 953683 (Why is no real title available?)
- scientific article; zbMATH DE number 1860652 (Why is no real title available?)
- scientific article; zbMATH DE number 3313427 (Why is no real title available?)
- A partial k-arboretum of graphs with bounded treewidth
- A simplified NP-complete satisfiability problem
- A special planar satisfiability problem and a consequence of its NP- completeness
- Deciding first-order properties of locally tree-decomposable structures
- Elements of finite model theory.
- Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
- Minimum propositional proof length is NP-hard to linearly approximate
- On the complexity of database queries
- On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic
- Planar Formulae and Their Uses
- Resolution Is Not Automatizable Unless W[P] Is Tractable
- The intractability of resolution
- Theory and Applications of Satisfiability Testing
Cited In (12)
- Characterizing Tseitin-formulas with short regular resolution refutations
- Complete inference via knowledge Petri nets and resolution rules
- An upper bound for resolution size: characterization of tractable SAT instances
- Parameterized and Exact Computation
- Backdoors to satisfaction
- Witnesses for Answer Sets of Logic Programs
- Contradiction separation based dynamic multi-clause synergized automated deduction
- 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
- Efficient arbitrary and resolution proofs of unsatisfiability for restricted tree-width
- Parameterized proof complexity
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)
