__
TR03-002 | 13th December 2002 00:00
__

#### Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable

**Abstract:**
The 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.