# Another way to solve SAT. Was it known?

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?

• Isn't this pretty much equivalent to DPLL? In your example set $y$ to false and notice that all the other clauses can be satisfied by setting the remaining variables to true. Sep 7, 2017 at 10:07
• @adrianN, particularly in this case it is true. But why would DPLL start from $\overline y$? Sep 7, 2017 at 10:40
• Your theorem doesn't seem to be saying anything. Sure, you can make all the variables positive. Great. Now what? You can do that for any instance. Are you claiming some kind of link between the original instance and the new one? Sep 7, 2017 at 12:08
• @rus9384 I can make anything positive that I want to make positive! A meaningful theorem would say "A formula can be changed _so that certain properties hold"." Your theorem says "A formula can be changed", which isn't saying anything. I'll change all formulas to "$X$" -- that establishes that all formulas can be changed. Sep 7, 2017 at 12:35
• Here's a more concrete example. "There is a polynomial time procedure that rewrites any CNF formula $\phi$ to give a new CNF formula $\phi'$ in which every variable appears at most three times, such that $\phi'$ is satisfiable if, and only if, $\phi'$ is satisfiable." Yours just says the equivalent of "There is a procedure that rewrites any CNF formula $\phi$ to give a new CNF formula $\phi'$ in which every variable appears at most three times." That's trivial -- rewrite every formula as "$X$". Sep 7, 2017 at 12:37