---
title: "2-SAT"
summary: The implication graph, the "x and not x in one SCC" criterion, and the assignment read off the condensation order — with the linear-time proof.
difficulty: core
tags: [sat, scc, reduction]
time: n + m
prereq: [directed/scc, foundations/types]
see: [directed/scc, complexity/npc-graphs]
---

## The problem

:::definition label="The problem"
Variables $x_1..x_n$, clauses $(a \lor b)$ where each literal is $x_i$ or $\lnot x_i$. Decide whether a satisfying assignment exists (and produce one). **3**-SAT with the same shape is NP-complete (@complexity/npc-graphs); the difference is exactly what makes 2-SAT linear.
:::

## The implication-graph criterion

:::theorem title="The implication-graph criterion"
Rewrite each clause $(a \lor b)$ as the two implications $(\lnot a \to b)$ and $(\lnot b \to a)$. The formula is satisfiable iff no variable $x_i$ has $x_i$ and $\lnot x_i$ in the same strongly connected component of that digraph.
:::

:::proof
**Necessity.** If $x_i \leadsto \lnot x_i \leadsto x_i$, then in any assignment $x_i \Rightarrow \lnot x_i$ and $\lnot x_i \Rightarrow x_i$ must both hold, which is impossible — every implication on the cycle must be satisfied, and a cycle through both polarities forces a contradiction.

**Sufficiency.** Contract to the condensation DAG and number the components in topological order. Define
$$x_i := \big[\ \operatorname{scc}(\lnot x_i)\ \text{comes strictly before}\ \operatorname{scc}(x_i)\ \text{in that order}\ \big].$$ This is well defined: no component contains both literals, so exactly one of the two orders holds. The key structural fact is that the implication graph is **skew-symmetric**: negating every literal is an anti-automorphism, $u \to v$ iff $\bar v \to \bar u$. Hence on the condensation, $C \le D$ iff $\bar D \le \bar C$ (where $\bar C$ is the component of the negated literals).

Now suppose a clause $(a \lor b)$ is falsified by this assignment: $a$ and $b$ are both false, i.e. $\bar a, \bar b$ both true. Truth of $\bar a$ means $\operatorname{scc}(a) < \operatorname{scc}(\bar a)$... precisely, "$\bar a$ true" is the rule applied to the literal $\bar a$, so $\operatorname{scc}(\overline{\bar a}) = \operatorname{scc}(a)$ comes before $\operatorname{scc}(\bar a)$:
$$\operatorname{scc}(a) < \operatorname{scc}(\bar a), \qquad \operatorname{scc}(b) < \operatorname{scc}(\bar b).$$
The clause's own implications give $\bar a \to b$, so $\operatorname{scc}(\bar a) \le \operatorname{scc}(b)$, and $\bar b \to a$ gives $\operatorname{scc}(\bar b) \le \operatorname{scc}(a)$. Chaining:
$$\operatorname{scc}(a) < \operatorname{scc}(\bar a) \le \operatorname{scc}(b) < \operatorname{scc}(\bar b) \le \operatorname{scc}(a),$$
a strict cycle in a DAG — impossible. So no clause is falsified. ∎
:::

## Reading the assignment off the components

:::note title="Practical reading of the rule (one line of code)"
After Tarjan/Kosaraju, `sat = (comp[2i] != comp[2i+1])` for all $i$; the assignment is
```cpp twosat-assign.cpp
// literal encoding: 2*i = "x_i is true", 2*i+1 = "x_i is false"
int neg(int l) { return l ^ 1; }
void add_or(int a, int b) {            // clause (a or b) as two implications
    adj[neg(a)].push_back(b);
    adj[neg(b)].push_back(a);
}
// comp[] = component number in REVERSE topological order (Kosaraju's second pass gives it free)
vector<char> sat_ok(2 * n);            // ... compute comps first, then:
for (int i = 0; i < n; i++)
    if (comp[2*i] == comp[2*i+1]) return false;          // x_i and ¬x_i together
for (int i = 0; i < n; i++)
    ans[i] = comp[2*i] > comp[2*i+1];                     // true iff its SCC is later
```
i.e. **set $x_i$ true when its own SCC is later than the SCC of $\lnot x_i$**. The comparison uses component numbers from Kosaraju's second pass, which are already in reverse topological order, so no extra sorting is needed.
:::

## Modelling: the clause types you need

:::props title="Modelling: the three clause types you will actually need"
- $(\lnot a \lor \lnot b)$ = "not both": add $a \to \bar b$ and $b \to \bar a$ — a **conflict** edge; this is the "choose an independent set of size..." pattern restricted to pairs,
- $a \to b$ (an implication "if $x$ then $y$") is $(\lnot a \lor b)$: both directions of an *equivalence* $a \leftrightarrow b$ are two clauses ⇒ $a, b$ in the same SCC, so **equality of variables is just SCC merging**, and "exactly one of $a,b$" is $(a\lor b)\land(\lnot a\lor\lnot b)$,
- "at most one of $x_1..x_k$ is true" needs $O(k^2)$ pairwise clauses — quadratic blowup is normally avoided with a **chain of auxiliary variables** (prefix counters): $O(k)$ clauses, which is the trick used in "sudoku-like grid constraints" and "at most one rectangle per row".
:::

## Four ways 2-SAT solutions die

:::warning title="The four ways 2-SAT solutions die"
1. Encoding literals as $\pm i$ and then mixing "index by $|i|$" with "index by literal" — use the $2i/2i{+}1$ encoding above everywhere, including in `add_or`,
2. forgetting the **second** implication of each clause (only $a \to b$, not $b \to a$) — satisfiability answers then differ from the truth on formulas with a single unit clause,
3. unit clauses $(a)$: must be encoded as $(a \lor a)$, giving $\lnot a \to a$; a solver that only handles two-literal clauses silently ignores these,
4. recursion depth in Tarjan on $2n$ vertices with $n \le 10^6$ (@foundations/walks), and using Kosaraju's **second-pass order wrongly** (it must be reverse finish order of the *transposed-first* pass, @directed/scc).
:::

## A worked instance

:::example title="A worked instance"
$(x_1 \lor x_2)\ \land\ (\lnot x_1 \lor x_2)\ \land\ (\lnot x_2 \lor \lnot x_3)\ \land\ (x_3)$.
Implications: $\bar 1 \to 2$, $\bar 2 \to 1$, $1 \to 2$, $\bar 2 \to \bar 1$, $2 \to \bar 3$, $3 \to \bar 2$, $\bar 3 \to 3$.
From $\bar 2 \to \bar 1$ and $\bar 1 \to 2 \to \bar 3 \to \bar 2$ we get a cycle through $\bar 2$, so $\operatorname{scc}(\bar 2) = \operatorname{scc}(\bar 3)$ and $2$ forces nothing; no variable and its negation share an SCC, so it is satisfiable, and the topological rule gives $x_2 = $ true (its negation's SCC is earlier), $x_3 = $ true (unit clause ⇒ $\bar 3 \to 3$ forces it), $x_1$ free ⇒ true by the rule. Check: clause 2 is $(\lnot x_1 \lor x_2) = (F \lor T)$ ✓.
:::

:::problems
- [[CSES 1684]] Giant Pizza | https://cses.fi/problemset/task/1684 | core | the textbook 2-SAT instance: two toppings per pizza, contradictory preferences
- [[CSES 1682]] Flight Routes Check | https://cses.fi/problemset/task/1682 | easy | the SCC machinery you need, without the SAT part
:::