# Is Monotone 3-SAT with exactly 3 distinct variables untractable? 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? Posted on Categories proxies