Solving Einstein's riddle (zebra puzzle)

[blokhin]

Dear all,

there are two known implementations of the famous Einstein's riddle (zebra puzzle) in OWL:

• http://persons.iis.nsk.su/en/person/ponom/ontologies (by Denis Ponomaryov, ALCOIF expressivity),
  attached
• http://folk.uio.no/martige/what/20120422/zebra.html (by Martin Skjæveland, ALCROIQ expressivity), attached

Unlike Protégé, this brute-force reasoner fails to solve both of these implementations (an expanded graph does not contain any triples connecting zebra and Japanese, which is an answer).

Is it an expected behavior?

[nicholascar]

I will look into this after the Python3 version is properly released

[blokhin]

@nicholascar my understanding is that the expressivity of these two ontologies is just too high. Please, correct me if I'm wrong.

[blokhin]

@iherman what do you think?

[ashleysommer]

@blokhin I've been looking into how these zebra-puzzle ontologies work within this implementation of OWL-RL, why they don't produce a solution, and what it would take for this implementation to be able to solve this puzzle using those ontologies.

I think it comes down to the restrictions of the specific flavour of OWL (RL) that is used.

See this page: https://www.w3.org/TR/owl2-profiles/#OWL_2_RL

[OWL-RL is] designed to accommodate both OWL 2 applications that can trade the full expressivity of the language for efficiency ...

This is achieved by defining a syntactic subset of OWL 2 which is amenable to implementation using rule-based technologies ... and presenting a partial axiomatization of the OWL 2 RDF-Based Semantics

a suitable rule-based implementation ... will have desirable computational properties; for example, it can return all and only the correct answers to certain kinds of query

Such an implementation can also be used with arbitrary RDF graphs. In this case, however, these properties no longer hold — in particular, it is no longer possible to guarantee that all correct answers can be returned

And in the Computational Properties section: https://www.w3.org/TR/owl2-profiles/#Computational_Properties

OWL-RL is PTIME-complete

PTIME is the class of problems solvable by a deterministic algorithm using time that is at most polynomial in the size of the input.

So by using a brute-force axiomatic rule-base approach (for performance, efficiency, and simplicity reasons), this implementation conforms to OWL-RL entailments/inferences but does not go as far as to automatically solve this kind of puzzle.

It seems to me that solving this puzzle would require the integration of a backtracking-capable Constraint Solving Problem resolver (CSP) such as https://labix.org/python-constraint. The OWL inferencer could build the constraints using an OWL->CSP axiom mapping, then after the OWL inferencing has finished, it could run the CSP resolver to get the solutions and plug them into the graph.

Unfortunately by doing this, it introduces a further layer of complexity to the OWL inferencer, and will significantly slow down the inferencing process. Furthermore, by doing this the problem is no longer solvable in PTIME, and is starting to stray away from the strictly rule-based approach of OWL-RL (correct me if I'm wrong).

[blokhin]

@ashleysommer many thanks for your kind explanation. Actually, @wrobell tried to solve this riddle as a case study for FaCT++ reasoning using his new Python bindings for rdflib and, although succeeded, found an uncontrolled performance degradation. So indeed this riddle is difficult.

[blokhin]

Well, it's not the Einstein's riddle is difficult, it's that the OWL2 QL/RL is difficult :)

And as far as I understand, the only way to tackle this difficulty is to resolve for heuristics... causing sometimes the uncontrolled performance degradations...

[cknoll]

I think the package owlready might be a way to go. I achieved to load the above ontologies but they seem to be incompletely represented. See this notebook for details:

https://github.com/cknoll/demo-material/blob/master/expertise_system/einstein-zebra-puzzle-owlready-solution-attempt.ipynb

I think, once the ontology is correctly loaded/represented the solution could be obtained via something like owlready2.sync_reasoner_pellet(infer_property_values=True, infer_data_property_values=True)

For Reference: I have two pending questions concerning this topic:

• http://owlready.8326.n8.nabble.com/Solve-Einstein-five-house-puzzle-with-owlready-tc785.html#a2071
• https://stackoverflow.com/questions/64508106/python-solve-einstein-zebra-puzzle-with-owlready

[cknoll]

Update: with the first ontology file I now get convincing results with the pellet-reasoner:

https://github.com/cknoll/demo-material/blob/master/expertise_system/einstein-zebra-puzzle-owlready-solution1.ipynb

[nicholascar]

So I guess owlread2 is using Pellet in DL mode underneath? I don't think we have a DL reasoner in Python, or at least not one for use with RDFlib!

I now have a student looking at updating OWL-RL (and probably renaming it) and I want to see support for EL & QL, as well as the current RDFS & RL. I also want assurance that all RL reasoning is being carried out properly, but I don't have plans for DL reasoning as that's a very different thing.

[blokhin]

Out of rigorousness, here’s the solution using FaCT++ reasoner in Python.