600 too large? dl-904

Concerning the dl test 904:

http://www.w3.org/TR/2003/CR-owl-test-20030818/dl-900-arith#description-logi
c-904


Jim wrote:
> I would, however, like to suggest we make this test with the numbers
> 200, 300, and 600 into an extra credit test -- now that my group has
> built Pellet, and run this problem with various values of i,j and k,
> I'm more sure then ever that we're just looking at a large
> combinatorics problem -- with enough space and time the system would
> prove it, and I think anything that doesn't need to enumerate
> examples will require some sort of heuristic -- we could pick a
> smaller number (20, 30, 60) to be the harder version of the problem
> if we think we need some values to push people a bit more...
>


My point of view in putting this test in was the following:

1) there are implementation strategies, such as those investigate by the
Racer team, that keep track of cardinalities as numbers and have a linear
programming module that check such constraints. I do not know the state of
that work, nor whether it is directly applicable to this test.

2) 600 was intended to be big enough to blow a brute force approach.

3) If the implementors cannot handle 600 then IMO it is a sufficiently small
number that some OWL users may be surprised.

4) Thus if the WG would choose to move this test to extra credit, I would
like to see appropriate health warnings, may be in reference or guide, to
the effect that, currently, the numbers in the cardinality constraints
should be kept small. The test document extra credit section could better
document our combined implementation experience.

Jeremy

Received on Wednesday, 10 September 2003 11:20:03 UTC