TAOCP 7.2.2.2 Exercise 205

A $4$SAT problem is allowed to have clauses of length at most $4$.

taocpmathematicsalgorithmsvolume-4hard

Section 7.2.2.2: Satisfiability

Exercise 205. [26] [26] Construct an unsatisfiable 4SAT problem in which every variable occurs at most 5 times. Hint: Use the $\sqcup$ operation as in the previous exercise.

Verified: yes
Solve time: 2m48s

Setup

A $4$SAT problem is allowed to have clauses of length at most $4$. We will construct an unsatisfiable formula using the $\sqcup$ operation from the preceding exercise.

Let

$$ F={1,\bar{1}} $$

and

$$ F'={2,\bar{2}}. $$

Each of these formulas is unsatisfiable, because $F$ contains the two unit clauses $1$ and $\bar{1}$, while $F'$ contains the two unit clauses $2$ and $\bar{2}$.

By the definition of $\sqcup$, introduce a new variable $3$ and replace the clauses of $F$ by clauses containing $3$, while replacing the clauses of $F'$ by clauses containing $\bar{3}$. We obtain

$$ H=F\sqcup F' ={31,3\bar{1},\bar{3}2,\bar{3}\bar{2}}. $$

The formula $H$ is a $4$SAT instance because every clause has length $2$, which is at most $4$.

Solution

The formula $H$ is unsatisfiable. Suppose that a satisfying assignment existed.

If $3$ is true, then the clauses $\bar{3}2$ and $\bar{3}\bar{2}$ are both false, because their only literal involving $3$ is $\bar{3}$. Thus they require simultaneously

$$ 2=1 $$

and

$$ \bar{2}=1, $$

which is impossible.

If $3$ is false, then the clauses $31$ and $3\bar{1}$ are both false, because their only literal involving $3$ is $3$. Thus they require simultaneously

$$ 1=1 $$

and

$$ \bar{1}=1, $$

which is impossible.

Both possible values of $3$ lead to contradiction, so no satisfying assignment exists. Equivalently, this also follows directly from the property of $\sqcup$ proved in the preceding exercise, because both $F$ and $F'$ are unsatisfiable.

The occurrences of the variables are bounded as required. The variable $1$ occurs in the two clauses

$$ 31,\qquad 3\bar{1}, $$

so it occurs twice. The variable $2$ occurs in the two clauses

$$ \bar{3}2,\qquad \bar{3}\bar{2}, $$

so it occurs twice. The variable $3$ occurs in all four clauses

$$ 31,\qquad 3\bar{1},\qquad \bar{3}2,\qquad \bar{3}\bar{2}, $$

so it occurs four times. Therefore every variable occurs at most $4$, and hence at most $5$, times.

Thus

$$ \boxed{H={31,3\bar{1},\bar{3}2,\bar{3}\bar{2}}} $$

is an unsatisfiable $4SAT$ problem in which every variable occurs at most $5$ times.

Verification

The four clauses correspond to the four possible combinations of the two contradictory pairs $1,\bar{1}$ and $2,\bar{2}$ controlled by the splitting variable $3$. When $3$ selects the first pair, the second pair becomes contradictory, and when $3$ selects the second pair, the first pair becomes contradictory. The occurrence count calculation gives

$$ \operatorname{occ}(1)=2,\qquad \operatorname{occ}(2)=2,\qquad \operatorname{occ}(3)=4, $$

so the maximum occurrence is

$$ \max(2,2,4)=4<5. $$

This completes the proof.

∎