--- title: 2-SAT via Implication Graphs module: Graphs moduleNumber: 6 lessonNumber: 12 order: 612 summary: | A boolean formula whose every clause has exactly two literals can be solved in _linear_ time — even though its three-literal cousin is NP-complete. The idea is to read each clause as a pair of implications, build a directed graph on the $2n$ literals, and ask a question we already know how to answer: which literals share a strongly connected component? The formula is satisfiable iff no variable lands in the same SCC as its own negation, and the SCCs' topological order yields a satisfying assignment for free. topics: [Graphs] sources: - book: CLRS ref: "Ch. 20 — (SCC applications)" - book: Skiena ref: "§ — Satisfiability" - book: Erickson ref: "Ch. — Strong Connectivity / Applications" practice: - title: 'Satisfiability of Equality Equations' slug: satisfiability-of-equality-equations difficulty: Medium - title: 'Possible Bipartition' slug: possible-bipartition difficulty: Medium - title: 'Divide Nodes Into the Maximum Number of Groups' slug: divide-nodes-into-the-maximum-number-of-groups difficulty: Hard --- The previous lesson gave us [**strongly connected components**](/algorithms/graphs/topological-sort-and-scc): the maximal sets of vertices in a directed graph that can all reach one another, computable in $O(n+m)$ by a [two-pass depth-first search](/algorithms/graphs/representations-and-traversal). This lesson is its most direct payoff: a problem that _looks_ like intractable boolean satisfiability, but whose two-literal special case collapses to a single SCC computation. The problem is **2-satisfiability** (2-SAT). We are given $n$ boolean variables $x_1, \dots, x_n$ and a formula in **conjunctive normal form** where every clause has _exactly two_ literals, a literal being a variable $x_i$ or its negation $\lnot x_i$: $$ \Phi = (\ell_{1} \vee \ell_{2}) \wedge (\ell_{3} \vee \ell_{4}) \wedge \cdots \wedge (\ell_{2m-1} \vee \ell_{2m}). $$ We must decide whether some assignment of true/false to the variables makes _every_ clause true at once, and if so, produce one. Allowing **three** literals per clause gives 3-SAT, which is NP-complete, the canonical hard problem we will meet in the intractability module. The jump from two literals to three is the jump from $O(n+m)$ to (as far as anyone knows) exponential. 2-SAT sits firmly in $\mathsf{P}$, and the reason is entirely graph-theoretic.[^skiena-sat] ## Reading a clause as two implications A two-literal disjunction is logically the same as a pair of implications. The clause $(a \vee b)$ asserts that at least one of $a$, $b$ is true. So if $a$ happens to be false, $b$ is _forced_ true; and symmetrically if $b$ is false, $a$ is forced. In symbols, $$ (a \vee b) \;\equiv\; (\lnot a \Rightarrow b) \;\wedge\; (\lnot b \Rightarrow a). $$ This rewriting is the whole idea. Build a directed **implication graph** $G$ on $2n$ vertices, one for each literal $x_i$ and one for its negation $\lnot x_i$. For every clause $(a \vee b)$ in $\Phi$, add the two edges $$ \lnot a \longrightarrow b \qquad\text{and}\qquad \lnot b \longrightarrow a, $$ where $a$ and $b$ range over _literals_ and double negation cancels ($\lnot\lnot x$ is $x$). In figures we write $\bar{x}$ for $\lnot x$. The construction rules, spelled out: - **Clause $(a \vee b)$** with two positive literals: edges $\bar a \to b$ and $\bar b \to a$. Nothing else — in particular _not_ $a \to b$. - **Clause $(\lnot a \vee b)$**, i.e. the implication $a \Rightarrow b$: edges $a \to b$ and $\bar b \to \bar a$. Encoding an implication directly still produces _two_ edges; the contrapositive comes along whether you write it or not. - **Clause $(\lnot a \vee \lnot b)$** ("not both"): edges $a \to \bar b$ and $b \to \bar a$. - **Unit clause $(a)$**: treat it as $(a \vee a)$, contributing the single edge $\bar a \to a$, which forces $a$ true (we will see why in a moment). - **Constraint "$x$ and $y$ must differ"**: two clauses $(x \vee y)$ and $(\lnot x \vee \lnot y)$, four edges; "must agree" is $(x \vee \lnot y)$ and $(\lnot x \vee y)$. Every clause thus contributes exactly two edges (a duplicated edge for a unit clause), so the graph has $2n$ vertices and $2m$ edges. An edge $u \to v$ reads "if $u$ is true, then $v$ must be true." Because implication is **transitive**, a directed _path_ $u \rightsquigarrow w$ means that committing to $u$ forces $w$: reachability in $G$ is the relation "forces." The graph is **skew-symmetric** by construction. The contrapositive $(\lnot a \Rightarrow b) \equiv (\lnot b \Rightarrow a)$ means every edge $u \to v$ has a mirror edge $\lnot v \to \lnot u$, and this symmetry is what makes the assignment step work. $$ % caption: skew-symmetry: every edge $u\to v$ (top) has a mirror edge % $\lnot v\to\lnot u$ (bottom, in acc) — its contrapositive \begin{tikzpicture}[ >=stealth, every node/.style={circle, draw, minimum size=9mm, inner sep=1pt, font=\small}] \definecolor{acc}{HTML}{2348F2} \node (u) at (0,1.0) {$u$}; \node (v) at (3.0,1.0) {$v$}; \node (nv) at (0,-0.8) {$\bar v$}; \node (nu) at (3.0,-0.8) {$\bar u$}; \draw[->, thick] (u) -- (v); \draw[->, acc, thick] (nv) -- (nu); \node[draw=none, font=\footnotesize] at (1.5,1.45) {edge}; \node[draw=none, font=\footnotesize, text=acc] at (1.5,-1.35) {mirror edge}; \end{tikzpicture} $$ $$ % caption: one clause, two edges: $(a\vee b)$ contributes $\lnot a\to b$ and % $\lnot b\to a$, each the contrapositive of the other \begin{tikzpicture}[ >=stealth, every node/.style={circle, draw, minimum size=9mm, inner sep=1pt, font=\small}] \definecolor{acc}{HTML}{2348F2} \node (na) at (0,1.0) {$\bar a$}; \node (b) at (3.0,1.0) {$b$}; \node (nb) at (0,-0.8) {$\bar b$}; \node (a) at (3.0,-0.8){$a$}; \draw[->, acc, thick] (na) -- (b); \draw[->, acc, thick] (nb) -- (a); \end{tikzpicture} $$ ## When is the formula satisfiable? A satisfying assignment must respect every forced implication: if it sets $u$ true and $u \rightsquigarrow v$, it must set $v$ true. The failure mode is a **cycle of forcing** that loops a literal back to its own negation — and such a cycle is exactly an SCC. > **Theorem (2-SAT satisfiability).** $\Phi$ is satisfiable **if and only if** no > variable $x_i$ has $x_i$ and $\lnot x_i$ in the _same_ strongly connected > component of the implication graph $G$. The "no collision" test is a decision procedure — it answers _satisfiable?_ — so its correctness splits into the two halves we named in [the foundations](/algorithms/foundations/what-is-an-algorithm): the test must never report satisfiable when no assignment exists (**soundness**), and must never miss a formula that is satisfiable (**completeness**). The two directions of the iff give exactly these two guarantees. The forward direction below — a collision forces a contradiction — is **completeness**: every truly unsatisfiable formula does produce a collision, so a satisfiable one never gets rejected. The converse, built constructively in the next section, is **soundness**: when the test passes we exhibit an assignment that really satisfies $\Phi$, so a "satisfiable" verdict is never a false positive. > **Proof of the forward (contradiction) direction.** Suppose some variable $x$ has > both $x$ and $\lnot x$ in one SCC. By definition of an SCC there is a path > $x \rightsquigarrow \lnot x$ and a path $\lnot x \rightsquigarrow x$. Reading the > edges as implications, $x \rightsquigarrow \lnot x$ says $x \Rightarrow \lnot x$ > and $\lnot x \rightsquigarrow x$ says $\lnot x \Rightarrow x$. Now consider any > assignment. If it sets $x = \text{true}$, then $x \Rightarrow \lnot x$ forces > $\lnot x$ true, i.e. $x$ false — a contradiction. If it sets $x = \text{false}$, > then $\lnot x \Rightarrow x$ forces $x$ true — again a contradiction. No > assignment survives, so $\Phi$ is unsatisfiable. $\qed$ $$ % caption: UNSAT: $x\rightsquigarrow\lnot x$ and $\lnot x\rightsquigarrow x$ put both in % one SCC, forcing $x\Rightarrow\lnot x$ and $\lnot x\Rightarrow x$ \begin{tikzpicture}[ >=stealth, every node/.style={circle, draw, minimum size=9mm, inner sep=1pt, font=\small}] \definecolor{acc}{HTML}{2348F2} \node[draw=acc, thick, text=acc] (x) at (0,0) {$x$}; \node (p) at (2.2,0.9) {$p$}; \node[draw=acc, thick, text=acc] (nx) at (4.4,0) {$\lnot x$}; \node (q) at (2.2,-0.9) {$q$}; \draw[->] (x) -- (p); \draw[->] (p) -- (nx); \draw[->] (nx) -- (q); \draw[->] (q) -- (x); \node[draw=none, font=\footnotesize, text=acc] at (2.2,-1.9) {one SCC: unsatisf\/iable}; \end{tikzpicture} $$ The **converse**, that if no variable collides with its negation in an SCC then a satisfying assignment _exists_, is the more delicate half. The construction below builds an explicit assignment, and the same skew-symmetry argument proves it consistent, establishing the converse constructively.[^erickson-scc] ## Constructing a satisfying assignment Suppose the test passes: no $x_i$ and $\lnot x_i$ share an SCC. Contract each SCC to a single super-vertex; the result is the **condensation** of $G$, which is always a directed acyclic graph (any cycle among components would have merged them). A DAG has a topological order, and topological order is what we assign by. > **Remark (The assignment rule).** For each variable $x$, set $x = \text{true}$ exactly when the SCC of > $x$ comes _after_ the SCC of $\lnot x$ in topological order of the condensation. > Equivalently, **assign true to whichever of $x$, $\lnot x$ lies in the SCC > that is topologically later** (closer to the sinks). A two-pass SCC algorithm (Kosaraju or Tarjan) already numbers the components in a _reverse_ topological order: Tarjan emits components sink-first, and Kosaraju's second pass discovers them in the order of decreasing first-pass finish time. So the comparison costs nothing extra: we set a literal true iff its component is discovered _before_ its negation's in that reverse order (i.e. later topologically). ```algorithm caption: $\textsc{TwoSat}(n, \text{clauses})$ — decide and assign in $O(n+m)$ build implication graph $G$ on $2n$ literal-vertices for each clause $(a \vee b)$ do add edge $\lnot a \to b$ and edge $\lnot b \to a$ $comp[\cdot] \gets \textsc{StronglyConnectedComponents}(G)$ // comp in reverse topo order for $i \gets 1$ to $n$ do if $comp[x_i] = comp[\lnot x_i]$ then return Unsatisfiable for $i \gets 1$ to $n$ do $value[x_i] \gets (comp[x_i] < comp[\lnot x_i])$ // later topo $\Rightarrow$ true return $value$ ``` > **Proof (the rule is consistent).** We must check the assignment never violates > an implication edge, never sets some $u$ true and a forced $v$ false. Two facts > make this automatic. First, edges of $G$ run from earlier components to _later_ > ones in topological order (that is what topological order means for a DAG), so an > edge $u \to v$ has $\text{comp}(u)$ no later than $\text{comp}(v)$. Second, the > skew-symmetry of $G$ guarantees that the condensation has a matching central > symmetry: the component of $\lnot u$ sits in the _mirror_ position to the > component of $u$. Concretely, if $u$'s component is topologically later than > $\lnot u$'s, so we set $u$ true, then for any edge $u \to v$ the mirror edge > $\lnot v \to \lnot u$ forces $\lnot v$'s component to be no later than $\lnot u$'s, > hence $v$'s component is no _earlier_ than $u$'s, so $v$ is also assigned true. The > edge is satisfied. No clause can be violated, so the assignment really satisfies > $\Phi$ — the converse of the theorem holds, and with it the **soundness** of the > decider: a "satisfiable" verdict always comes with a witness.[^clrs-scc] $\qed$ $$ % caption: assign by reverse topological order of SCCs \begin{tikzpicture}[ >=stealth, node distance=8mm, every node/.style={draw, minimum size=9mm, inner sep=3pt, font=\small}] \definecolor{acc}{HTML}{2348F2} % condensation: every SCC is a singleton here (the implication graph is acyclic) \node (c1) {$\overline{x}_3$}; \node (c2) [right=of c1] {$\overline{x}_2$}; \node (c3) [right=of c2] {$\overline{x}_1$}; \node (c4) [right=of c3, draw=acc, thick, text=acc] {$x_1$}; \node (c5) [right=of c4, draw=acc, thick, text=acc] {$x_2$}; \node (c6) [right=of c5, draw=acc, thick, text=acc] {$x_3$}; \draw[->, thick] ([yshift=-7mm]c1.west) -- ([yshift=-7mm]c6.east) node[midway, below, draw=none, font=\footnotesize] {top\/ological order: sinks at righ\/t, pick the later literal of eac\/h pair}; \end{tikzpicture} $$ Here $\lnot x_1$ sits in an earlier component than $x_1$, so $x_1$ is set **true** (its SCC, highlighted, is later); likewise $\lnot x_3$ precedes $x_3$, so $x_3$ is **true**. The whole pipeline (build $G$, run one SCC computation, scan the $n$ variables twice) is $O(n+m)$ time and space, matching the cost of the SCC algorithm it rests on. ## A complete worked example We run the pipeline once end to end. Take three variables and four clauses: $$ \Phi = (x_1 \vee x_2) \wedge (\lnot x_1 \vee x_3) \wedge (\lnot x_2 \vee \lnot x_3) \wedge (x_1 \vee x_3). $$ **Build the implication graph.** Each clause $(a \vee b)$ contributes $\bar a \to b$ and $\bar b \to a$. Working clause by clause (writing $\bar x$ for $\lnot x$): | Clause | First edge | Second edge | | --- | --- | --- | | $(x_1 \vee x_2)$ | $\bar x_1 \to x_2$ | $\bar x_2 \to x_1$ | | $(\lnot x_1 \vee x_3)$ | $x_1 \to x_3$ | $\bar x_3 \to \bar x_1$ | | $(\lnot x_2 \vee \lnot x_3)$ | $x_2 \to \bar x_3$ | $x_3 \to \bar x_2$ | | $(x_1 \vee x_3)$ | $\bar x_1 \to x_3$ | $\bar x_3 \to x_1$ | That is eight edges on the six literal-vertices $x_1, \bar x_1, x_2, \bar x_2, x_3, \bar x_3$: $$ % caption: The implication graph of $\Phi$. Eight edges (two per clause); the mirror % symmetry is visible — e.g. $x_1 \to x_3$ pairs with $\bar x_3 \to \bar x_1$. % The edges close two three-cycles: SCC A = {x-bar-1, x2, x-bar-3} (left, grey) % and SCC B = {x1, x-bar-2, x3} (right, blue). No literal shares a component with % its negation, so $\Phi$ is satisfiable. Both cross edges run A -> B, so B is the % later (sink) component. \begin{tikzpicture}[>=Stealth, font=\small, A/.style={circle, draw, minimum size=8.5mm, inner sep=1pt, font=\small, fill=black!8}, B/.style={circle, draw=acc, thick, minimum size=8.5mm, inner sep=1pt, font=\small, fill=acc!12, text=acc}] \definecolor{acc}{HTML}{2348F2} % SCC A on the left (a 3-cycle), SCC B on the right (a 3-cycle) \node[A] (nx1) at (0,1.3) {$\bar x_1$}; \node[A] (x2) at (1.5,-0.4) {$x_2$}; \node[A] (nx3) at (0,-2.1) {$\bar x_3$}; \node[B] (x1) at (5.5,1.3) {$x_1$}; \node[B] (nx2) at (4.0,-0.4) {$\bar x_2$}; \node[B] (x3) at (5.5,-2.1) {$x_3$}; % SCC A internal cycle \draw[->] (nx1) -- (x2); \draw[->] (x2) -- (nx3); \draw[->] (nx3) -- (nx1); % SCC B internal cycle \draw[->, acc] (x1) -- (x3); \draw[->, acc] (x3) -- (nx2); \draw[->, acc] (nx2) -- (x1); % cross edges A -> B \draw[->, black] (nx1) to[bend left=10] (x1); \draw[->, black] (nx3) to[bend right=10] (x1); \node[font=\scriptsize] at (0.5,-3.0) {SCC A (earlier)}; \node[font=\scriptsize, acc] at (5.0,-3.0) {SCC B (later / sink)}; \end{tikzpicture} $$ **Run SCCs.** The edges close two directed triangles: $\bar x_1 \to x_2 \to \bar x_3 \to \bar x_1$ is one strongly connected component, and $x_1 \to x_3 \to \bar x_2 \to x_1$ is another. So $$ \text{SCC } A = \set{\bar x_1,\ x_2,\ \bar x_3}, \qquad \text{SCC } B = \set{x_1,\ \bar x_2,\ x_3}. $$ No variable meets its own negation: $x_1 \in B$ while $\bar x_1 \in A$, and likewise for $x_2$ and $x_3$. The collision test passes on all three variables, so $\Phi$ is **satisfiable**. **Read the assignment.** The condensation has just two super-vertices, $A$ and $B$, joined by the cross edges $\bar x_1 \to x_1$ and $\bar x_3 \to x_1$, both running $A \to B$. So $B$ is topologically _later_ (the sink). The rule "assign true to whichever of $x_i$, $\bar x_i$ lies in the later SCC" makes every variable read straight off which component holds its positive literal: - $x_1 \in B$ (later) $\Rightarrow$ $x_1 = \text{true}$. - $x_2 \in A$ (earlier), so $\bar x_2 \in B$ is later $\Rightarrow$ $x_2 = \text{false}$. - $x_3 \in B$ (later) $\Rightarrow$ $x_3 = \text{true}$. **Check it.** The assignment $(x_1, x_2, x_3) = (\text{T}, \text{F}, \text{T})$ satisfies every clause: $(x_1 \vee x_2) = \text{T}$, $(\lnot x_1 \vee x_3) = (\text{F} \vee \text{T}) = \text{T}$, $(\lnot x_2 \vee \lnot x_3) = (\text{T} \vee \text{F}) = \text{T}$, and $(x_1 \vee x_3) = \text{T}$. No search was needed. For contrast, add the clause $(\lnot x_1 \vee \lnot x_3)$ — forbidding $x_1$ and $x_3$ from both being true. Its edges $x_1 \to \bar x_3$ and $x_3 \to \bar x_1$ now run $B \to A$, and the graph already had the cross edges $\bar x_1 \to x_1$ and $\bar x_3 \to x_1$ running $A \to B$. Edges in both directions collapse $A$ and $B$ into a single strongly connected component containing all six literals — in particular $x_1$ and $\bar x_1$ together. Once that happens the collision test fires and the formula is correctly reported unsatisfiable — no assignment can honor "$x_1$ or $x_2$", "$x_1$ or $x_3$", "not both $x_2$ and $x_3$", "$x_1 \Rightarrow x_3$", and "not both $x_1$ and $x_3$" at once. ::impl{algo="two_sat"} ## Where 2-SAT shows up The pattern to recognize is: each item has exactly **two states**, and the constraints are **pairwise**. Then every constraint becomes a two-literal clause and the whole problem becomes one implication graph. This covers a wide range: placing labels on a map so adjacent labels do not collide (each label goes left-or-right), scheduling tasks each offered in one of two slots, two-coloring under "these two must differ / must agree" rules, and consistency checking in hardware and program verification, where 2-SAT is a standard subroutine. _Pure_ 2-SAT rarely appears verbatim on LeetCode, but the implication-graph and pairwise- constraint shape is common: **Satisfiability of Equality Equations** is a union-find consistency check that is 2-SAT with only equalities and disequalities; **Possible Bipartition** asks for a two-coloring under "must differ" constraints, exactly the constraint-graph reduction; and **Divide Nodes Into the Maximum Number of Groups** layers a bipartiteness/BFS-distance argument on top. The implication-graph technique unifies these as one family, and in competitive programming and formal verification 2-SAT in its raw form is common too. ## The boundary of tractability 2-SAT is a boundary case: almost any modification of the problem is NP-hard. **The canonical linear algorithm.** The implication-graph reduction and the "later SCC wins" assignment rule are due to Aspvall, Plass, and Tarjan (1979), who packaged the whole thing as a single $O(n + m)$ procedure.[^apt] Their paper actually solves the more general **quantified** 2-SAT, but strip the quantifiers and what remains is the algorithm here: build $G$, one SCC pass, two scans. It remains the standard method, used verbatim in competitive programming and as a subroutine in SAT solvers' preprocessing. **Randomized 2-SAT.** A different linear-expected-time algorithm ignores the graph entirely. Papadimitriou's random-walk method starts from any assignment and, while some clause is unsatisfied, picks one and flips a _uniformly random_ one of its two literals.[^papadimitriou] Each flip is a step in a random walk on the number of variables that agree with a fixed satisfying assignment; because a two-literal clause guarantees at least a $\tfrac12$ chance of stepping _toward_ the target, the walk reaches a satisfying assignment in $O(n^2)$ expected flips. The same idea with three literals only steps toward the target with probability $\tfrac13$, and the walk drifts — this is why Schöning's randomized 3-SAT algorithm runs in exponential (though better-than-brute-force) time. **Everything nearby is hard.** The two-to-three-literal boundary is the most famous, but not the only one: - **3-SAT** is NP-complete (Cook-Levin), the archetypal hard problem of the [intractability](/algorithms/intractability/np-completeness) module. - **MAX-2-SAT** — satisfy as _many_ clauses as possible when you cannot satisfy them all — is NP-hard even though plain 2-SAT is easy; the Goemans-Williamson semidefinite-programming relaxation gives the best known approximation. - **Weighted / quantified** variants and counting the number of satisfying assignments (#2-SAT) are all intractable. $$ % caption: The tractability cliff. 2-SAT is in P (one SCC computation); MAX-2-SAT and 3-SAT % are NP-hard. The single extra literal, or the shift from "satisfy all" to % "satisfy the most", crosses the boundary. \begin{tikzpicture}[font=\small] \definecolor{acc}{HTML}{2348F2} \definecolor{hard}{HTML}{D1342B} \node[draw=acc, thick, fill=acc!10, minimum width=26mm, minimum height=11mm, align=center, font=\small] (p) at (0,0) {2-SAT\\ in P: $O(n+m)$}; \node[draw=hard, thick, fill=hard!8, minimum width=26mm, minimum height=11mm, align=center, font=\small] (h1) at (4.2,0.9) {MAX-2-SAT\\ NP-hard}; \node[draw=hard, thick, fill=hard!8, minimum width=26mm, minimum height=11mm, align=center, font=\small] (h2) at (4.2,-0.9) {3-SAT\\ NP-complete}; \draw[->, >=Stealth, hard, thick] (p.east) to[bend left=10] node[above, font=\scriptsize, black]{+"maximize"} (h1.west); \draw[->, >=Stealth, hard, thick] (p.east) to[bend right=10] node[below, font=\scriptsize, black]{+1 literal} (h2.west); \end{tikzpicture} $$ 2-SAT is a different problem from general SAT, not merely a smaller one: its special structure (every clause is an implication, so forcing is a reachability relation) is what collapses it into a graph question. Without that structure the problem is NP-hard. ## Takeaways - **2-SAT** (CNF satisfiability with **exactly two literals per clause**) is solvable in $O(n+m)$, unlike NP-complete **3-SAT**; the gap from two to three literals is the gap from polynomial to (conjecturally) exponential. - Each clause $(a \vee b)$ is the implication pair $\lnot a \Rightarrow b$ and $\lnot b \Rightarrow a$; collecting them builds a **skew-symmetric implication graph** on the $2n$ literals, where reachability = forcing. - **Satisfiability theorem:** $\Phi$ is satisfiable **iff** no variable shares an SCC with its own negation; a collision means $x \Rightarrow \lnot x$ and $\lnot x \Rightarrow x$, an outright contradiction. - An assignment is read straight off the **condensation DAG**: set each literal true iff its SCC is **topologically later** than its negation's; skew-symmetry proves this never violates an implication edge. - The whole algorithm is _one_ **strongly-connected-components computation** plus two linear scans, a direct payoff of the SCC machinery from the previous lesson. [^skiena-sat]: **Skiena**, § — Satisfiability: 2-SAT is polynomial via implication graphs, while general SAT and 3-SAT are NP-complete. [^erickson-scc]: **Erickson**, Ch. — Strong Connectivity / Applications: the implication-graph reduction and the SCC characterization of 2-SAT satisfiability. [^clrs-scc]: **CLRS**, Ch. 20 — (SCC applications): strongly connected components and the condensation DAG, the substrate the 2-SAT assignment rule runs on. [^apt]: **Aspvall, B., Plass, M. F. & Tarjan, R. E.** (1979), "A linear-time algorithm for testing the truth of certain quantified boolean formulas," _Information Processing Letters_ 8(3), 121–123 — the implication-graph SCC algorithm for 2-SAT. [^papadimitriou]: **Papadimitriou, C. H.** (1991), "On selecting a satisfying truth assignment," _Proc. FOCS 1991_, 163–169 — the random-walk algorithm solving 2-SAT in expected $O(n^2)$ time.