GA: 2-SAT

PDF of Eric’s handwritten notes are here.

In this lecture we’ll present a poly-time algorithm for determining if a 2-SAT formula is satisfiable using the SCC algorithm from last class.  Let’s begin with a review of the terminology.

Boolean formula

Variables: x_1, x_2,\dots,x_n taking values True or False

Literals: x_1,\overline{x_1},x_2,\overline{x_2},\dots,x_n,\overline{x_n}.

Operators: \vee= OR, \wedge= AND.

Clause is an OR of several literals. Example: (\overline{x_3}\vee x_5\vee\overline{x_2}\vee x_1).

Boolean formula f is in conjunctive normal form (CNF) means that it is the AND of m such clauses. Example: (x_2)\wedge(\overline{x_3}\vee x_5\vee\overline{x_2}\vee x_1)\wedge(\overline{x_2}\vee\overline{x_1}).

SAT

Input: given formula f in CNF with n variables and m clauses.

Output: assignment satisfying f if one exists, and NO if no satisfying assignment exists.

k-SAT: same as SAT but the input f has clauses with \le k literals in each. We’ll see that SAT is NP-complete and k-SAT is NP-complete for each k\ge 3.

2-SAT has a polynomial-time algorithm.

Simplifying the input.

Take input f for 2-SAT. We’ll assume all clauses have size exactly 2. What about clauses of size 1?  A clause of size 1 is called a `unit clause’.

For f, take a unit clause, say literal a_i:

  • satisfy this clause by setting a_i=T
  • remove all clauses containing a_i (these are all satisfied)
  • drop any occurrences of \overline{a_i}.

Let f' be the resulting formula.
Observation: f is satisfiable \Leftrightarrow f' is satisfiable.

Thus we can repeat the above procedure until all unit clauses are eliminated.  Then we are left with a formula where all clauses are of size exactly 2, or we have some empty clauses (the clauses were never eliminated but the literals were dropped).  If we have an empty clause then the formula is not satisfiable, so we just output NO.

Graph representation.

Take f with clauses of size exactly 2, and n variables and m clauses. Create a directed graph as follows:

  • 2n vertices corresponding to x_1, \overline{x_1},x_2,\overline{x_2},\dots,x_n,\overline{x_n}
  • 2m edges corresponding to 2 “implications” per clause
  • example: (x_i\vee\overline{x_j})
    • if x_i=F then we need to set x_j=F to satisfy this clause.
    • if x_j=T then we need x_i=T.
    • so we include edges \overline{x_i}\rightarrow\overline{x_j} and x_j\rightarrow x_i.
  • In general for clause (\alpha\vee\beta), add edges \overline{\alpha}\rightarrow\beta and \overline{\beta}\rightarrow\alpha.

Example: f=(\overline{x_1}\vee\overline{x_2})\wedge(x_2\vee x_3)\wedge(\overline{x_3}\vee\overline{x_1}). (see PDF for the graph). Note path x_1\rightarrow\overline{x_2}\rightarrow x_3\rightarrow\overline{x_1}. So if x_1=T then we need \overline{x_1}=T (i.e., x_1=F), contradiction. But if x_1=F then we can set x_2=T and x_3 be anything to satisfy f.

Note: a path x_i \leadsto x_j means setting x_i=T we must also set x_j=T. Thus if there’s a path x_i\leadsto\overline{x_i} then we can’t set x_i=T and satisfy f. Similarly if there’s a path \overline{x_i}\leadsto x_i. Therefore if x_i and \overline{x_i} are in the same SCC, then f is unsatisfiable.

Lemma: f is satisfiable  \Leftrightarrow\ \forall_i, x_i and \overline{x_i} are in different SCC’s.

We just argued that if \exists_i where x_i and \overline{x_i} are in the same SCC, then f is unsatisfiable. Thus we proved \Rightarrow. We now need to show \Leftarrow which we’ll do by giving an algorithm.

Key idea: take a sink SCC S and set S=T (by satisfying all literals in S). Note that S has no outgoing edges so no implications from setting S=T. But we’ve also set \overline{S}=F (does \overline{S} have incoming edges?)

Take a source SCC S' and set S'=F. Note that S' has no incoming edges so we’ll never be forced to set S' to T. But we’ve also set \overline{S'}=T (does \overline{S'} have outgoing edges?)

Key Lemma: S is a sink SCC \Leftrightarrow\ \overline{S} is a source SCC.

So we take a sink SCC S:

  • set S=T (and thus \overline{S}=F)
  • remove S and \overline{S}
  • repeat until empty graph

This is valid because no variable x_i has x_i and \overline{x_i} in the same SCC. Just need to prove the lemma now.

Claim: \alpha\leadsto\beta\Leftrightarrow\overline{\beta}\leadsto\overline{\alpha}. (\leadsto means a path)

Proof: for \Rightarrow: suppose path \alpha\leadsto\beta is \gamma_0\rightarrow\gamma_1\rightarrow\cdots\rightarrow\gamma_l where \gamma_0=\alpha and \gamma_l=\beta. Note that the edge \gamma_i\rightarrow\gamma_{i+1} comes form the clause (\overline{\gamma_i}\vee\gamma_{i+1}) and the other edge is \overline{\gamma_{i+1}}\rightarrow\overline{\gamma_i}. Thus we have the path \overline{\gamma_l}\rightarrow\overline{\gamma_{i-1}}\rightarrow\cdots\rightarrow\overline{\gamma_0} where \overline{\gamma_l}=\overline{\beta} and \overline{\gamma_0}=\overline{\alpha}.

For \Leftarrow, similarly we can construct a path \alpha\leadsto\beta from a path \overline{\beta}\leadsto\overline{\alpha}.  \Box

Take SCC S. For \alpha,\beta\in S, there are paths \alpha\leadsto\beta and \beta\leadsto\alpha. Thus there’s also paths \overline{\beta}\leadsto\overline{\alpha} and \overline{\alpha}\leadsto\overline{\beta}. So \overline{\alpha} and \overline{\beta} are in the same SCC S'. Therefore \overline{S} is a SCC. So S is a SCC \Leftrightarrow\ \overline{S} is a SCC.

Moreover, \overline{S} has no incoming edges (so source SCC) if and only if S has no outgoing edges (sink SCC). This proves the key lemma.