2-SAT

What Is 2-SAT?

2-SAT (2-Satisfiability) is a special case of the boolean satisfiability problem. Given n boolean variables x₁, x₂, …, x_n, and a formula in conjunctive normal form (CNF) where every clause has exactly two literals, determine whether there is a truth assignment that satisfies all clauses simultaneously.

A 2-SAT formula looks like:

(a ∨ b) ∧ (¬a ∨ c) ∧ (¬b ∨ ¬c) ∧ (b ∨ c)

Each clause (l1 ∨ l2) contains two literals, where a literal is either a variable x_i or its negation ¬x_i.

While general SAT (3-SAT and above) is NP-complete, 2-SAT can be solved in linear time O(n + m) using implication graphs and strongly connected components. This makes it a powerful tool in competitive programming:

• Team selection — “if person A is on the team, then person B must also be”
• Configuration problems — pairs of conflicting or dependent binary choices
• Graph coloring with 2 colors — certain constraints map directly to 2-SAT clauses
• Scheduling — binary decisions with pairwise constraints

The Implication Graph

The key insight is that every 2-SAT clause (a ∨ b) is logically equivalent to two implications:

(a ∨ b)  ≡  (¬a → b) ∧ (¬b → a)

Read it as: “if a is false, then b must be true” and “if b is false, then a must be true.” We build a directed graph where each variable x_i and its negation ¬x_i are separate nodes (2n nodes total), and each clause contributes two directed edges.

Example

Consider the formula with three variables (a, b, c) and four clauses:

The resulting implication graph with 6 nodes and 8 directed edges:

Notice the symmetry: if there is an edge from ¬a to b, there is always a contrapositive edge from ¬b to a. This is inherent to the construction and is critical for correctness.

Solving 2-SAT with SCCs

The connection between 2-SAT and strongly connected components is elegant:

A 2-SAT formula is UNSATISFIABLE
  if and only if
there exists a variable x such that
  x and ¬x are in the SAME strongly connected component.

Why? If x and ¬x are in the same SCC, there is a path from x to ¬x and from ¬x to x. Following implications: if x is true, we are forced to conclude ¬x is true (contradiction); if x is false, ¬x is true, which forces x to be true (again contradiction). No valid assignment exists.

Algorithm Overview

1. Build the implication graph (2n nodes, 2m edges for m clauses).
2. Find all SCCs using Kosaraju’s or Tarjan’s algorithm.
3. Check: for every variable x_i, verify that x_i and ¬x_i are in different SCCs. If any pair shares an SCC, output “UNSATISFIABLE.”
4. Extract a satisfying assignment from the SCC topological order.

Total time: O(n + m), where n is the number of variables and m is the number of clauses.

Step-by-Step Walkthrough

Let’s trace the full algorithm on our running example: variables a, b, c with clauses (a∨b), (¬a∨c), (¬b∨¬c), (b∨c).

Constructing the Assignment

Once we have found all SCCs and confirmed that no variable shares an SCC with its negation, we extract the satisfying assignment using the topological order of the condensation DAG (the DAG formed by collapsing each SCC into a single node).

For each variable x:
  if comp(x) > comp(¬x):   // x's SCC appears later in topo order
      x = TRUE
  else:
      x = FALSE

Intuition: In the implication graph, if ¬x can reach x (meaning assuming ¬x forces x to be true), but x does not force ¬x, then x should be true. The SCC with higher topological order is the one whose truth we “prefer.”

Why Does This Work?

The condensation DAG has a crucial property: if SCC(x) has a higher topological order than SCC(¬x), then there is no path from x to ¬x in the condensation. This means setting x = true cannot force any contradiction.

Implementation note: In Kosaraju’s algorithm, SCCs are discovered in reverse topological order. So the component index assigned during the second DFS pass naturally gives us the comparison: comp[x] > comp[¬x] means x’s SCC was discovered later, which corresponds to appearing earlier in reverse topological order — i.e., later in actual topological order.

Interactive Animation

C++ Implementation

Full 2-SAT Solver with Kosaraju’s SCC

#include <bits/stdc++.h>
using namespace std;

