2-SAT

2-SAT is the Boolean satisfiability problem restricted to formulas in conjunctive normal form whose clauses have at most two literals. Where 3-SAT is NP-complete^[12], 2-SAT can be solved in linear time^[2]^[3]. The reason is that a two-literal clause $a \lor b$ is equivalent to the pair of implications $\neg a \Rightarrow b$ and $\neg b \Rightarrow a$ : a formula is unsatisfiable exactly when some variable implies its own negation and its negation implies it, which is a question about the strongly connected components of a graph. A satisfying assignment can be read off the order of those components. 2-SAT problems arise in scheduling, map labelling and other problems where each item has two alternatives and constraints relate pairs of choices.

§ 01

The implication graph

For a 2-CNF formula over variables $x_{1}, \dots, x_{n}$ , the implication graph has a vertex for each of the $2 n$ literals, and for each clause $a \lor b$ the two edges

\neg a \to b \neg b \to a

A unit clause $a$ is treated as $a \lor a$ , giving the edge $\neg a \to a$ . Paths are chains of implications: if there is a path from $u$ to $v$ , every satisfying assignment that makes $u$ true makes $v$ true. The graph is skew-symmetric: it has an edge $u \to v$ exactly when it has $\neg v \to \neg u$ , the contrapositive.

The criterion

Write $u \equiv v$ when literals $u$ and $v$ lie in the same strongly connected component, that is, each implies the other. Aspvall, Plass and Tarjan proved^[3]:

F is satisfiable ⟺ x \neq \equiv \neg x for every variable x

If $x$ and $\neg x$ are in one component, $x$ implies $\neg x$ and $\neg x$ implies $x$ , so neither value is possible. Conversely, if no component contains a complementary pair, order the components topologically and make each literal true if its component comes after its negation's. By skew symmetry the components of $x$ and $\neg x$ are mirror images, so this assigns each variable exactly one value, and no edge can lead from a true literal to a false one, so every clause is satisfied.

§ 02

Algorithm

Tarjan's algorithm finds the strongly connected components in one depth-first search, in time linear in the size of the graph^[4]. It numbers components in reverse topological order, so a variable is true when its positive literal's component has the smaller number:

2-SAT by strongly connected components, with the assignment checked against the clauses.

(* 2-SAT in linear time. Each clause (a v b) gives two implications,
   -a -> b and -b -> a. The formula is unsatisfiable exactly when some
   variable and its negation are in the same strongly connected component
   of the implication graph. Variables are 1..n; literal v is node 2v,
   -v is node 2v+1. *)
let node l = if l > 0 then 2 * l else (2 * -l) + 1
let neg_node u = u lxor 1
 
let solve n clauses =
  let size = (2 * n) + 2 in
  let graph = Array.make size [] in
  List.iter (fun (a, b) ->
    graph.(neg_node (node a)) <- node b :: graph.(neg_node (node a));
    graph.(neg_node (node b)) <- node a :: graph.(neg_node (node b))) clauses;
  (* Tarjan's algorithm. Components are numbered in reverse topological
     order: a component is numbered before any component that reaches it. *)
  let index = Array.make size (-1) and low = Array.make size 0 and comp = Array.make size (-1) in
  let on_stack = Array.make size false and stack = ref [] and counter = ref 0 and ncomp = ref 0 in
  let rec visit u =
    index.(u) <- !counter; low.(u) <- !counter; incr counter;
    stack := u :: !stack; on_stack.(u) <- true;
    List.iter (fun w ->
      if index.(w) < 0 then (visit w; low.(u) <- min low.(u) low.(w))
      else if on_stack.(w) then low.(u) <- min low.(u) index.(w)) graph.(u);
    if low.(u) = index.(u) then begin
      let rec pop () = match !stack with
        | w :: rest -> stack := rest; on_stack.(w) <- false; comp.(w) <- !ncomp; if w <> u then pop ()
        | [] -> () in
      pop (); incr ncomp
    end
  in
  for u = 2 to size - 1 do if index.(u) < 0 then visit u done;
  if List.exists (fun v -> comp.(2 * v) = comp.((2 * v) + 1)) (List.init n (fun i -> i + 1)) then None
  else
    (* v is true if its component comes later in topological order than
       that of -v, that is, has the smaller number. *)
    Some (Array.init (n + 1) (fun v -> v > 0 && comp.(2 * v) < comp.((2 * v) + 1)))
 
let satisfies a clauses = List.for_all (fun (x, y) -> let t l = if l > 0 then a.(l) else not a.(-l) in t x || t y) clauses

Running it.

(x1 v x2)(-x1 v x3)(-x2 v -x3)(x3 v x4)(-x4 v -x1):
  x1=true x2=false x3=true x4=false, satisfies: true
(x1 v x2)(x1 v -x2)(-x1 v x2)(-x1 v -x2):
  unsatisfiable
random instance, 100000 variables, 50000 clauses: satisfiable, assignment checked: true

The second formula contains all four clauses on two variables and every literal implies every other, so all four lie in one component. The whole procedure is linear in the number of variables plus clauses, and the random instance with a hundred thousand variables is solved in a single pass. Even, Itai and Shamir had earlier given a different linear-time algorithm that assigns values and propagates them with limited backtracking^[2].

Resolution and propagation

