Is Monotone 3-SAT with exactly 3 distinct variables untractable?

Question

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?

Answer 1

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.