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
Abstract In this paper, we present improved exact and parameterized algorithms for the maximum satisfiability problem. In particular, we give an algorithm that computes a truth assignment for a boolean formula F satisfying the maximum number of clauses in time O(1.3247 m | F |), where m is the number of clauses in F , and | F | is the sum of the number of literals appearing in each clause in F . Moreover, given a parameter k , we give an O(1.3695 k +| F |) parameterized algorithm that decides whether a truth assignment for F satisfying at least k clauses exists. Both algorithms improve the previous best algorithms by Bansal and Raman for the problem.