4NAE ≤p 3NAE | Complexity Atlas

The construction

On a 4CNF formula $\varphi$ , give every clause $C=\ell_1\vee\ell_2\vee\ell_3\vee\ell_4$ its own fresh auxiliary variable $z_C$ and replace it with the pair $(\ell_1\vee\ell_2\vee z_C)\;\wedge\;(\bar z_C\vee\ell_3\vee\ell_4).$

Return the resulting formula. This is exactly the splitting step of $\mathrm{SAT}\le_p\mathrm{3SAT}$ — the identical construction — but here it must be re-proved under NAE semantics, which is a stronger requirement than ordinary satisfiability.

Visualization

Correctness — both directions

4NAE ∈ ⟹ 3NAE ∈

Suppose $v$ NAE-satisfies $\varphi$ . Let $C=\ell_1\vee\ell_2\vee\ell_3\vee\ell_4$ ; under $v$ it holds both a true and a false literal. Set $z_C$ as follows:

if $v(\ell_1)\ne v(\ell_2)$ — the first pair already has both values, so use $z_C$ to fix the second: if $v(\ell_3)=v(\ell_4)$ set $v(z_C)=v(\ell_3)$ , whereupon $\bar z_C$ supplies the opposite value in $(\bar z_C\vee\ell_3\vee\ell_4)$ ; otherwise any choice works.
if $v(\ell_1)=v(\ell_2)=:b$ — since $C$ has both a true and a false literal, some $t\in\{3,4\}$ has $v(\ell_t)=\lnot b$ . Set $v(z_C)=\lnot b$ . Then in the first clause $\ell_1,\ell_2$ give $b$ and $z_C$ gives $\lnot b$ — both values; and in the second $\bar z_C$ gives $b$ while $\ell_t$ gives $\lnot b$ — both values again.

In every case both clauses are NAE-satisfied, and $z_C$ occurs nowhere else. So the output is NAE-satisfiable.

3NAE ∈ ⟹ 4NAE ∈

Suppose $v$ NAE-satisfies the output; restrict it to the variables of $\varphi$ . Let $C=\ell_1\vee\ell_2\vee\ell_3\vee\ell_4$ ; we show it holds both values.

Write $c=v(z_C)$ . The clause $(\ell_1\vee\ell_2\vee z_C)$ is NAE-satisfied, so it holds a literal valued $\lnot c$ — and that literal must be $\ell_1$ or $\ell_2$ , since the third is $z_C$ , valued $c$ . So some $s\in\{1,2\}$ has $v(\ell_s)=\lnot c$ .

Likewise $(\bar z_C\vee\ell_3\vee\ell_4)$ is NAE-satisfied and $\bar z_C$ is valued $\lnot c$ ; so it holds a literal valued $c$ , necessarily $\ell_3$ or $\ell_4$ . So some $t\in\{3,4\}$ has $v(\ell_t)=c$ .

Thus $C$ holds literals valued $\lnot c$ and $c$ — both a true and a false one. So $C$ is NAE-satisfied, and as $C$ was arbitrary, $\varphi\in\mathrm{4NAE}$ .

Cost of the reduction

TimeO(|φ|)

SpaceO(|φ|)

Output sizeO(|φ|)

Each clause is handled once: $m$ clauses become $2m$ , with $m$ new variables. Unlike $\mathrm{SAT}\le_p\mathrm{3SAT}$ there is no loop here — the clause length is a fixed $4$ , so a single split suffices.

What it buys

$\mathrm{3NAE}$ is NP-hard, which licenses it as the starting point for $\mathrm{3NAE}\le_p\mathrm{MAXCUT}$ and $\mathrm{3NAE}\le_p\mathrm{3COL}$ .

Pitfalls

"Same construction as $\mathrm{SAT}\le_p\mathrm{3SAT}$ , therefore correct" is not an argument. NAE semantics differ, and the proof above uses $\bar z_C$ in a completely different way — there it satisfied a clause, here it forces the opposite value.

The chain

Rests on

3SAT ≤p 4NAE

Used later by

Where this was read from

Lesson 10משפט 3: $\mathrm{3NAE}$ ו- $\mathrm{4NAE}$ הן NP-קשות
2024 '1 מועד 2"One of the course exercises described a reduction from 4-NAE to 3-NAE" — counting the output.
2024The $k\mathrm{NAE}$ family and the reductions inside it.

As with $\mathrm{3SAT}\le_p\mathrm{4NAE}$ : the lesson assigns it as homework without writing the construction. The 2024 paper confirms it was given as a course exercise, so it is marked corpus-backed; the full write-up here is a completion.