2SAT

2-SAT is a special case of the boolean satisfiability problem in which the formula is a conjunction of disjunctions of at most two literals. In the standard formulation, the formula is in 2-CNF: F = ∧i (ℓi1 ∨ ℓi2), where each literal ℓ is either a variable xk or its negation ¬xk. The problem asks whether there exists an assignment to the variables that makes F true.

A classic linear-time algorithm uses an implication graph. For each clause (a ∨ b), add the implications ¬a → b and ¬b → a. The graph has one vertex for every literal x and ¬x. The formula is satisfiable if and only if no variable x has x and ¬x in the same strongly connected component (SCC). This condition follows from the logical consequence of implications: if x and ¬x are mutually reachable, both must be true, a contradiction.

To get a satisfying assignment, compute the SCCs of the graph (via Tarjan or Kosaraju) and consider the condensation graph's topological order. For each variable x, assign it true if the SCC containing x comes after the SCC containing ¬x; otherwise assign false. If both literals are in the same SCC, the formula is unsatisfiable.

2-SAT runs in linear time relative to the input size: O(n + m) for n variables and m clauses. It is a fundamental example of a problem in P, in contrast to general SAT, which is NP-complete. Applications include circuit design, software verification, scheduling and constraint solving.