Solving MAX-r-SAT Above a Tight Lower Bound
Abstract
We present an exact algorithm that decides, for every fixed in time whether a given multiset of clauses of size admits a truth assignment that satisfies at least clauses. Thus \textsc{Max--Sat} is fixed-parameter tractable when parameterized by the number of satisfied clauses above the tight lower bound . This solves an open problem of Mahajan et al. (J. Comput. System Sci., 75, 2009). Our algorithm is based on a polynomial-time data reduction procedure that reduces a problem instance to an equivalent algebraically represented problem with variables. This is done by representing the instance as an appropriate polynomial, and by applying a probabilistic argument combined with some simple tools from Harmonic analysis to show that if the polynomial cannot be reduced to one of size , then there is a truth assignment satisfying the required number of clauses. We introduce a new notion of bikernelization from a parameterized problem to another one and apply it to prove that the above-mentioned parameterized \textsc{Max--Sat} admits a polynomial-size kernel. Combining another probabilistic argument with tools from graph matching theory and signed graphs, we show that if an instance of \textsc{Max-2-Sat} with clauses has at least variables after application of certain polynomial time reduction rules to it, then there is a truth assignment that satisfies at least clauses. We also outline how the fixed-parameter tractability and polynomial-size kernel results on \textsc{Max--Sat} can be extended to more general families of Boolean Constraint Satisfaction Problems.
Cite
@article{arxiv.0907.4573,
title = {Solving MAX-r-SAT Above a Tight Lower Bound},
author = {Noga Alon and Gregory Gutin and Eun Jung Kim and Stefan Szeider and Anders Yeo},
journal= {arXiv preprint arXiv:0907.4573},
year = {2011}
}