- Title
- On finding short resolution refutations and small unsatisfiable subsets
- Creator
- Fellows, Michael R.; Szeider, Stefan; Wrightson, Graham
- Relation
- Theoretical Computer Science Vol. 351, Issue 3, p. 351-359
- Publisher Link
- http://dx.doi.org/10.1016/j.tcs.2005.10.005
- Publisher
- Elsevier
- Resource Type
- journal article
- Date
- 2006
- 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.
- Subject
- resolution complexity; parameterized complexity; W[1]-completeness; bounded local treewidth; planar formulas
- Identifier
- http://hdl.handle.net/1959.13/926729
- Identifier
- uon:9924
- Identifier
- ISSN:0304-3975
- Language
- eng
- Reviewed
- Hits: 2210
- Visitors: 2168
- Downloads: 0
Thumbnail | File | Description | Size | Format |
---|