  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',
'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 $O(15^k*k*m^3)$ and thus we show that this problem is fixed-parameter
tractable.
