2-CNF satisfiability
A 2-CNF formula is one where each clause has two literals. One can show that the satisfiability of 2-CNF is polynomial-time, as follows:
-
Consider one of the clauses l1 ∨ l2. This can be written as two implications, (¬l1 ⇒ l2) and (¬l2 ⇒ l1).
-
The complete algorithm is to process each clause of a 2-CNF formula into such a pair of implications. Now, viewing each such implication as a graph edge, we can connect its source to its destination; for example, in (¬l1 ⇒ l2), connect node ¬l1 to node l2. In any situation, if a double negation is introduced, as in ¬¬a, we must simplify it to a before proceeding.
-
Finally, we connect pairs of edges such that the destination vertex of one edge is the source vertex of the other. For example, if (¬l1 ⇒ l2) is an edge, and (l2 ⇒ l3) is another edge, connect these edges at the common point l2.
Now, the following results can be shown:
-
If the graph resulting from the above construction is cyclic and a cycle includes p and ¬p for some literal p, the formula is unsatisfiable.
-
If this situation does not arise, we can perform a value assignment to the variables (find a satisfying assignment) as follows:
– If a literal x (for variable x) is followed by literal ¬x in the graph, assign x false.
– If a literal ¬x (for variable x) is followed by x in the graph, assign x true.
– Else assign x arbitrarily.