2-SAT is also easy for resolution: resolving two clauses of at most two literals gives a clause of at most two literals, so the closure under resolution has $O (n^{2})$ clauses, and the formula is unsatisfiable exactly when the empty clause appears. Krom showed decidability of this class in 1967 by this kind of argument^[1]. Unit propagation is complete in a weaker sense: assigning a literal and propagating either finds a conflict, which proves the negation, or leaves a formula that is still satisfiable if the original was, because the untouched clauses are exactly those of the original that mention no assigned variable.

§ 03

Complexity

2-SAT is in P, and more precisely it is NL-complete: satisfiability reduces to reachability in the implication graph, which a nondeterministic machine can check in logarithmic space^[10]. The optimization version, MAX-2-SAT, which asks for an assignment satisfying as many clauses as possible, is NP-hard^[9], as is 2-SAT with a constraint on the number of true variables. 3-SAT is NP-complete^[12], so the boundary between tractable and intractable lies between two and three literals per clause.

§ 04

Random 2-SAT

In a random 2-CNF formula with $n$ variables and $m = α n$ clauses, each clause chosen uniformly, the probability of satisfiability tends to 1 for $α < 1$ and to 0 for $α > 1$ , a result proved independently by Chvátal and Reed and by Goerdt^[6]^[7]. The transition sharpens as $n$ grows, within a window of width of order $n^{- 1/3}$ around $α = 1$ ^[8]:

The fraction of random formulas that are satisfiable, over 200 formulas for each size and ratio.

(* Random 2-SAT: m clauses over n variables, each with two distinct
   variables and random signs. The probability of satisfiability drops from
   near 1 to near 0 around m/n = 1, more sharply as n grows. *)
let random_formula n m =
  List.init m (fun _ ->
    let a = 1 + Random.int n in
    let rec other () = let b = 1 + Random.int n in if b = a then other () else b in
    let s x = if Random.bool () then x else -x in
    (s a, s (other ())))

Running it.

n         m/n=0.6  m/n=0.8  m/n=0.9  m/n=1.0  m/n=1.1  m/n=1.2  m/n=1.4
100           100%       99%       98%       98%       87%       80%       41%
1000          100%      100%      100%       95%       72%       25%        0%
10000         100%      100%      100%       88%       24%        0%        0%

At $α = 1.2$ a fifth of the formulas with 100 variables are unsatisfiable, and all of those with 10,000 are. The critical ratio for 3-SAT, about 4.27, is known only from experiments and non-rigorous calculations, and the hardest random 3-SAT instances lie near it.

§ 05

A random walk

Papadimitriou gave a simple randomized algorithm: start from any assignment and, while some clause is false, pick a false clause and flip one of its two variables at random. If the formula has a satisfying assignment $A$ , each flip moves the current assignment one step closer to $A$ with probability at least one half, since at least one of the two variables of a false clause disagrees with $A$ . The number of disagreements behaves like a random walk on $0, \dots, n$ biased toward 0, which reaches 0 in $O (n^{2})$ expected steps^[5]:

The random walk on a formula that forces all variables equal, where the walk is unbiased.

(* Papadimitriou's random walk: start from any assignment; while some
   clause is false, pick a false clause and flip one of its two variables
   at random. On a satisfiable formula it finds a solution in O(n^2)
   expected flips. *)
let walk n clauses =
  let a = Array.init (n + 1) (fun _ -> Random.bool ()) in
  let cls = Array.of_list clauses in
  let t l = if l > 0 then a.(l) else not a.(-l) in
  let flips = ref 0 in
  let rec loop () =
    let unsat = List.filter (fun (x, y) -> not (t x || t y)) (Array.to_list cls) in
    match unsat with
    | [] -> !flips
    | _ ->
        let x, y = List.nth unsat (Random.int (List.length unsat)) in
        let v = abs (if Random.bool () then x else y) in
        a.(v) <- not a.(v); incr flips; loop ()
  in
  loop ()
 
(* A satisfiable chain on which the walk behaves like a random walk on a
   line: x1 = x2 = ... = xn, and x1 true. *)
let chain n = (1, 1) :: List.concat (List.init (n - 1) (fun i -> [ (-(i + 1), i + 2); (i + 1, -(i + 2)) ]))

Running it; 20 runs for each n.

n      average flips  flips / n^2
10                66        0.655
20               311        0.778
40              1315        0.822
80              4275        0.668

The number of flips divided by $n^{2}$ stays roughly constant. The same idea, with restarts, gives Schöning's algorithm for 3-SAT, which is exponential but faster than exhaustive search.

§ 06

Applications

Even, Itai and Shamir met 2-SAT in timetabling, where each class must be placed in one of two periods and pairs of classes conflict^[2]. In map labelling, each feature can take its label in one of two positions and overlapping labels exclude each other; deciding whether all features can be labelled is 2-SAT^[11]. Other examples are 2-colouring of graphs with additional constraints, the placement of pairs of alternatives in circuit layout, and the Horn-like fragments of constraint problems. In CDCL solvers, binary clauses are kept in the implication graph directly and propagated separately from longer clauses.

§ 07

History

Krom studied formulas with only binary disjunctions in 1967^[1], and Cook noted in 1971 that satisfiability of 2-CNF is decidable in polynomial time while 3-CNF is NP-complete^[12]. Even, Itai and Shamir gave a linear-time algorithm in 1976^[2], and Aspvall, Plass and Tarjan the one based on strongly connected components in 1979^[3]. Papadimitriou's random walk appeared in 1991^[5], and the threshold for random 2-SAT was established in 1992^[6]^[7].