Re: sat to horn sat

Mitch wrote:

apoph wrote:


Okay, is there an algorithm R that turns any sat instance X into a horn
sat instance R(X) so that:

1) X is satisfiable iff R(X) is satisfiable.



No, because there are some formulas that are not horn:

e.g. 'p or q'

(the only other one on two vars is 'p!=q' or equivalently '(p ^ -q) v
(-p ^ q)')

But maybe you want an algorithm that converts a sat instance you
-assume- to be horn-able. And since you don't care about complexity, of
course there's the naive algorithm of 'generate-and-test': try all horn
formulas (up to a sufficient size) and test equivalence with X.

But that's terribly inefficient. But maybe you want an efficient
algorithm?

Mitch



As to your last question: I'd just like to see an example of reduction from sat to horn sat (no requirements on effiency). See for example http://en.wikipedia.org/wiki/Reduction_%28complexity%29.

It is true that not all formulas are horn but that doesn't say that there couldn't be an algorithm R that outputs a horn formula (or set of horn formulas) when input is a set of formulas. For example the trivial one: R that produces some constant set of horn clauses for all X: R(X)=print("{'p or -p', '-y', 'u'}"). Tricky part is to define R so that it applies to all to sat instances (set of sat formulas) preserving satisfiability.

And surely there exists one that satisfies the requirement "X is satisfiable iff R(X) is satisfiable". For example R2: if(X is satisfiable){ print "{p}" } else { print "{p},{-p}" } but it is not interesting since it requires that X must be decided first (by trial and error for example). I'm not saying that finding an algorithm to solve sat is not interesting problem but it is a problem of its own.

If I understood correctly what you mean by equivalence of set of formulas (both either satisfiable or not satisfiable?) then 'generate-and-test' requires that one must first decide X and then try to find set of horn formulas that are either satisfiable or not. So pretty much algorithm R2.

Unless, of course, if there is a way to tell if two set of formulas (sat and horn sat) are equivalent without deciding sat first then that might just be what I'm looking for.

-a
.

Relevant Pages

  • Re: sat to horn sat
    ... |>apoph wrote: ... |>>Is there an algorithm that turns sat instances into horn sat? ... R is not trivial in a sense that it first decides X and then outputs some fixed satisfiable or unsatisfiable horn sat instance accordingly to the satisfiability of X. ...
    (sci.math)
  • Re: sat to horn sat
    ... apoph wrote: ... X is satisfiable iff Ris satisfiable. ... because there are some formulas that are not horn: ... But maybe you want an algorithm that converts a sat instance you ...
    (sci.math)
  • Re: sat to horn sat
    ... because there are some formulas that are not horn: ... But maybe you want an algorithm that converts a sat instance you ... identical satisfying instances. ... input and return a Horn formula Rthat is satisfiable iff X ...
    (sci.math)
  • Re: why not just publish truth table?
    ... The problem "satisfiability" is NP complete. ... then every algorithm takes too long. ... too much time to be practical [which is certainly untrue, ... with the context of the previous sentence. ...
    (sci.math)
  • Satisfiability problem compiler
    ... If tomorrow somebody invented an algorithm to solve any satisfiability ... compiler which would (in polynomial time, or in some efficient way) convert ... Does anyone know of research into such a compiler? ...
    (comp.theory)