Fixed-Parameter Tractability of Satisfying beyond the Number of Variables

Abstract

We consider a CNF formula F as a multiset of clauses: F = {c 1,…, 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 an edge between v ∈ V(F) and c ∈ F if v ∈ c or v¯∈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 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.