Solving MAX-r-SAT above a Tight Lower Bound

Noga Alon, Gregory Gutin, Eun Jung Kim, Stefan Szeider, Anders Yeo

Research output: Contribution to journalArticlepeer-review

78 Scopus citations

Abstract

We present an exact algorithm that decides, for every fixed ≥2 in time O(m)+2 O(k2) whether a given multiset of m clauses of size r admits a truth assignment that satisfies at least ((2 r -1)m+k)/2 r clauses. Thus Max-r-Sat is fixed-parameter tractable when parameterized by the number of satisfied clauses above the tight lower bound (1-2 -r )m. This solves an open problem of Mahajan et al. (J. Comput. Syst. Sci. 75(2):137-153, 2009). Our algorithm is based on a polynomial-time data reduction procedure that reduces a problem instance to an equivalent algebraically represented problem with O(9 r k 2) 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 O(9 r k 2), 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 Max-r-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 Max-2-Sat with m clauses has at least 3k variables after application of a certain polynomial time reduction rule to it, then there is a truth assignment that satisfies at least (3m+k)/4 clauses. We also outline how the fixed-parameter tractability and polynomial-size kernel results on Max-r-Sat can be extended to more general families of Boolean Constraint Satisfaction Problems.

Original languageEnglish (US)
Pages (from-to)638-655
Number of pages18
JournalAlgorithmica (New York)
Volume61
Issue number3
DOIs
StatePublished - Nov 2011
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • General Computer Science
  • Computer Science Applications
  • Applied Mathematics

Keywords

  • Above lower bound
  • Bikernel
  • Fixed-parameter tractable
  • Kernel
  • Max SAT

Fingerprint

Dive into the research topics of 'Solving MAX-r-SAT above a Tight Lower Bound'. Together they form a unique fingerprint.

Cite this