Fixed-Parameter Tractability of Satisfying Beyond the Number of Variables

Abstract

We consider a CNF formula F as a multiset of clauses: F={c ₁,…,c _m }. The set of variables of F will be denoted by V(F). Let B _F denote the bipartite graph with partite sets V(F) and F and with an edge between v∈V(F) and c∈F if v∈c or $\bar{v} \in c$. The matching number ν(F) of F is the size of a maximum matching in B _F . In our main result, we prove that the following parameterization of MaxSat (denoted by (ν(F)+k)-SAT) is fixed-parameter tractable: Given a formula F, decide whether we can satisfy at least ν(F)+k clauses in F, where k is the parameter.

A formula F is called variable-matched if ν(F)=|V(F)|. Let δ(F)=|F|−|V(F)| and δ ^∗(F)=max _F′⊆F δ(F′). Our main result implies fixed-parameter tractability of MaxSat parameterized by δ(F) for variable-matched formulas F; this complements related results of Kullmann (IEEE Conference on Computational Complexity, pp. 116–124, 2000) and Szeider (J. Comput. Syst. Sci. 69(4):656–674, 2004) for MaxSat parameterized by δ ^∗(F).

To obtain our main result, we reduce (ν(F)+k)-SAT into the following parameterization of the Hitting Set problem (denoted by (m−k)-Hitting Set): given a collection $\mathcal{C}$ of m subsets of a ground set U of n elements, decide whether there is X⊆U such that C∩X≠∅ for each $C\in \mathcal{C}$ and |X|≤m−k, where k is the parameter. Gutin, Jones and Yeo (Theor. Comput. Sci. 412(41):5744–5751, 2011) proved that (m−k)-Hitting Set is fixed-parameter tractable by obtaining an exponential kernel for the problem. We obtain two algorithms for (m−k)-Hitting Set: a deterministic algorithm of runtime $O((2e)^{2k+O(\log^{2} k)} (m+n)^{O(1)})$ and a randomized algorithm of expected runtime $O(8^{k+O(\sqrt{k})} (m+n)^{O(1)})$. Our deterministic algorithm improves an algorithm that follows from the kernelization result of Gutin, Jones and Yeo (Theor. Comput. Sci. 412(41):5744–5751, 2011).