On Finding Short Resolution Refutations and Small Unsatisfiable Subsets

摘要

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 formulas and/or to various restricted versions of resolution including tree-like resolution, input resolution, and read-once resolution. Applying a metatheorem of Prick 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.