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?

Answer

Let’s first talk about 2-CNF-SAT. That is, the problem of determining whether a 2-CNF formula has a satisfying assignment. We need a couple of ideas which we can tie together into an algorithm.

Say we have a clause in our 2-CNF-SAT instance that looks like this: (xixj)(x_i \vee x_j). We can turn this clause into the equivalent logical implication (¬xixj)(\neg x_i \Rightarrow x_j). Since implication is transitive, if we have clauses (¬xixj)(\neg x_i \Rightarrow x_j) and (xjxk)(x_j \Rightarrow x_k), then a satisfying assignment must also satisfy (¬xixk)(\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 (xi¬xi)(x_i \Rightarrow \neg x_i) and (¬xixi)(\neg x_i \Rightarrow x_i) for some variable xix_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 (xi¬xj)(x_i \Rightarrow \neg x_j), then the graph should have a directed edge from vertex xix_i to vertex ¬xj\neg x_j.

If this graph contains a strongly connected component which contains any variable and its negation, the original formula is not satisfiable (by our condition above). If the graph contains no such component, then the formula is satisfiable. Thankfully, there are fast algorithms to detect strongly connected components in directed graphs, so we can do all of this in time linear in the size of the graph.

Now, constructing a satisfying assignment if one exists is a bit more complicated. You can refer to the linked paper for this algorithm or find a summary here, but it requires a few other tools that are a bit outside of the scope of the question (e.g. skew symmetric graphs). However, you can find this satisfying assignment in linear time, too.