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.
展开▼
机译：使用N变量和M子句的CNF中命题式F的缺陷定义为M-N.众所周知，最小的不挑离式（通过除去任何条款而变得满足的不匹匹替匹配的公式）具有阳性缺乏。识别最小不可挑离的公式是NP - 硬，并且最近显示了缺乏k的最小不匹匹替匹配的公式，可以在时间n ^ {o（k）}。我们改进了这一结果，并呈现了时间复杂度O的算法O（2 ^ K N ^ 4）。问题是在R.G的意义上的固定参数。 Downey和Mr Colorows，参数化复杂性，春家，纽约，1999。我们的算法给出了可满足问题的固定参数易解参数化：如果公式f的所有子集的最大缺陷最为k，那么我们可以在时间o（2 ^ Kn ^ 3）决定f是否满足（并且我们通过提供令人满意的真实分配或常规解决方案驳斥来证明决定）。用于固定参数易停工性可满足决策的已知参数是树宽或与树宽相关。与树宽度（其是NP难以计算）相反，通过图形匹配算法可以有效地计算最大缺陷。我们展示了一类无限类的公式，其中最大缺乏率优于树宽（和相关参数），以及逆转普遍的无限阶级。
展开▼
