RE: Proposed response to Martin Merry, HP

On May 12, Jeremy Carroll writes:
> 
> >
> > For some reason, the encoding of SAT problems in Test [1] uses
> > nominals, rather than the standard class based encoding (e.g., as used
> > in the TANCS test suite), which pushes the problem into that part of
> > the language which is hard for complete reasoners to deal with. Using
> > the class based encoding, FaCT is able to solve the test cases in less
> > than 0.05s on a 1GHz PIII desktop.
> 
> 
> 
> I am surprised that the failure directed backtracking techniques are not
> successful on the examples I produced.

I didn't say that. They may be successful in an implemented system, but I
don't have access to such a system.

> 
> They are intended to be easy for an appropriately optimized system (not that
> I have an optimization to suggest - I merely ran the pre-encoded form
> through a specialized reasoner, and like you got a very small time).

The trouble with encoding the problem in terms of nominals is that the
resulting KB is saying something much "stronger" than the original
problem. In particular, there are lots of implicit cardinality
constraints on the size of classes. The encoding of the problem
actually relies on relatively subtle interactions between such
constraints. E.g., the only reason we know that plus1 and minus1
cannot be interpreted as the same object is that the class TorF is
defined to be equivalent to the class {T F}, where T and F are
different, so the cardinality of TorF must be 2, so plus1 and minus1
must be interpreted as 2 different objects (phew!).

Dealing with such interactions is non-trivial for a complete reasoner
(and, speaking for myself, also for a human reasoner), and may rule
out the use of many very useful reasoning techniques and
optimisations.

Having said that, the example does not use inverse roles and so would
be solvable using known algorithms. For this size of problem I would
expect the performance of such algorithms to be good.

> 
> I would suggest that this report merely enhances Martin's comment. If
> implementors can't implement oneOf as adequately as the rest of the language
> is this going to result in confusion as to how solid OWL DL actually is?

I think this is covered by Jim's proposed response. Users should be
aware that nominals are a very powerful construct, and the
(gratuitous) use of nominals is likely to adversely affect
performance.

Ian


> 
> 
> Jeremy

Received on Monday, 12 May 2003 09:57:35 UTC