Solving 2-SAT in linear time

2-Satisfiability (2-SAT) is the problem of determining whether a collection of boolean variables with constraints on pairs of variables can be assigned values satisfying all the constraints. Although 3-SAT is NP complete, 2-SAT can be solved in linear time.

A 2-SAT instance can be described using 2-CNF as follows:

(x0 OR x1) AND (~x0 OR x2) AND (~x1 OR ~x2)

The 2-SAT problem is to find a truth assignment to these variables that makes a formula of this type true: we must choose whether to make each of the variables true or false, so that every clause has at least one term that becomes true.

Aspvall, Plass & Tarjan (1979) found a simple linear time procedure for solving 2-SAT instances, based on the notion of strongly connected components. The algorithm is as follows:

  1. Create the inference graph G such that for each variable xi in the 2-SAT instance, xi and ~xi are vertices of the inference graph. xi and ~xi are complements of each other.
  2. For each clause (u OR v), add the edges ~u -> v and ~v -> u to the inference graph G.
  3. Process the strongly connected components S of G in reverse topological order as follows: If S is marked, do nothing. If S = ~S (i.e., a variable and its complement belong to the same SCC), then stop, the instance is unsatisfiable. Otherwise, mark S true and ~S false.
  4. We get a satisfying assignment by assigning to each variable the truth value of the component containing it.

Take a look at the C++ implementation.

One thought on “Solving 2-SAT in linear time

  1. Pingback: Strongly Connected Components in a Directed Graph C++ implementation | Everything Under The Sun

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s