Converting into CNF Form

Question

If you have disjunctive clause comprising of $n$ literals for example $(X_1\cup X_2\cup X_3\cup\cdots \cup X_n)$. where $n\geq 4$. How you can convert it into CNF (Conjunctive Normal Form) of $n-2$ disjunctive clauses each having exactly $3$ literals.

For example $(Y_1\cup Y_2\cup Y_3) \cap (Y_4\cup Y_5\cup Y_6)\cap \cdots \cap (Y_{m-2}\cup Y_{m-1}\cup Y_m)$ and having the same truth assignment.

Answer 1

To break a clause into several smaller clauses, additional switching variables can be introduced. Basically, a disjunction (OR) of many inputs is replaced by a disjunction of disjunctions with fewer inputs.

Proposed method:

1. First clause is $(X_1 \cup X_2 \cup t_1)$

2. Second clause $(\neg t_1 \cup X_3 \cup t_2)$

3. Third clause $(\neg t_2 \cup X_4 \cup t_3)$

4. Clause $k$ for $k = 2 \, \dots \, (n - 3)$ is $(\neg t_{k-1} \cup X_{k+1} \cup t_k)$

5. Last clause $(\neg t_{n-3} \cup X_{n-1} \cup X_{n})$

---

Example for $n=4$ literals:

$$(X_1\cup X_2\cup X_3\cup X_4) = (X_1 \cup X_2 \cup t_1) \cap (\neg t_1 \cup X_3 \cup X_4) $$

---

Example for 5 literals:

$$(X_1\cup X_2\cup X_3\cup X_4 \cup X_5) = (X_1 \cup X_2 \cup t_1) \cap (\neg t_1 \cup X_3 \cup t_2) \cap (\neg t_2 \cup X_4 \cup X_5) $$

---

The first and the last clause cover two literals each. The other $n-4$ clauses include two switching variables and one original literal. Therefore, the total number of clauses is $2 + (n-4) = n - 2$ with clause-length 3.

Introduction of switching variables was suggested by Tseitin.

---

Update:

I am not really sure about this solution. Could someone have an eye on it?