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?

Improve this question
$\endgroup$
9
  • $\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, 2017 at 10:07
  • $\begingroup$ @adrianN, particularly in this case it is true. But why would DPLL start from $\overline y$? $\endgroup$
    – rus9384
    Sep 7, 2017 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, 2017 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, 2017 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, 2017 at 12:37

1 Answer 1

Reset to default
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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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