Dept. of Computer Science, Royal Holloway, University of London, Egham, UK.

We consider the problem Max-r-SAT, an extensively studied variant of the classic satisfiability problem. Given an instance of CNF (Conjunctive normal form) in which each clause consists of exactly r literals, we seek to find a satisfying truth assignment that maximizes the number of satisfied clauses. Even when r=2, the problem is intractable unless P=NP. Hence the next quest is how close we can get to optimality with moderate usage of computation time/space.

We present an algorithm that decides, for every fixed r≥2 in time O(m) + 2^{O(k2)} whether a given set of m clauses of size r admits a truth assignment that satisfies at least ((2^{r}-1)m+k)/2^{r} clauses. Our algorithm is based on a polynomial-time preprocessing procedure that reduces a problem instance to an equivalent algebraically represented problem with O(k^{2}) variables. Moreover, by combining another probabilistic argument with tools from graph matching theory and signed graphs, we show that an instance of Max-2-Sat either is a YES-instance or can be transformed into an equivalent instance of size at most 3k.

This is a joint work with Noga Alon, Gregory Gutin, Stefan Szeider, and Anders Yeo.

Tags: 김은정