Fixed-Parameter Tractability of Satisfying Beyond the Number of Variables

We consider a CNF formula F as a multiset of clauses: F={c1,…,cm}. The set of variables of F will be denoted by V(F). Let BF 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 \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\bar{v} \in c$\end{document}. The matching number ν(F) of F is the size of a maximum matching in BF. 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.