English

Almost 2-SAT is Fixed-Parameter Tractable

Data Structures and Algorithms 2008-04-18 v4 Computational Geometry Logic in Computer Science

Abstract

We consider the following problem. Given a 2-CNF formula, is it possible to remove at most kk 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-kk 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(15kkm3)O(15^k*k*m^3) and thus we show that this problem is fixed-parameter tractable.

Keywords

Cite

@article{arxiv.0801.1300,
  title  = {Almost 2-SAT is Fixed-Parameter Tractable},
  author = {Igor Razgon and Barry O'Sullivan},
  journal= {arXiv preprint arXiv:0801.1300},
  year   = {2008}
}

Comments

This new version fixes the bug found by Somnath Sikdar in the proof of Claim 8. In the repaired version the modification of the Almost 2-SAT problem called 2-SLASAT is no longer needed and only the modification called 2-ASLASAT remains relevant. Hence the whole manuscript is updated so that the 2-SLASAT problem is not mentioned there anymore

R2 v1 2026-06-21T10:00:59.043Z