# Solving 2-CNF-SAT in Linear Time

This is one last question from quora. While I sometimes worry that 95% of the math and computer science questions on the site are students' homework problems, reviewing the algorithm to solve 2-CNF-SAT is a good reminder that there are often fast algorithms to solve "low-dimensional" forms.

## Question

What is the algorithm that solves 2-CNF in a polynomial running time? And what is its exact running time polynomial order?

Say we have a clause in our 2-CNF-SAT instance that looks like this: $(x_i \vee x_j)$. We can turn this clause into the equivalent logical implication $(\neg x_i \Rightarrow x_j)$. Since implication is transitive, if we have clauses $(\neg x_i \Rightarrow x_j)$ and $(x_j \Rightarrow x_k)$, then a satisfying assignment must also satisfy $(\neg x_i \Rightarrow x_k)$ even if that clause isn’t explicitly present in our formula.
We can use this idea to prove that some instances definitely aren’t satisfiable. If this "chaining" of implications produces both $(x_i \Rightarrow \neg x_i)$ and $(\neg x_i \Rightarrow x_i)$ for some variable $x_i$, then we know that the formula can’t be satisfiable. We can’t make both of these conditions true at the same time. As it turns out, if we don’t have this double implication between any variable and its negation, the formula is satisfiable.
There are a few algorithms which we can construct to detect our condition. My favorite is from Aspvall, Plass, and Tarjan (1979). Construct a graph with one vertex for each variable and one vertex for each variable’s negation. Add directed edges between the vertices according to the implication rules in your formula. For instance, if the formula contains the clause $(x_i \Rightarrow \neg x_j)$, then the graph should have a directed edge from vertex $x_i$ to vertex $\neg x_j$.