Almost 2-SAT is fixed-parameter tractable

We consider the following problem. Given a 2-CNF formula, is it possible to remove at most k 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-k 2-SAT, 2-CNF deletion, and 2-SAT deletion. The status of the 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 that solves this problem in O(15(k), x k x m(3)) time showing that this problem is fixed-parameter tractable. (C) 2009 Elsevier Inc. All rights reserved.