So If I understood correctly, the conversion from 4-SAT statement to 3-SAT statement follows the following approach:

(a or b or c or d) -> (a or b or z) and (-z or c or d)

Where the z is a new literal. However, with 4 literals there exists 4^2 different permutations (a or b or c or d) and (-a or b or c or d) and (a or -b or...) and ...

If I convert each of the clauses with the approach above (add always new literal z_n and it's negation) like:

(a or b or z) and (c or d or -z) and (-a or b or z_2) and (c or d or -z_2) and ...

, then the resulting 3-SAT statement is indeed satisfiable. Even if the 4-SAT statement with the all permutations for 4 literals is not. They should be equisatisfiable?


You're right in saying that they should be equisatisfiable. And they are.

I'm not sure why you think converting your unsatisfiable $4-\text{SAT}$ instance into a $3-\text{SAT}$ instance would make it satisfiable. Because it doesn't.

If a $4-\text{SAT}$ instance is unsatisfiable, then no matter how you choose to assign truth values to your variables, there will be some clause that is not satisfied. Without loss of generality, let that clause be $(a \vee b\vee c\vee d)$. Since this clause is not satisfied by your assignment, it follows that all of $a, b, c$ and $d$ are false.

Now converting this into a $3-\text{SAT}$ instance gives you these pair of clauses: $(a \vee b \vee z)(\neg z \vee c\vee d)$. Note that since $a, b, c$ and $d$ are all false, in order for both of these clauses to be satisfied, both $z$ and $\neg z$ need to be true, which is impossible.

In other words, the resulting $3-\text{SAT}$ instance is also unsatisfiable.

  • $\begingroup$ This is the wrong proof. You are trying to convert an unsatisfying assignment to the 4-CNF into an unsatisfying assignment of the 3-CNF. What you need to show is that a satisfying assignment of the 3CNF can be converted to a satisfying assignment of the 4-CNF, just as in the other answer. $\endgroup$ Feb 24 '18 at 4:42
  • $\begingroup$ @SashoNikolov, I didn't prove equisatisfiability. What I did was address the specific query that the OP had. The OP took a specific unsatisfiable $4-\text{SAT}$ instance with $16$ clauses, replaced each clause $a\vee b\vee c\vee d$ with the pair of clauses $(a\vee b\vee z)(\neg z\vee c \vee d)$ and claimed that the resulting $3-\text{SAT}$ instance is satisfiable. What I did is show that it's not true: if the original $4-\text{SAT}$ instance was unsatisfiable to begin with, changing each clause in the manner mentioned in the question does not make it satisfiable. $\endgroup$
    – mursalin
    Feb 24 '18 at 5:08
  • $\begingroup$ It's still the same issue: your argument does not prove the resulting 3-CNF is not satisfiable. You cannot say "since $a, b, c$ and $d$ are all false" because that does not need to be the case in every possible assignment of truth values for the 3-CNF. The only way I see how to prove the 3-CNF is unsatisfiable is to show that any satisfying assignment to the 3-CNF can be turned into a satisfying assignment to the 4-CNF. $\endgroup$ Feb 24 '18 at 5:17
  • $\begingroup$ @SashoNikolov, if a 4-SAT instance is unsatisfiable, then for any assignment of the variables, there is (at least) one clause with all of the literals set to false. I call that clause $a\vee b\vee c\vee d$ by possibly renaming some of the literals. $a,b,c,d$ are all false because I picked the clause with all false literals and called it $a\vee b\vee c\vee d$. I hope this makes sense. $\endgroup$
    – mursalin
    Feb 24 '18 at 5:25

So if I get it correctly, you started with the $2^4$ many clauses

  • $a \vee b \vee c \vee d$
  • $\neg a \vee b \vee c \vee d$
  • $a \vee \neg b \vee c \vee d$
  • $\ldots$
  • $\neg a \vee \neg b \vee \neg c \vee \neg d$

There does not exist a valuation to the variables in $\{a,b,c,d\}$ that satisfies all of them, so these 16 clauses are together unsatisfiable.

Now we translate these clauses into 3CNF. This yields 32 clauses:

  • $a \vee b \vee z_0$, $\neg z_0 \vee c \vee d$
  • $\neg a \vee b \vee z_1$, $\neg z_1 \vee c \vee d$
  • $a \vee \neg b \vee z_2$, $\neg z_2 \vee c \vee d$
  • $\ldots$
  • $\neg a \vee \neg b \vee z_{15}$, $\neg z_{15} \vee \neg c \vee \neg d$

This set of clauses should be equisatisfiable to the set of clauses given above as the translation to 3CNF yields an equisatisfiable formula.

And it actually is equisatisfiable. To see this, assume that we have a model $m$ for the 3CNF formulation. This assigns values to all variables in $\{a,b,c,d,z_0,z_1, \ldots, z_{15}\}$. We know that $m$ (restricted to $\{a,b,c,d\}$ is also a model for the original CNF), as for every $i \in \{0, \ldots, 15\}$, we know that the if $z_i$ has a false $\mathbf{false}$, then one of the first two literals of the original $i$th clause have to hold, and if $z_i$ has a $\mathbf{true}$ value, then one of the latter two literals of the original $i$th clause have to hold.

Since the original 4CNF instance is unsatisfiable, and we know that from every model for the 3CNF SAT instance we can obtain a model for the 4CNF instance, we now know that the assumption that there exists a satisfying model for the 3CNF SAT instance exists must be wrong.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.