2-SAT

2-SAT asks whether a boolean formula in conjunctive normal form with exactly two literals per clause is satisfiable. Unlike 3-SAT, it is solvable in linear time — via strongly connected components.

The implication graph

A clause $(a\vee b)$ is equivalent to two implications:

$(a\vee b)\equiv (\neg a\Rightarrow b)\wedge (\neg b\Rightarrow a).$

Build a directed graph with $2n$ vertices — one for each literal $x_i$ and $\neg x_i$ — and add both implication edges per clause. The graph is skew-symmetric: edge $u\to v$ implies edge $\neg v\to \neg u$.

The theorem

The formula is satisfiable iff no variable $x$ has $x$ and $\neg x$ in the same SCC.

If they share a component, then $x\Rightarrow \neg x$ and $\neg x\Rightarrow x$, which is a contradiction. Otherwise, an assignment exists — and there is a beautifully simple way to read it off:

Set $x$ true iff $\mathrm{comp}[x]$ comes later in topological order than $\mathrm{comp}[\neg x]$.

Since Tarjan numbers components in reverse topological order, that is comp[x] < comp[!x] with Tarjan’s numbering (and comp[x] > comp[!x] with Kosaraju’s). Check which convention your SCC code uses.

Implementation

struct TwoSat {
    int n;                                   // number of variables
    vector<vector<int>> adj, radj;
    vector<int> comp, order; vector<bool> used;
 
    TwoSat(int n) : n(n), adj(2*n), radj(2*n) {}
    int var(int i, bool sign) { return 2*i + (sign ? 0 : 1); }   // x_i / !x_i
 
    void addImplication(int a, bool sa, int b, bool sb) {
        adj[var(a, sa)].push_back(var(b, sb));
        radj[var(b, sb)].push_back(var(a, sa));
    }
    // clause (a^sa OR b^sb)
    void addClause(int a, bool sa, int b, bool sb) {
        addImplication(a, !sa, b, sb);
        addImplication(b, !sb, a, sa);
    }
    void addTrue(int a, bool sa)  { addClause(a, sa, a, sa); }   // force a = sa
 
    void dfs1(int u) { used[u] = true; for (int v : adj[u]) if (!used[v]) dfs1(v); order.push_back(u); }
    void dfs2(int u, int c) { comp[u] = c; for (int v : radj[u]) if (comp[v] == -1) dfs2(v, c); }
 
    bool solve(vector<bool>& assign) {
        used.assign(2*n, false); comp.assign(2*n, -1); order.clear();
        for (int i = 0; i < 2*n; i++) if (!used[i]) dfs1(i);
        int c = 0;
        for (int i = 2*n - 1; i >= 0; i--) if (comp[order[i]] == -1) dfs2(order[i], c++);
 
        assign.assign(n, false);
        for (int i = 0; i < n; i++) {
            if (comp[2*i] == comp[2*i + 1]) return false;
            assign[i] = comp[2*i] > comp[2*i + 1];    // Kosaraju numbering
        }
        return true;
    }
};

Encoding common constraints

Constraint	Clauses
$a$ is true	$(a\vee a)$
$a$ is false	$(\neg a\vee \neg a)$
$a\Rightarrow b$	$(\neg a\vee b)$
$a=b$	$(\neg a\vee b)\wedge (a\vee \neg b)$
$a\ne b$ (XOR)	$(a\vee b)\wedge (\neg a\vee \neg b)$
at most one of $a,b$	$(\neg a\vee \neg b)$
at least one of $a,b$	$(a\vee b)$
at most one of $x_1..x_k$	pairwise is $O(k^2)$; use the prefix-OR trick for $O(k)$ auxiliary variables

The at-most-one trick

Introduce $p_i$ meaning “some $x_j$ with $j\le i$ is true”. Then add $x_i\Rightarrow p_i$, $p_{i-1}\Rightarrow p_i$, and $p_{i-1}\Rightarrow \neg x_i$. That is $O(k)$ clauses instead of $O(k^2)$ — essential when $k$ is large.

Typical problems

• Two choices per object with pairwise conflicts — the canonical shape. Each object picks one of two options; some pairs of options are incompatible.
• Interval / segment placement — each item goes left or right, overlapping placements forbidden.
• 2-colouring with extra constraints — beyond plain bipartiteness.
• Boolean equation systems with binary clauses.
• Geometry: place each label above or below its point without overlaps.
• Binary search + 2-SAT — “maximise the minimum separation” problems: binary search the answer, build the 2-SAT instance for that threshold, test feasibility.

That last pattern is very common and worth internalising: 2-SAT decides feasibility, so pair it with a binary search whenever the problem asks to optimise a threshold.

See also: SCC · SAT · Tarjan