2
$\begingroup$

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?

$\endgroup$
6
  • 1
    $\begingroup$ 2-SAT (wiki) can be solved in polynomial time. $\endgroup$
    – hengxin
    Dec 17 '14 at 3:45
  • $\begingroup$ 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. $\endgroup$
    – chibro2
    Dec 17 '14 at 3:48
  • 1
    $\begingroup$ 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. $\endgroup$
    – hengxin
    Dec 17 '14 at 4:00
  • $\begingroup$ @hengxin Make an answer? $\endgroup$ Dec 17 '14 at 6:33
  • $\begingroup$ @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. $\endgroup$
    – hengxin
    Dec 17 '14 at 8:33
4
$\begingroup$

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:

2sat

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.