# Time complexity of solving a set of 2-sat instances?

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?

• 2-SAT (wiki) can be solved in polynomial time. Dec 17, 2014 at 3:45
• So if n is the number of variables and m is the number of clauses, what is the complexity in big O? I also read the same article but could not find a complexity. Dec 17, 2014 at 3:48
• By the SCC algorithm, the 2-SAT instance is modeled by a directed graph, in which there is one vertex per variable or negated variable, and an edge connecting one vertex to another whenever the corresponding variables are related by an implication in the implicative normal form of the instance. The SCC algorithm itself can be solved by two DFS procedures, in $O(|V|+|E|)$ time. Dec 17, 2014 at 4:00
• @hengxin Make an answer? Dec 17, 2014 at 6:33
• @YuvalFilmus I am not sure whether it is the answer the OP is asking for because the question mentions the fastest known 2SAT solver. Anyway, I have converted my comment into an answer. Dec 17, 2014 at 8:33

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: