We consider the following problem. Given a 2-CNF formula, is it possible to remove at most @math clauses so that the resulting 2-CNF formula is satisfiable? This problem is known to different research communities in Theoretical Computer Science under the names 'Almost 2-SAT', 'All-but- @math 2-SAT', '2-CNF deletion', '2-SAT deletion'. The status of fixed-parameter tractability of this problem is a long-standing open question in the area of Parameterized Complexity. We resolve this open question by proposing an algorithm which solves this problem in @math and thus we show that this problem is fixed-parameter tractable.
The parameterized MAX-SAT problem (a complementary problem to the one considered in the present paper) where the goal is to satisfy at least @math clauses of arbitrary sizes received a considerable attention from the researchers resulted in a series of improvements of the worst-case upper bound on the runtime of this problem. Currently the best algorithm is given in @cite_12 and solves this problem in @math , where @math is the size of the given formula.
@cite_12
2148185803
We present an exact 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. 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, Raman and Sikdar (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 O(k2) 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(k2), then there is a truth assignment satisfying the required number of clauses. 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 certain polynomial time reduction rules to it, then there is a truth assignment that satisfies at least (3m + k) 4 clauses. We also outline how the fixed-parameter tractability result on Max-r-Sat can be extended to a family of Boolean Constraint Satisfaction Problems.