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?