SAT variant with almost disjoint clauses

Question

I'm wondering whether the following SAT variant is NP-complete or polynomial. The formula given in input has n*m variables, and it has two parts.

A part with the n positive clauses: $$(x_{1,1} \lor \dots \lor x_{1,m}) \land \\\dots\\(x_{n,1} \lor \dots \lor x_{n,m})$$

And a part with negative clauses with two variables: $$ \neg x_{i,j} \lor \neg x_{k,l} $$ where $x_{i,j}$ and $x_{k,l}$ are part of the n*m variables mentioned above.

Thank you for the help

Answer 1

I don't know the Multicolored Clique Problem suggested by Daniello, however there is a simple reduction from 3SAT:

Given a 3SAT formula $\varphi$ over $n$ variables $x_1,...,x_n$; for each $x_i$ add two variables:

• $y_{i}^T$ that represents $x_i = true$, and
• $y_{i}^F$ that represents $x_i = false$

and add the clause $(\neg y_{i}^T \lor \neg y_{i}^F)$ that represents the condition that $x_i$ cannot be both true and false.

Finally replace every clause $C_j = (l_{j1} \lor l_{j2} \lor l_{j3})$ of $\varphi$ with a clause made of three positive literals $(y_{j1}^a \lor y_{j2}^b \lor y_{j3}^c)$ where:

• $a = T$ if $l_{j1}= x_{j1}$, $b=F$ if $l_{j1} = \neg x_{j1}$
• $b = T$ if $l_{j2}= x_{j2}$, $b=F$ if $l_{j2} = \neg x_{j2}$
• $c = T$ if $l_{j3}= x_{j3}$, $b=F$ if $l_{j3} = \neg x_{j3}$

For example $(x_1 \lor \neg x_2 \lor \neg x_3)$ becomes: $(y_1^T \lor y_2^F \lor y_3^F)$

Update:

In order to make every positive literal $y_i$ (that can be $y_i^T$ or $y_i^F$) occur only once in the upper part, you can use the following technique:

Suppose that $y_i$ occurs twice, then you can simply replace the two occurrences with two new positive variables: $y_i'$ and $y_i''$ and add the conditions for: $y_i' \leftrightarrow y_i''$:

$$(\neg y_i' \lor y_i'') \land (\neg y_i'' \lor y_i')$$

At this point repeat the split procedure ($y_i'$ becomes $y_i^{T'}$ and $\neg y_i'$ becomes $y_i^{F'}$):

$$(\neg y_i^{T'} \lor \neg y_i^{F''}) \land (\neg y_i^{T''} \lor \neg y_i^{F'}) \land (y_i^{T'} \lor y_i^{F'}) \land (y_i^{T''} \lor y_i^{F''}) $$

and add a dum clause to the upper part in order to include the $y_i^{F'}$ and $y_i^{F''}$, for example: $(y_i^{F'} \lor y_i^{F''} \lor z_i)$, where $z_i$ is a new variable that can make the clause true.

If $y_i$ occurs more than twice the procedure is similar.