On Finding Short Resolution Refutations and Small Unsatisfiable Subsets
Theoretical Computer Science, vol. 351, no. 3, pp. 351-359, 2006.
A preliminary version appeared in: Parameterized and Exact Computation, R. Downey, M. Fellows, F. Dehne, (eds.), Proceedings of the First International Workshop on Parameterized and Exact Computation (IWPEC04), Lecture Notes in Computer Science 3162, pp. 223-234, Springer Verlag, 2004.
Download: [paper ps] [paper pdf]
Abstract: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, the first level of the W-hierarchy of fixed-parameter intractable problems. Our results remain true if restricted to 3-SAT formulas 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 locally bounded treewidth the considered problems are fixed-parameter tractable. Hence, the problems are fixed-parameter tractable for planar CNF formulas and CNF formulas of bounded genus, k-SAT formulas with bounded number of occurrences per variable, and CNF formulas of bounded treewidth.