PaperlayerView exact revision on arXiv

Source-linked AI summary

Almost 2-SAT is Fixed-Parameter Tractable

Igor Razgon, Barry O'Sullivan

arXiv:0801.1300v4cs.DScs.CGcs.LO

TL;DR

Almost 2-SAT asks whether at most k clauses can be removed from a 2-CNF formula to make it satisfiable, a long-standing open question in parameterized complexity. The paper develops an algorithm for the problem and proves it runs in O(15^k*k*m^3) time, establishing fixed-parameter tractability.

  • Problem

    Whether deleting at most k clauses can make a 2-CNF formula satisfiable was a long-standing open question about fixed-parameter tractability.

    Source: §1 · p. 1

  • Method

    The algorithm solves an annotated 2-ASLASAT subproblem and uses iterative compression to reduce 2-ASAT to repeated applications of that solver.

    Source: §1.1 · p. 2

  • Results

    O(15^k*k*m^3) time suffices to solve 2-ASAT, establishing fixed-parameter tractability.

    Source: §1 · p. 1, §5 · pp. 24, 27

  • Takeaways & Limitations

    The paper resolves the open fixed-parameter tractability question for deleting clauses from 2-CNF formulas to obtain satisfiability.

    Source: §1 · p. 1

    Except in the final theorem, the analysis assumes pairwise distinct clauses and represents unit clauses by repeating their literal.

    Source: §2.1 · p. 4

Abstract

from arXiv · show

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.

1 Introduction

Almost 2-SAT asks whether deleting at most k clauses can make a 2-CNF formula satisfiable; this paper resolves the long-standing fixed-parameter tractability question. Its algorithm uses an annotated subproblem, clause-walk separation, and iterative compression to obtain an O(15^k*k*m^3)-time algorithm.

1 Introduction

  • O(15^k*k*m^3) time solves 2-ASAT, establishing that the long-standing open problem is fixed-parameter tractable.The bound is for a formula with m clauses.Source: §1 · p. 1

1.1 Overview of the algorithm

  • The algorithm combines an O*(5^k)-time annotated 2-ASLASAT solver with O*(3^k) applications via iterative compression.The transformation adapts a method employed for graph bipartization.Source: §1.1 · p. 2

1.2 Related Work

  • The approach adapts iterative compression used for graph bipartization and applies a graph-separation theorem strategy to neutral literals.Iterative compression was introduced in the graph bipartization work.Source: §1.1 · p. 2, §1.2 · p. 3

1.1 Overview of the algorithm

  • For 2-ASLASAT, unsatisfiability is characterized by walks from ¬L to ¬l or from ¬l back to itself, so clause deletion becomes walk separation.A Menger-like theorem equates the minimum clause separator with the maximum number of clause-disjoint paths when F is satisfiable with respect to L; a Ford–Fulkerson-like procedure computes this separator in polynomial time as a solution-size lower bound.Source: §1.1 · p. 2
  • Adding a neutral literal preserves the separator size and does not increase the solution size; otherwise, the recursive algorithm branches on a selected clause.The nonneutral case has at most three branches, each decreasing the parameter or increasing the lower bound, which bounds the search tree as a function of k.Source: §1.1 · pp. 2–3

2 Terminology

This section defines the formula, walk, and deletion-problem terminology used in the paper and develops structural characterizations connecting satisfiability with walks, separators, and neutral literals. It also presents a neutral-literal argument constructing a clause set no larger than the original whose deletion eliminates two specified walks to the negated literal.

2.1 2-CNF Formulas

  • The paper treats clauses as size two and, except in the final theorem, pairwise distinct; removal denotes taking the conjunction of clauses not removed.A unit clause is represented by repeating its literal, and F \ C denotes removal of one clause.Source: §2.1 · p. 4

2.2 Walks and paths

  • A walk is a nonempty clause sequence whose consecutive clauses link a literal to its negation; a path is a walk with pairwise distinct clauses.The walk's first and last literals specify its endpoints.Source: §2.2 · p. 5

2.3 2-ASAT and 2-ASLASAT problems.

  • Almost 2-SAT (2-ASAT) asks for a smallest CS of a 2-CNF formula F, while 2-ASLASAT asks for a smallest CS of the input triplet (F, L, l).In their parameterized versions, the output is a CS of size at most k if one exists; otherwise, it is NO.Source: §2.3 · p. 6

3.1 Basic Lemmas.

  • SWRT(F, L ∪ {l}) is false exactly when F has a walk from ¬l to ¬l or from ¬L to ¬l.Any walk from ¬L can also be reduced to a path with the same first and last literals using a subset of its clauses.Source: §3.2 · p. 7, §3.1 · p. 7

3.3 Smallest Separators

  • When SWRT(F, ¬L) is true, the largest number of clause-disjoint paths from L to ly equals the smallest separator size and the corresponding arc-separator size in the implication graph.The graph paths run from ¬L to ly; the equality relies on the stated satisfiability condition.Source: §3.3 · p. 9

