Complexity Theory, Three-Sat and Two-Sat

Three-Sat

Restricted versions of the satisfiability problem are just as powerful, and often prove useful when showing other problems are np complete.

Given a boolean expression, use demorgan's laws to pull nots down to variables. Then convert to conjunctive normal form by a bottom-up recursive process. If two substrings are in cnf and they are anded, just and all their clauses together. If two substrings are ored, introduce a new variable y, and combine the clauses of the first ored with y, and the clauses of the second ored with ~y. If y is true all clauses in the second string must be true, or, if y is false all clauses in the first string must be true. Here is an example.

(a|b|c & ~a|b|~c) | (d|e|c & b|~e|~d)

y|a|b|c & y|~a|b|~c & ~y|d|e|c & ~y|b|~e|~d

If a clause comes up short, i.e. fewer than 3 atoms, you can (optionally) pad the clause using additional variables. For instance, c|d can become y|c|d & ~y|c|d. Thus every clause has at least three atoms. Some versions of 3-sat make this a requirement; others don't mind some shorter clauses floating about.

Break longer clauses up into packets of size 3 by introducing new variables. For instance, a|b|c|d|e becomes a|b|x & ~x|c|y & ~y|d|e. The result is a conjuction of clauses, each with three atoms or less. This is an instance of 3-sat.

Of course an instance of 3-sat is a boolean expression, which is an np problem. Conversely, converting an arbitrary boolean expression to an equivalent 3-sat instance can be done in polynomial time, hence 3-sat is np complete.

Clearly four-sat and higher are also np complete.

Two-Sat

In contrast, 2-sat is a tractable problem. First gather the singleton clauses and assign values to variables accordingly. Substitute these values throughout, gather more singleton clauses, and repeat until each clause has two atoms. Don't forget to watch for contradictions along the way. If c stands alone, it has to be true, and when you replace c with 1 throughout, the singleton clause ~c, if it exists, drops to 0, and that kills the entire expression.

Now every clause has two atoms. The clause ~a|b means a implies b and ~b implies ~a. Create a matrix of variables and their complements implying variables and their complements, and take the transitive closure. If a variable implies its negation then the negation must be true. Substitute throughout and begin again, watching for contradictions.

Assume there are no contradictions, and an implication path never carries c to ~c, or ~c to c. Suppose an implication cycle exists, e.g. a→b→c→d→a. realize that all the atoms in the cycle must be equal. Giving any variable in this cycle a value assigns values to all of them. In this case we would replace b c and d with a throughout, and start again. Continue this process until there are no more variables, or no cycles.

Assume the logical implications determine directed arcs that never form cycles. If a is the root of an implication tree let a be true. Let a be false if ~a leads an implication tree. Traverse the tree and fill in the values implied by the value assigned to a. Then move to the start of another implication tree and repeat until all variables are set.

Suppose you have the arcs a implies b and c implies ~b, and you assigned true to a and c, yielding the contradiction b&~b. This is imposssible since c implies ~b means b implies ~c. When a is set to true then b is set to true and c is set to false. When you move to a new tree, the implications hit new variables, or they consistently reassign values to old variables. The assignments cannot create a contradiction, hence the original 2-sat instance is satisfied.