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) + 2O(k2) whether a given set of m clauses of size r admits a truth assignment that satisfies at least ((2r-1)m+k)/2r clauses. Our algorithm is based on a polynomial-time preprocessing procedure that reduces a problem instance to an equivalent algebraically represented problem with O(k2) 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.