Almost 2-SAT is Fixed-Parameter Tractable

TL;DR

This paper proves that the Almost 2-SAT problem, which involves removing at most k clauses to make a 2-CNF formula satisfiable, is fixed-parameter tractable by providing a specific algorithm.

Contribution

The authors resolve the long-standing open question by demonstrating fixed-parameter tractability of Almost 2-SAT with a new algorithm.

Findings

Algorithm solves Almost 2-SAT in O(15^k * k * m^3) time

Almost 2-SAT is fixed-parameter tractable

Addresses a long-standing open problem in Parameterized Complexity

Abstract

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.