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.
Variables: taking values True or False
Operators: OR, AND.
Clause is an OR of several literals. Example: .
Boolean formula is in conjunctive normal form (CNF) means that it is the AND of such clauses. Example: .
Input: given formula in CNF with variables and clauses.
Output: assignment satisfying if one exists, and NO if no satisfying assignment exists.
k-SAT: same as SAT but the input has clauses with literals in each. We’ll see that SAT is NP-complete and k-SAT is NP-complete for each .
2-SAT has a polynomial-time algorithm.
Simplifying the input.
Take input 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 , take a unit clause, say literal :
- satisfy this clause by setting
- remove all clauses containing (these are all satisfied)
- drop any occurrences of .
Let be the resulting formula.
Observation: is satisfiable 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.
Take with clauses of size exactly 2, and variables and clauses. Create a directed graph as follows:
- vertices corresponding to
- edges corresponding to 2 “implications” per clause
- if then we need to set to satisfy this clause.
- if then we need .
- so we include edges and .
- In general for clause , add edges and .
Example: . (see PDF for the graph). Note path . So if then we need (i.e., ), contradiction. But if then we can set and be anything to satisfy .
Note: a path means setting we must also set . Thus if there’s a path then we can’t set and satisfy . Similarly if there’s a path . Therefore if and are in the same SCC, then is unsatisfiable.
Lemma: is satisfiable and are in different SCC’s.
We just argued that if where and are in the same SCC, then is unsatisfiable. Thus we proved . We now need to show which we’ll do by giving an algorithm.
Key idea: take a sink SCC and set (by satisfying all literals in ). Note that has no outgoing edges so no implications from setting . But we’ve also set (does have incoming edges?)
Take a source SCC and set . Note that has no incoming edges so we’ll never be forced to set to T. But we’ve also set (does have outgoing edges?)
Key Lemma: is a sink SCC is a source SCC.
So we take a sink SCC :
- set (and thus )
- remove and
- repeat until empty graph
This is valid because no variable has and in the same SCC. Just need to prove the lemma now.
Claim: . ( means a path)
Proof: for : suppose path is where and . Note that the edge comes form the clause and the other edge is . Thus we have the path where and .
For , similarly we can construct a path from a path .
Take SCC . For , there are paths and . Thus there’s also paths and . So and are in the same SCC . Therefore is a SCC. So S is a SCC is a SCC.
Moreover, has no incoming edges (so source SCC) if and only if S has no outgoing edges (sink SCC). This proves the key lemma.