3.4 Neutral Literals

  • A neutral literal preserves separator size, and adding it to L leaves a culprit set no larger than a smallest one for the original instance.A literal is neutral when adding it gives a valid 2-ASLASAT instance and leaves SepSize(F, ¬L, ¬l) unchanged.Source: §3.4 · p. 11
  • The set Y of eligible clauses in SP is bounded by |XR|: |Y| ≤ |XR|.Clause-disjoint paths associated with clauses in Y each intersect a clause of XR.Source: §3.4 · p. 12
  • F \ X* has no walk from ¬(L ∩ {l*}) to ¬l.The proof uses the last clause from SP on a putative path to show it would witness membership in Y, contradicting Y ⊆ X*.Source: §3.4 · p. 13
  • F \ X* has no walk from ¬l to ¬l.A putative walk would yield a walk from ¬(L ∩ {l*}) to ¬l, contradicting the preceding claim.Source: §3.4 · p. 13
  • X* is a clause set of (F, L ∪ {l*}, l) and satisfies |X*| ≤ |X|.The construction is X* = Y ∪ XSP ∪ XNR, with |Y| ≤ |XR|.Source: §3.4 · pp. 12, 14

4 Algorithm for the parameterized 2-ASLASAT problem and its analysis

This section presents a recursive solver for parameterized 2-ASLASAT, proves its correctness, and analyzes its search tree. It bounds FindCS’s runtime by combining a search-tree size bound with the cost of processing each recursive call.

4.1 The algorithm

  • The algorithm selects a clause from a suitable walk and branches by extending L with clause literals, deleting the clause, or both.Its cases distinguish walks from ¬L to ¬l and walks from ¬l back to ¬l, with branching determined by the clause literals’ relation to L and l.Source: §4.1 · p. 14

4.2 Additional Terminology and Auxiliary Lemmas

  • The measures α and β govern search-tree progress: α strictly decreases at every child, while β never increases and strictly decreases at non-trivial nodes.Consequently, the tree height is at most the root’s α, and β drops by at least the number of intervening non-trivial nodes along a path.Source: §4.2 · pp. 17–18

4.3 Correctness Proof

  • FindCS correctly returns a clause set of size at most k when one exists, and returns NO only when no such set exists.The proof establishes correctness by induction over recursive calls, which preserve valid inputs and decrease α.Source: §4.3 · pp. 18–19

4.4 Evaluation of the runtime.

  • The runtime analysis bounds search-tree leaf growth using β and distinguishes one-, two-, and three-child recursive calls.The supplied analysis shows that recursive calls can have up to three children and applies the β measure to bound the resulting leaf count.Source: §4.4 · pp. 20–21

4.4 Evaluation of the runtime

  • O(5^k*k*(n+k)*(m+|L|)) time suffices to solve parameterized 2-ASLASAT, where n=|Var(F)| and m=|Clauses(F)|.Theorem 6 gives this bound for an instance (F, L, l, k).Source: §4.4 · pp. 22–23
  • The search tree has at most 5^k leaves and at most 5^k*(n+k) nodes, with height at most n+k.Source: §4.4 · p. 22
  • Each recursive call takes O(k*(m+|L|)) time; SCC tests use DFS, while flow and neutrality checks use O(k) Ford–Fulkerson iterations with BFS.The implication graph operations take O(m+|L|) per DFS or BFS, and subsequent recursive-call graphs are subgraphs of the original graph.Source: §4.4 · p. 23

5 Fixed-Parameter Tractability of 2-ASAT problem

Section 5 establishes fixed-parameter tractability through reductions among annotated and ordinary 2-ASAT problems, iterative compression, and a transformation for formulas with repeated clauses.

5 Fixed-Parameter Tractability of 2-ASAT problem

  • O(15^k*k*m^3) time solves 2-ASAT, including formulas with repeated clause occurrences.Theorem 7 gives this bound for a formula with m clauses.Source: §5 · p. 24
  • Problem I1 is reduced to annotated 2-ASLASAT on a transformed formula, with solutions mapped back and the transformed formula having O(m) clauses.The construction establishes correspondence between deletion sets and separators for the annotated instance.Source: §5 · pp. 25–26
  • Problem I2 enumerates deletion or either-literal choices for each of k+1 clauses, reducing each case to Problem I1 and giving an O(15^k*k*m^2) bound.Problem I1 is solved in O(5^k*k*m^2) time.Source: §5 · pp. 24, 26, 27
  • For formulas without repeated clauses, iterative compression processes m prefixes with at most m calls to Problem I2, yielding O(15^k*k*m^3) time.Problem I2 is bounded by O(15^k*k*m^2).Source: §5 · pp. 26–27
  • Repeated clause occurrences are handled by indexing each occurrence and replacing it with two clauses using a fresh literal, producing a distinct-clause formula with 2m clauses.The paper establishes that deletion feasibility is preserved by this transformation.Source: §5 · pp. 27–28
  • The result also implies fixed-parameter tractability for vertex cover above perfect matching and related vertex-cover deletion problems through stated FPT-equivalences.The paper identifies these as by-products of the main result.Source: §5 · p. 28
Loading 0801.1300v4…