Junqiang Peng: A Fast Algorithm for MaxSAT Above Half Number of Clauses

Abstract

In the MaxSAT problem, given a CNF formula $\mathcal{F}$ with $m$ clauses and an integer $k$, we are asked whether there is a truth assignment that satisfies at least $k$ clauses of $\mathcal{F}$. The natural and well-studied parameterization of the MaxSAT problem takes $k$ as the parameter. In this work, we study the following parameterization of the MaxSAT problem: Given a CNF formula $\mathcal{F}$ with $m$ clauses, decide whether at least $m/2 + \mu$ clauses in $\mathcal{F}$ could be satisfied, where $\mu$ is the excess of the number of satisfied clauses over the trivial lower bound $m/2$ and is taken as the parameter. This perspective is known as the “above guarantee” parameterization. Since its introduction by Mahajan and Raman in 1999, the analysis of parameterization above guarantee has become a highly active and fruitful line of research. In this paper, we develop a new algorithm with runtime $O^*(2.1479^{\mu})$, improving the previous best upper bound $O^*(5.4064^{\mu})$ for this problem. Here, the $O^*$ notation omits polynomial factors.