On finding short resolution refutations and small unsatisfiable subsets

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

		Thumbnail	File	Description	Size	Format