struct TwoSAT {
    int n;
    vector<vector<int>> adj, radj;
    vector<int> order, comp;
    vector<bool> vis;

    TwoSAT(int n) : n(n), adj(2*n), radj(2*n), comp(2*n, -1), vis(2*n) {}

    // Variable x: positive literal = 2*x, negative literal = 2*x+1
    // Negate a literal: lit ^ 1
    void addClause(int u, bool nu, int v, bool nv) {
        // clause: (u == nu) OR (v == nv)
        int a = 2*u + (nu ? 0 : 1);
        int b = 2*v + (nv ? 0 : 1);
        adj[a^1].push_back(b);
        adj[b^1].push_back(a);
        radj[b].push_back(a^1);
        radj[a].push_back(b^1);
    }

    void dfs1(int v) {
        vis[v] = true;
        for (int u : adj[v])
            if (!vis[u]) dfs1(u);
        order.push_back(v);
    }

    void dfs2(int v, int c) {
        comp[v] = c;
        for (int u : radj[v])
            if (comp[u] == -1) dfs2(u, c);
    }

    bool solve(vector<bool>& values) {
        vis.assign(2*n, false);
        order.clear();
        for (int i = 0; i < 2*n; i++)
            if (!vis[i]) dfs1(i);

        comp.assign(2*n, -1);
        int c = 0;
        for (int i = 2*n - 1; i >= 0; i--)
            if (comp[order[i]] == -1) dfs2(order[i], c++);

        values.assign(n, false);
        for (int i = 0; i < n; i++) {
            if (comp[2*i] == comp[2*i+1]) return false;
            values[i] = comp[2*i] > comp[2*i+1];
        }
        return true;
    }
};

Usage Example

int main() {
    int n, m;
    cin >> n >> m;
    TwoSAT sat(n);

    for (int i = 0; i < m; i++) {
        int u, v;
        cin >> u >> v;
        // positive number = true literal, negative = false literal
        bool nu = u > 0, nv = v > 0;
        u = abs(u) - 1; v = abs(v) - 1;
        sat.addClause(u, nu, v, nv);
    }

    vector<bool> vals;
    if (sat.solve(vals)) {
        cout << "SATISFIABLE\n";
        for (int i = 0; i < n; i++)
            cout << (vals[i] ? "T" : "F") << " \n"[i==n-1];
    } else {
        cout << "UNSATISFIABLE\n";
    }
}

Complexity

Common Extensions

Ladder Encoding for At-Most-One

When you need at most one of k variables to be true and k is large, the naive O(k²) pairwise approach is too slow. Introduce auxiliary variables y₁,…,y_k−1 and add:

// At most one of x[0..k-1] is true, using auxiliary y[0..k-2]
for (int i = 0; i < k-1; i++) {
    // x[i] implies y[i]
    sat.addClause(x[i], false, y[i], true);
    // y[i] implies not x[i+1]
    sat.addClause(y[i], false, x[i+1], false);
    if (i > 0) {
        // y[i-1] implies y[i]
        sat.addClause(y[i-1], false, y[i], true);
    }
}

This adds only O(k) clauses while enforcing the same constraint.

Practice Problems

1. CSES. Giant Pizza — Textbook 2-SAT, great for testing your template
2. Codeforces 228E. The Road to Berland is Paved with Good Intentions — Classic 2-SAT modeling
3. Codeforces 776D. The Door Problem — Switches and doors as 2-SAT
4. Codeforces 27D. Ring Road 2 — Non-crossing arcs on a circle
5. Codeforces 1971H. ±1 — Direct 2-SAT application
6. Codeforces 568C. New Language — 2-SAT with string constraints

Summary

• 2-SAT solves boolean formulas in CNF with exactly 2 literals per clause in O(n+m) time.
• Each clause (a ∨ b) becomes two edges in an implication graph: ¬a→b and ¬b→a.
• The formula is unsatisfiable iff any variable x and ¬x share a strongly connected component.
• Extract the assignment from SCC topological order: set x = true if comp(x) > comp(¬x).
• Common extensions include forcing variables, XOR constraints, and at-most-one via ladder encoding.
• The struct-based C++ template with Kosaraju’s SCC is clean and reusable for competitive programming.