ECCC-Report TR03-002https://eccc.weizmann.ac.il/report/2003/002Comments and Revisions published for TR03-002en-usFri, 07 Feb 2003 00:00:00 +0200
Revision 1
| Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable |
Stefan Szeider
https://eccc.weizmann.ac.il/report/2003/002#revision1Fri, 07 Feb 2003 00:00:00 +0200https://eccc.weizmann.ac.il/report/2003/002#revision1
Paper TR03-002
| Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable |
Stefan Szeider
https://eccc.weizmann.ac.il/report/2003/002The deficiency of a propositional formula F in CNF with n variables
and m clauses is defined as m-n. It is known that minimal
unsatisfiable formulas (unsatisfiable formulas which become
satisfiable by removing any clause) have positive deficiency.
Recognition of minimal unsatisfiable formulas is NP-hard, and it was
shown recently that minimal unsatisfiable formulas with deficiency k
can be recognized in time n^{O(k)}. We improve this result and
present an algorithm with time complexity O(2^k n^4). Whence the
problem is fixed-parameter tractable in the sense of R.G. Downey and
M.R. Fellows, Parameterized Complexity, Springer, New York, 1999.
Our algorithm gives raise to a fixed-parameter tractable
parameterization of the satisfiability problem: If the maximum
deficiency over all subsets of a formula F is at most k, then we can
decide in time O(2^k n^3) whether F is satisfiable (and we certify the
decision by providing either a satisfying truth assignment or a
regular resolution refutation). Known parameters for fixed-parameter
tractable satisfiability decision are tree-width or related to
tree-width. In contrast to tree-width (which is NP-hard to compute)
the maximum deficiency can be calculated efficiently by graph matching
algorithms. We exhibit an infinite class of formulas where maximum
deficiency outperforms tree-width (and related parameters), as well as
an infinite class where the converse prevails.
Thu, 16 Jan 2003 00:20:55 +0200https://eccc.weizmann.ac.il/report/2003/002