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:

(x_{0} OR x_{1}) AND (~x_{0} OR x_{2}) AND (~x_{1} OR ~x_{2})

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:

- Create the inference graph G such that for each variable x
_{i} in the 2-SAT instance, x_{i} and ~x_{i} are vertices of the inference graph. x_{i} and ~x_{i} are complements of each other.
- For each clause (u OR v), add the edges ~u -> v and ~v -> u to the inference graph G.
- 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.
- 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.

28.635308
77.224960

### Like this:

Like Loading...

*Related*

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