Theorem. If and only if SAT instance $\varphi$ is satisfiable, there is a way to negate variables in $\varphi$ and get $\varphi'$ where all clauses have at least one positive literal.
Also we can change word 'negative' by 'positive'.
For example, let we have an instance $(x\lor y\lor\overline z)\land(\overline y\lor\overline t)\land(x\lor z\lor t)\land(\overline y\lor z\lor\overline t)\land(x\lor\overline t)$
We have monotone clauses $(\overline y\lor\overline t)$ and $(x\lor z\lor t)$.
$(\overline y\lor\overline t)$ is shorter, let's modify it.
Negating $y$ gives us a formula that has no negative clauses. So, $x\overline yzt$ is positive assignment.
Let us take unsatisfiable formula $(x\lor y)\land(x\lor\overline y)\land(\overline x\lor \overline z)\land(z\lor t)\land(z\lor\overline t)$.
There is one negative clause $(\overline x\lor \overline z)$.
Flipping $x$ or $z$ will not reduce the amount of negative clauses. In fact both renamings $xy$ and $zt$ do not allow to get rid of negative or positive clauses.
In fact, this can be seen as generalization for renamable Horn SAT.
We can try to implement an algorithm that will try to reduce the amount of these clauses. Is such way to solve SAT is known?