0
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – adrianN Sep 7 '17 at 10:07
  • $\begingroup$ @adrianN, particularly in this case it is true. But why would DPLL start from $\overline y$? $\endgroup$ – rus9384 Sep 7 '17 at 10:40
  • $\begingroup$ 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? $\endgroup$ – David Richerby Sep 7 '17 at 12:08
  • 1
    $\begingroup$ @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. $\endgroup$ – David Richerby Sep 7 '17 at 12:35
  • 1
    $\begingroup$ 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$". $\endgroup$ – David Richerby Sep 7 '17 at 12:37
4
$\begingroup$

You haven't really specified an algorithm, but a similar idea is used by random walk algorithms for SAT such as Schöning's algorithm (see for example Giurgiu's Master thesis or one of the many online lecture notes on the topic).

The same approach is also used in the heuristic algorithm WalkSAT which has recently been used to prove an algorithmic version of the Lovász local lemma.

$\endgroup$
  • $\begingroup$ I am trying to understand renamable Horn algorithm, maybe it'll help. $\endgroup$ – rus9384 Sep 7 '17 at 12:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.