Please use this identifier to cite or link to this item: http://hdl.handle.net/1959.13/926729
- Title
- On finding short resolution refutations and small unsatisfiable subsets
- Author/Creator
-
Fellows, Michael R.;
Szeider, Stefan;
Wrightson, Graham
- Institution
- The University of Newcastle. Faculty of Engineering & Built Environment, School of Electrical Engineering and Computer Science
- Description
- We consider the parameterized problems of whether a given set of clauses can be refuted within k resolution steps, and whether a given set of clauses contains an unsatisfiable subset of size at most k. We show that both problems are complete for the class W[1], the first level of the W-hierarchy of fixed-parameter intractable problems. Our results remain true if restricted to 3-SAT instances and/or to various restricted versions of resolution including tree-like resolution, input resolution, and read-once resolution. Applying a metatheorem of Frick and Grohe, we show that, restricted to classes of sets of clauses of locally bounded treewidth, the considered problems are fixed-parameter tractable. For example, the problems are fixed-parameter tractable for planar CNF formulas.
- Relation
- Theoretical Computer Science Vol. 351, Issue 3, p. 351-359
- Publisher Link
- http://dx.doi.org/10.1016/j.tcs.2005.10.005
- Date
- 2006
- Publisher
- Elsevier
- Keyword(s)
-
resolution complexity;
parameterized complexity;
W[1]-completeness;
bounded local treewidth;
planar formulas
- Resource Type
- journal article
- Identifier
- http://hdl.handle.net/1959.13/926729
- Identifier
- ISSN:0304-3975
- Reviewed
12 Visitors
13 Hits
0 Downloads
