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.