Re: sat to horn sat

James Dolan wrote:

in article <hleng.160$rk3.112@xxxxxxxxxxxxx>, apoph <xxxx@xxxxxxx>
wrote:

|Proginoskes wrote:
|
|>apoph wrote:
|> |>
|>>Is there an algorithm that turns sat instances into horn sat?
|>> |>>
|>
|>If there is a polynomial algorithm that does, then P=NP; Horn SAT is
|>known to be in P. (See
|>http://www.cs.berkeley.edu/~kunal/CS270/notes/lec1draft.ps for
|>instance.)
|>
|> --- Christopher Heckman
|>
|> |>
|Yes you're right. That is also necessary condition for np=p since
|horn sat is p-complete.
|
|But complexity is not an issue here. Any algorithm will do.

you should probably make your question a bit more precise: is there an
algorithm that turns a sat instance x into a horn-sat instance with
the same ??? as x? there might be only one relatively obvious way of
choosing "???" so as to make it an interesting question, but
nevertheless you should be the one to do the work of actually making
it precise.



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.
2) 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.

-a
.

Relevant Pages

  • Re: sat to horn sat
    ... But maybe you want an algorithm that converts a sat instance you ... I'd just like to see an example of reduction from sat to horn sat. ... Tricky part is to define R so that it applies to all to sat instances preserving satisfiability. ... And surely there exists one that satisfies the requirement "X is satisfiable iff Ris satisfiable". ...
    (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
    ... |>apoph wrote: ... |>>Is there an algorithm that turns sat instances into horn sat? ...
    (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)