On finding short resolution refutations and small unsatisfiable subsets |
| |
Authors: | Michael R Fellows Stefan Szeider Graham Wrightson |
| |
Affiliation: | 1. School of Electrical Engineering and Computer Science, University of Newcastle, Callaghan 2308 NSW, Australia;2. Department of Computer Science, Durham University, Durham DH1 3LE, UK |
| |
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 W1], 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. |
| |
Keywords: | Resolution complexity Parameterized complexity W[1]-completeness" target="_blank">gif" overflow="scroll">W[1]-completeness Bounded local treewidth Planar formulas |
本文献已被 ScienceDirect 等数据库收录! |
|