[proofplan] We give a deterministic polynomial-time decision algorithm for $\mathrm{2SAT}$. Given a 2-CNF formula, we build its implication graph, where each clause $a \lor b$ is represented by the implications $\neg a \to b$ and $\neg b \to a$. The formula is unsatisfiable exactly when some literal and its negation lie in the same strongly connected component. If no such conflict occurs, a topological ordering of the component condensation graph produces a satisfying assignment. [/proofplan] [step:Build the implication graph from the clauses] Let $\varphi$ be a 2-CNF formula with variables $x_1,\dots,x_n$ and clauses $C_1,\dots,C_m$. First inspect the clauses of $\varphi$. If some clause has no literals, then that clause is the empty disjunction, which is false under every truth assignment; in this case the algorithm rejects immediately. For the rest of the construction, assume every clause has one or two literals. Let $L$ be the set of literals \begin{align*} L := \{x_1,\neg x_1,\dots,x_n,\neg x_n\}. \end{align*} For a literal $\ell \in L$, write $\bar{\ell}$ for its complementary literal, so $\bar{x_i}=\neg x_i$ and $\overline{\neg x_i}=x_i$. Define the implication graph of $\varphi$ to be the directed graph \begin{align*} G_\varphi := (V,E) \end{align*} with vertex set $V=L$. For each clause $C_j = (a_j \lor b_j)$, where $a_j,b_j \in L$, put the two directed edges \begin{align*} \bar{a_j} \to b_j \end{align*} and \begin{align*} \bar{b_j} \to a_j \end{align*} into $E$. If a clause has one literal $a_j$, regard it as $(a_j \lor a_j)$, which adds the implication $\bar{a_j}\to a_j$. The graph $G_\varphi$ has $2n$ vertices and at most $2m$ edges, so it can be constructed in time polynomial in the length of the input encoding of $\varphi$. [/step] [step:Relate clauses to implications] For every truth assignment $\alpha:L\to\{\mathrm{true},\mathrm{false}\}$ satisfying $\alpha(\bar{\ell})=\neg\alpha(\ell)$ for all $\ell\in L$, a clause $(a\lor b)$ is satisfied by $\alpha$ if and only if both implications $\bar a\to b$ and $\bar b\to a$ are satisfied by $\alpha$. Indeed, if $(a\lor b)$ is false, then $a$ and $b$ are both false, so $\bar a$ and $\bar b$ are both true. Hence both implications have true hypotheses and false conclusions. Conversely, if $\bar a\to b$ is false, then $\bar a$ is true and $b$ is false, so $a$ is false and $b$ is false; thus $(a\lor b)$ is false. The same argument applies to $\bar b\to a$. Therefore $\alpha$ satisfies $\varphi$ if and only if $\alpha$ satisfies every directed edge of $G_\varphi$, in the sense that no edge $u\to v$ has $\alpha(u)=\mathrm{true}$ and $\alpha(v)=\mathrm{false}$. [guided] The implication graph is useful because a clause with two literals is equivalent to two one-way logical constraints. Fix a truth assignment \begin{align*} \alpha:L\to\{\mathrm{true},\mathrm{false}\} \end{align*} such that $\alpha(\bar{\ell})=\neg\alpha(\ell)$ for each literal $\ell\in L$. Consider one clause $(a\lor b)$. This clause fails exactly when both literals are false: \begin{align*} \alpha(a)=\mathrm{false} \end{align*} and \begin{align*} \alpha(b)=\mathrm{false}. \end{align*} The first equality means $\alpha(\bar a)=\mathrm{true}$, and the second says the conclusion $b$ is false. Hence the implication $\bar a\to b$ is false. Similarly, $\alpha(\bar b)=\mathrm{true}$ and $\alpha(a)=\mathrm{false}$, so $\bar b\to a$ is false. Conversely, suppose the implication $\bar a\to b$ is false. An implication is false only when its hypothesis is true and its conclusion is false, so \begin{align*} \alpha(\bar a)=\mathrm{true} \end{align*} and \begin{align*} \alpha(b)=\mathrm{false}. \end{align*} Since $\alpha(\bar a)=\neg\alpha(a)$, this gives $\alpha(a)=\mathrm{false}$. Thus both $a$ and $b$ are false, and the clause $(a\lor b)$ is false. The implication $\bar b\to a$ gives the same conclusion by exchanging $a$ and $b$. Thus satisfying all clauses is exactly the same as satisfying all directed implications in $G_\varphi$. [/guided] [/step] [step:Detect unsatisfiability from a complementary pair in one strongly connected component] Suppose there exists an index $i\in\{1,\dots,n\}$ such that $x_i$ and $\neg x_i$ lie in the same strongly connected component of $G_\varphi$. Then there is a directed path from $x_i$ to $\neg x_i$ and a directed path from $\neg x_i$ to $x_i$. Let $\alpha$ be any assignment satisfying all implications in $G_\varphi$. Along any directed edge $u\to v$, if $\alpha(u)=\mathrm{true}$ then $\alpha(v)=\mathrm{true}$. By induction along a directed path, truth propagates from the first vertex of the path to the last vertex. If $\alpha(x_i)=\mathrm{true}$, the path from $x_i$ to $\neg x_i$ forces $\alpha(\neg x_i)=\mathrm{true}$, contradicting $\alpha(\neg x_i)=\neg\alpha(x_i)$. If $\alpha(x_i)=\mathrm{false}$, then $\alpha(\neg x_i)=\mathrm{true}$, and the path from $\neg x_i$ to $x_i$ forces $\alpha(x_i)=\mathrm{true}$, again a contradiction. Hence no satisfying assignment exists. [/step] [step:Construct an assignment when no complementary pair lies in one component] Assume now that, for every $i\in\{1,\dots,n\}$, the literals $x_i$ and $\neg x_i$ lie in distinct strongly connected components of $G_\varphi$. Let $\mathcal{C}$ be the set of strongly connected components of $G_\varphi$. Define the condensation graph \begin{align*} D_\varphi := (\mathcal{C},E_{\mathcal{C}}) \end{align*} by putting an edge $A\to B$ in $E_{\mathcal{C}}$ whenever $A,B\in\mathcal{C}$, $A\neq B$, and there exist literals $u\in A$ and $v\in B$ with $u\to v$ in $G_\varphi$. The graph $D_\varphi$ is acyclic by maximality of strongly connected components. Choose a topological ordering of $\mathcal{C}$, and let \begin{align*} \tau:\mathcal{C}\to\{1,\dots,|\mathcal{C}|\} \end{align*} denote its rank function, chosen so that $A\to B$ in $D_\varphi$ implies $\tau(A)<\tau(B)$. For each literal $\ell\in L$, let $[\ell]\in\mathcal{C}$ denote the strongly connected component containing $\ell$. Define the assignment $\alpha:L\to\{\mathrm{true},\mathrm{false}\}$ by \begin{align*} \alpha(\ell)=\mathrm{true} \quad \Longleftrightarrow \quad \tau([\ell])>\tau([\bar{\ell}]). \end{align*} This is well-defined as a Boolean assignment on variables because $[\ell]\neq[\bar{\ell}]$ by assumption, so exactly one of $\tau([\ell])>\tau([\bar{\ell}])$ and $\tau([\bar{\ell}])>\tau([\ell])$ holds. Therefore $\alpha(\bar{\ell})=\neg\alpha(\ell)$ for every literal $\ell\in L$. [/step] [step:Show the topological-order assignment satisfies every implication] Let $u\to v$ be an arbitrary edge of $G_\varphi$. We prove that $\alpha(u)=\mathrm{true}$ implies $\alpha(v)=\mathrm{true}$. Assume, for contradiction, that \begin{align*} \alpha(u)=\mathrm{true} \end{align*} and \begin{align*} \alpha(v)=\mathrm{false}. \end{align*} By the definition of $\alpha$, \begin{align*} \tau([u])>\tau([\bar u]) \end{align*} and \begin{align*} \tau([v])<\tau([\bar v]). \end{align*} The edge $u\to v$ gives either $[u]=[v]$ or an edge $[u]\to[v]$ in the condensation graph. Hence \begin{align*} \tau([u])\le \tau([v]). \end{align*} Because every edge in the implication graph comes from a clause together with its contrapositive companion, the edge $u\to v$ is accompanied by the edge $\bar v\to \bar u$. Therefore the same condensation argument gives \begin{align*} \tau([\bar v])\le \tau([\bar u]). \end{align*} Combining the four inequalities yields \begin{align*} \tau([u])\le \tau([v])<\tau([\bar v])\le \tau([\bar u])<\tau([u]). \end{align*} This is impossible. Hence no edge $u\to v$ has $\alpha(u)=\mathrm{true}$ and $\alpha(v)=\mathrm{false}$. By the equivalence between clauses and implications proved above, $\alpha$ satisfies every clause of $\varphi$. [/step] [step:Conclude the algorithm runs in polynomial time] The decision algorithm is now explicit: first reject if $\varphi$ contains an empty clause; otherwise construct $G_\varphi$, compute its strongly connected components, reject if some $x_i$ and $\neg x_i$ lie in the same component, and otherwise accept. The implication graph has $2n$ vertices and at most $2m$ edges. Strongly connected components of a finite directed graph can be computed in time linear in the number of vertices plus the number of edges, for example by depth-first search. The remaining checks compare the component labels of $x_i$ and $\neg x_i$ for $i=1,\dots,n$, which takes linear time in $n$. Thus the entire algorithm runs in time polynomial in the input size of $\varphi$. It accepts exactly the satisfiable 2-CNF formulas, so $\mathrm{2SAT}\in\mathrm{P}$. [/step]