[Solved]: Time complexity of solving a set of 2-sat instances?

Problem Detail: 

Suppose I have a set of 2-SAT instances, the set is of size $2^{3C}$ for some constant $C$. What is the time complexity of solving all instances using the fastest known 2-SAT solver?

Asked By : chibro2

Answered By : hengxin

Although 3SAT problem is NP-complete, there is a polynomial algorithm making use of the beautiful SCC (Strongly Connected Component) directed graph algorithm.

Suppose there are $n$ variables and $m$ clauses in the 2SAT instance $\mathcal{I}$. The parameters $n$ and $m$ represent the size of $\mathcal{I}$

The 2-SAT instance is modeled by a directed graph $\mathcal{G_I}$, with

• $2n$ vertices: for each variable $x$ in $\mathcal{I}$, there are two vertices $v_x$ and $v_{\bar{x}}$ (i.e., variable and its negation).
• $2m$ edges: for each clause $x \lor y$, there are two directed edges $\bar{x} \to y$ and $\bar{y} \to x$. Note that the latter two implicative forms are equivalent to $x \lor y$.

The polynomial algorithm (it is actually a linear algorithm) proceeds as follows:

1. Obtain the SCCs of $\mathcal{G_{I}}$ in linear time $O(n + m)$;
2. Assign True to each literal (Notice: not the variable) in the destination SCC (denoted $SCC_d$);
3. Delete $SCC_d$ and its corresponding source SCC ($SCC_s$). (Note the symmetry in the graph $\mathcal{G_{I}}$);
4. Repeat (2) and (3) until $\mathcal{G_{I}}$ is empty.

For example:

$\mathcal{I} = (x_1 \lor x_2) \land (\bar{x_2} \lor x_3) \land (\bar{x_1} \lor \bar{x_2}) \land (x_3 \lor x_4) \land (\bar{x_3} \lor x_5) \land (\bar{x_4} \lor \bar{x_5}) \land (\bar{x_3} \lor x_4)$

The graph $\mathcal{G_{I}}$ is:

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/35425