cs2102
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 ∨ ¬B ∨ C ∨ (¬D ∧ E).
Here is a two-clause solution: (A ∨ ¬B ∨ ¬x) ∧ (x ∨ C∨ ¬D) ∧ (x ∨ C ∨ E).

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 ∨ ¬B ∨ C ∨ ¬D)∧(A ∨ ¬B ∨ C ∨ E)
(A ∨ ¬B ∨ C ∨ ¬D)∧(A ∨ ¬B ∨ C ∨ E)
(A ∨ ¬B ∨ C) ∨ (¬D∧E)
A ∨ ¬B ∨ C ∨ (¬D∧E)

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:

(F ∨ F ∨ ¬x)∧(x ∨ F ∨ ¬D)∧(x ∨ F ∨ E)
Because of the first term, x must be F if we want to satisfy the formula:
(F ∨ F ∨ T)∧(F ∨ F ∨ ¬D)∧(F ∨ F ∨ E) ≡ (¬D∧E)
This has the same satisfiability as the remaining variables in the original formula (if ¬D∧E 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 ∨ ¬B ∨ C ∨ ¬D)∧(A ∨ ¬B ∨ C ∨ E) 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.