1
$\begingroup$

I have given the following SAT variation:

Given a formula F in CNF where each clause C has exactly 3 distinct literals and for each C in F either all literals are positive or all literals are negated. Example:

$F= (x_1\vee x_2 \vee x_4) \wedge (\neg x_2\vee \neg x_3 \vee \neg x_4) \wedge (x_3\vee x_4 \vee x_5)$

Is this variation of SAT tractable?

My findings so far:

I suspect the problem is NP-complete and therefore not tractable. Thus I would like to perform a poly-reduction from 3-SAT to the variation described above.

An arbitrary 3-SAT formula can be converted to monotone 3-SAT.

Take following example:

$C_1=(x_1\vee x_2 \vee \neg x_3)$ and define $z_3$ by $\neg x_3 \leftrightarrow z_3$ and $x_3 \leftrightarrow \neg z_3$ which is equivalent to $(x_3\vee z_3)\wedge(\neg x_3 \vee \neg z_3)$.

From that we get the monotone form of $C_1$ by

$(x_1\vee x_2 \vee \neg x_3) \leftrightarrow (x_1\vee x_2 \vee z_3)\wedge (x_3\vee z_3)\wedge(\neg x_3 \vee \neg z_3)$

By applying this transformation to all clauses I get a monotone 3-SAT formula which is equally satisfiable.

My reduction produces additional 2 clauses with 2 literals for each non-monotone clause, but how do I get only monotone clauses with exactly 3 distinct literals?

$\endgroup$
  • $\begingroup$ Use Schaefer's theorem (though I'm not sure it has the condition of 3 distinct variables). $\endgroup$ – Yuval Filmus Jul 10 '20 at 12:03
  • 2
    $\begingroup$ Does this answer your question? What is the complexity of determining whether or not conjunction of positive CNF and negative CNF is satisfiable? $\endgroup$ – Kyle Jones Jul 10 '20 at 19:34
  • $\begingroup$ Its not the complete answer since your transformation only changes the clauses to monotone clauses. It produces 2 additional clauses with 2 literals to do this. But what I would also like to have is that every clause has exactly 3 distinct literals after the transformation. $\endgroup$ – Pepe Jul 11 '20 at 8:40
2
$\begingroup$

I will try to answer now my own question and would be glad about some feed back concerning the corectness.

Like in the question above discussed and pointed out by Kyle Jones we can reduce arbitrary 3-SAT formulas to monotone 3-SAT formulas.

For example a clause $C=(x_1\vee x_2 \vee \neg x_3)$ can be converted to $C'(x_1\vee x_2 \vee z_3)\wedge (z_3 \vee x_3) \wedge (\neg z_3 \vee \neg x_3)$. One can check if $C$ is satisfiable $C'$ is also satisfiable and if $C$ is not satisfiable $C'$ is also not satisfiable.

The next step is to convert all the clauses with less than 3 literals to clauses with exactly 3 distinct literals.

Therefore take for example $C_1=(x_1 \vee x_2)$ and transform it to $C_1'=(x_1 \vee x_2 \vee y_1)\wedge (x_1 \vee x_2 \vee y_2) \wedge (x_1 \vee x_2 \vee y_3) \wedge (\neg y_1 \vee \neg y_2 \vee \neg y_3)$ then again if $C_1$ is satisfiable $C_1'$ is also satisfiable and if $C_1$ is not satisfiable $C_1'$ is also not satisfiable. The same can be done for the negative case i.e. $C_2=(\neg x_1 \vee \neg x_2)$ can be transformed to $C_2'=(\neg x_1 \vee \neg x_2 \vee \neg u_1)\wedge (\neg x_1 \vee \neg x_2 \vee \neg u_2) \wedge (\neg x_1 \vee \neg x_2 \vee \neg u_3) \wedge ( u_1 \vee u_2 \vee u_3)$

By applying the two transformations one can convert an arbitrary 3-SAT instance to a monotone 3-SAT instance with exactly 3 distinct literals. As can be seen easily above the transformations have polynomial complexity. Therefore since 3-SAT is NP-hard the reduction aswell must be NP-hard.

$\endgroup$
  • 1
    $\begingroup$ Well done, this reduction works. To be complete, you should indicate what should happen to the clause $(\neg z_3\vee \neg x_3)$, because it should be treated slightly differently from the clause $(z_3\vee x_3)$. $\endgroup$ – Lieuwe Vinkhuijzen Jul 11 '20 at 11:49
  • $\begingroup$ Thank you, I added this case to the answer. $\endgroup$ – Pepe Jul 12 '20 at 16:37

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.