Discrete Mathematics
This is a preserved file from cs2102 Fall 2016. An updated version may exist at https://uvacs2102.github.io/

Three-Clause Challenge Refuted!


Challenge 5 has been refuted by Henry Spece!

Challenge 5. (From PS3 Solutions) Prove that the four-clause solution given for question 6 is the shortest possible equivalent 3CNF formula.

The challenge as stated was actually bogus! The four-clause solution isn’t the shortest possible equivalent 3CNF formula. Henry found a three-clause equivalent 3CNF formula, and proved that there is no two-clause equivalent 3CNF formula.

His answer is below:

The four-clause 3-CNF equivalent solution to the logical equation is not the smallest equivalent solution to the equation.

The following is the original formula: A ∨ ¬BC ∨ (¬DE).
Here is a two-clause solution: (A ∨ ¬B ∨ ¬x) ∧ (xC∨ ¬D) ∧ (xCE).

This can be shown to be equivalent to the original formula by constraining x to be A∨¬B and algebraically reducing:

(A∨¬B∨¬(A∨¬B))∧(A ∨ ¬BC ∨ ¬D)∧(A ∨ ¬BCE)
(A ∨ ¬BC ∨ ¬D)∧(A ∨ ¬BCE)
(A ∨ ¬BC) ∨ (¬DE)
A ∨ ¬BC ∨ (¬DE)

To further prove the equivalence, we can make the original formula unsatisfied and show that there is no satisfying assignment for x. To be unsatisfied, A must be F, B must be T, and C must be F. This reduces the formula to:

(FF ∨ ¬x)∧(x ∨ F ∨ ¬D)∧(x ∨ FE)
Because of the first term, x must be F if we want to satisfy the formula:
(FFT)∧(FF ∨ ¬D)∧(FFE) ≡ (¬DE)
This has the same satisfiability as the remaining variables in the original formula (if ¬DE is not satisfied, there is no satisfying assignment for x).

Proof that this is the shortest possible solution: There is no two or one clause solution because a new variable in addition to A, B, C, D, and E is required for each clause to have only three terms, and this variable must be repeated (by the rules we use to select that variable). Therefore, only 5 variables may be represented in a two-clause solution, while there are at least six variables required for equivalence to the original formula.

Proof that a new variable is required: The original formula reduces to (A ∨ ¬BC ∨ ¬D)∧(A ∨ ¬BCE) in CNF form, which has two clauses, each containing a unique combination of four variables. There is no way to reduce the number of variables per clause of a solution without adding a variable, therefore at least one variable must be added to form the 3-CNF equivalent of this formula.