ok@cs.mu.oz.au (Richard O'Keefe) (09/21/89)
I've found a nice embedding of 3SAT as a Prolog program with three
predicates: two of them are a fixed number of ground unit clauses
(one has arity 3, the other arity 6) and the other has one clause
where no variable appears more than twice. The Herbrand universe
of this Horn clause program is {0, 1}.
The utility of this is that it shows that all the bottom-up type
inference methods that I think I understand (which isn't many) must
take exponential time. Worse still, it shows that because the
Mycroft/O'Keefe type checker allowed functor overloading (even
though it didn't allow predicate overloading) it is possible to
construct a simple predicate with one clause which takes exponential
time just to CHECK. (I believe the cost is reasonable if there is
no overloading.)
I'm in the process of writing this up as a short paper, but I would
be interested to know of any other *simple* mappings of standard
NP-complete or harder problems into Horn clauses.