SAT

In its general form, SAT concerns an expression in CNF (Conjunctive Normal Form). It’s many clauses, ANDed (∧) together. Each clause is a disjunction, a number of literals (variables or negated (¬) variables) ORed (∨) together.


    (a ∨ b ∨ c) ∧ (a ∨ b ∨ ¬c ∨ d) ∧ (c ∨ d) ∧ (b)

SAT ⇒ 3SAT

Say we have an arbitrary expression:


    (a ∨ b ∨ c) ∧ (a ∨ b ∨ ¬c ∨ d) ∧ (c ∨ d) ∧ (b)

It’s CNF, but not 3-CNF. We want 3-CNF, because we want to work with 3SAT, which is easier than SAT. We want each disjunctive clause to be three exactly elements. How can we convert CNF to 3-CNF? There are several cases to consider:

clauses with one element
clauses with two elements
clauses with three elements
clauses with more than three elements

Clause with one element

If we have a clause with one element, (b), we introduce a new variable x, and rewrite the single-element clause thus:


    (b) ≡ (b ∨ x) ∧ (b ∨ ¬x)

If x=0 (false), then this reduces to

(b) ≡ (b ∨ 0) ∧ (b ∨ ¬0)
(b) ≡ (b) ∧ (b ∨ ¬0)
(b) ≡ (b) ∧ (b ∨ 1)
(b) ≡ (b) ∧ (1)
(b) ≡ (b)

If x=1 (true), then this reduces to

(b) ≡ (b ∨ 1) ∧ (b ∨ ¬1)
(b) ≡ (1) ∧ (b ∨ ¬1)
(b) ≡ (b ∨ ¬1)
(b) ≡ (b ∨ 0)
(b) ≡ (b)

∴, (b) ≡ (b ∨ x) ∧ (b ∨ ¬x). Hooray! We’ve converted a one-element clause into two two-element clauses.

Or, you can just convert (b) to (b ∨ 0), if you allow boolean constants instead of literals. Or even (b ∨ b).

Clause with two elements

If we have a clause with two elements, (c ∨ d), we introduce a new variable y, and rewrite the single-element clause thus:


    (c ∨ d) ≡ (c ∨ d ∨ y) ∧ (c ∨ d ∨ ¬y)

If y=0 (false), then this reduces to

(c ∨ d) ≡ (c ∨ d ∨ 0) ∧ (c ∨ d ∨ ¬0)
(c ∨ d) ≡ (c ∨ d) ∧ (c ∨ d ∨ ¬0)
(c ∨ d) ≡ (c ∨ d) ∧ (c ∨ d ∨ 1)
(c ∨ d) ≡ (c ∨ d) ∧ (1)
(c ∨ d) ≡ (c ∨ d)

If y=1 (true), then this reduces to

(c ∨ d) ≡ (c ∨ d ∨ 1) ∧ (c ∨ d ∨ ¬1)
(c ∨ d) ≡ (1) ∧ (c ∨ d ∨ ¬1)
(c ∨ d) ≡ (c ∨ d ∨ ¬1)
(c ∨ d) ≡ (c ∨ d ∨ 0)
(c ∨ d) ≡ (c ∨ d)

∴, (c ∨ d) ≡ (c ∨ d ∨ y) ∧ (c ∨ d ∨ ¬y). Hooray! We’ve converted a two-element clause into two three-element clauses.

Clause with three elements

Great!

Clause with more than three elements

Lemma: if the formula (A ∨ B) is satisfiable, that is, if there is a truth-assignment to A and B such that (A ∨ B) is true, then the formula (A ∨ z) ∧ (B ∨ ¬z), where z is a new variable, is satisfiable. This is true even if A and B are not simple variables, but instead expressions.

Think of it this way:

If (A ∨ B) is true, then either A is true, or B is true (or maybe both).
If A is true, then let z=0, which yields: (A ∨ 0) ∧ (B ∨ ¬0), which is true.
If B is true, then let z=1, which yields: (A ∨ 1) ∧ (B ∨ ¬1), which is true.
If A and B are both false, then (A ∨ B) is false. (A ∨ z) ∧ (B ∨ ¬z) ⇒ (0 ∨ z) ∧ (0 ∨ ¬z) ⇒ z ∧ ¬z ⇒ false.

Or, as a truth table:

A	B	A ∨ B	A ∨ z	B ∨ ¬z	(A ∨ z) ∧ (B ∨ ¬z)
0	0	0	z	¬z	0
0	1	1	z	1	z
1	0	1	1	¬z	¬z
1	1	1	1	1	1

The last column is satisfiable, by an appropriate assignment to z, in all rows except the first one, where A ∨ B itself is not satisfiable. Therefore, the formulas A ∨ B and (A ∨ z) ∧ (B ∨ ¬z) have equal satisfiability.

This lets us break a lengthy clause into two smaller clauses. We can pull the last two components of the lengthy clause into a separate clause of length 3, replacing them with a new variable. This reduces the length of the first clause by one element. Rinse & repeat.

(a ∨ b ∨ c ∨ d) ⇒ (a ∨ b ∨ z) ∧ (c ∨ d ∨ ¬z)
(a ∨ b ∨ c ∨ d ∨ e) ⇒ (a ∨ b ∨ c ∨ z) ∧ (d ∨ e ∨ ¬z)
(a ∨ b ∨ c ∨ d ∨ e ∨ f) ⇒ (a ∨ b ∨ c ∨ d ∨ z) ∧ (e ∨ f ∨ ¬z)