HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

Computational Complexity of Not All Equal SAT variant

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
satvariantallequalcomputationalnotcomplexity

Problem

Not All Equal SAT is an NP Complete problem. Let us now consider another variant of the problem.

Given a Not All Equal SAT (NAESAT) problem (arbitrary number of literals allowed per clause) with an additional constraint that each pair of clauses share at least 1 literal (not variables but literals).

Is this problem still NP-hard? It seems so, but I am unsure about the reduction.

Solution

Your problem is NP-hard, as can be seen by a (known, I believe) reduction from CNF-SAT: Reduce from (for example) $3$-SAT as follows. Given a formula $F$, create a formula for your special NAE-SAT by introducing exactly one additional variable, say $y$. Add $y$ to every clause in $F$ to obtain $F'$.

Example: $F = (x_1 \vee x_2 \vee \neg x_3) \wedge (\neg x_2 \vee x_3 \vee \neg x_4)$ becomes $F' := (x_1 \vee x_2 \vee \neg x_3 \vee y) \wedge (\neg x_2 \vee x_3 \vee \neg x_4 \vee y)$

After doing this, every clause contains $y$ and thus shares (at least) one literal.

Proof sketch:
If $F$ is satisfiable, use the same satisfying assignment to satisfy $F'$, together with $y = false$.

If $F'$ is satisfiable, there are two options

  • $y = false $, in this case the same assignment satisfies $F$ ($F'$ has at least one true literal per clause, and it is never $y$, thus $F$ has at least one true literal per clause as well)



  • $y = true$, negate the satifying assignment for $F'$ to satisfy $F$ (at least one false literal per clause in $F'$, after negating the assignment we have at least one true literal per clause)

Context

StackExchange Computer Science Q#77242, answer score: 9

Revisions (0)

No revisions yet.