6
$\begingroup$

I am trying to figure out how to reduce a 3SAT problem to a 3SAT NAE (Not All Equal) problem.

Not only that, I also figure out that I am not so sure about the reduction to 3SAT either.

Anyway, how do I go for that?

Since the size of each clause is already the same, I don't have to work on that. But I can't seem to find a way to create an instance I2 of 3SAT-NAE which is accepted iff the 3SAT accepts it.

EXTRA QUESTION: Does SAT (or 3SAT) allow any operation in the clauses? Because I always saw V (or) and never other operations. That confuses me a lot, because if it only allows V, then I don't get the reduction I found; but if it accepts even AND, then I get it.

$\endgroup$
2
  • $\begingroup$ with NOT all Equal you mean: all clauses true but for a single one? And No: SAT and 3-SAT are in en.wikipedia.org/wiki/Conjunctive_normal_form that's why you'll always find $\lor$ inside the clause and $\land$ between them $\endgroup$
    – b00n heT
    Jan 22, 2014 at 17:06
  • 1
    $\begingroup$ There must be at least 1 True and 1 False. {T,T,F} {F,F,T} {T,F,T} {F,T,F}.... The one you said is similar to OIT (On In Three) and wants exactly 1 True and 2 False. $\endgroup$
    – N3sh
    Jan 22, 2014 at 17:07

2 Answers 2

6
$\begingroup$

For the pedantic's sake, we first have a polynomial reduction $3SAT \leq_p s3SAT$, where the later has strictly 3 terms per clause, not less (as accepted by the former). This is achieved by taking an instance of $3SAT$ and mapping the clauses respectively:

$ (a) \mapsto (\lnot s \lor \lnot s \lor \lnot s) \land (s \lor s \lor a) $

$ (a \lor b) \mapsto (\lnot s \lor \lnot s \lor \lnot s) \land (s \lor b \lor a) $

where $s$ is a dummy variable, and a and b are terms where $\lnot \lnot$ is negated respectively. We concatenate the end result with $\land$. Clearly we construct in polynomial time.

Next we do the polynomial reduction $s3SAT \leq_p NAE-4SAT$, where the second is simply $NAE-3SAT$ but with four terms per clause. For this we take an instance of $s3SAT$ and map each clause as follows:

$ (x \lor y \lor z) \mapsto (x \lor y \lor z \lor s) \land (\lnot x \lor \lnot y \lor \lnot z \lor \lnot s)$

Where $x,y,z$ are terms and $s$ is our dummy variable, as before. Notice the symmetry here, if we find an assignment with $s = true$ we can simply invert the assignment to receive another valid assignment with $s=false$. This is the assignment we want.

As a last step we reduce $NAE-4SAT \leq_p NAE-3SAT$. Take an instance in $NAE-4SAT$ and map the clauses as follows:

$ (a \lor b \lor c \lor d) \mapsto (s \lor a \lor b) \land (\lnot s \lor c \lor d)$

All the same as before, concatenate the result once more. Notice here that if the true and false variable's (one of each must exist) are mapped to the same clause, $s$ can be choose appropriately. If they are mapped to different clauses, $s$ can be choose opposite to the respective variable value in each pair.

To summarize: $3SAT \leq_p s3-SAT \leq_p NAE_4SAT \leq_p NAE-3SAT$.

Answer to extra question: 3SAT only allows $\lor$ in the clauses.

$\endgroup$
1
$\begingroup$

A more straightforward solution is the following:

for each clause add a new variable ci and perform the following transformation.

$(x1 ∨ x2 ∨ x3) \rightarrow (x1 ∨ x2 ∨ ci) ∧ (x3 ∨ \lnot ci ∨ F)$

Where F is the constant value false.

If $(x1 ∨ x2 ∨ x3)$ has a solution where all literals evaluate to true then set ci to false and $(x1∨ x2 ∨ ci) ∧ (x3 ∨ \lnot ci ∨ F)$ is also satisfied with the added condition of "Not-All-Equal".

If $(x1 ∨ x2 ∨ x3)$ has no solution (all literals evaluate to false) then there is no assignment of ci that can make $(x1∨ x2 ∨ ci) ∧ (x3 ∨ \lnot ci ∨ F)$ true.

If $(x1 ∨ x2 ∨ x3)$ has a solution where not all literals evaluate to true then we can always set ci so that $(x1∨ x2 ∨ ci) ∧ (x3 ∨ \lnot ci ∨ F)$ is satisfied.

some examples for the last case:

  • if $x1=x2=t \land x3=f$ set ci=f.
  • if $x1=x3=t \land x2=f$ set ci=t.

...

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .