Einstein's riddle

Have you ever tried to solve the famous Einstein's logic puzzle? It is claimed that only 2% of the world's population can solve it!
A Description Logic reasoner can do it for you just in one click. Below is a formulation of the puzzle in ALCOIF description logic:


The ontology has been created using Protege 4.0. It contains the original formulation of the puzzle taken from http://en.wikipedia.org/wiki/Zebra_puzzle. For convenience, all key axioms in the ontology are provided with annotation, a corresponding condition of the puzzle.

Just classify this ontology in Protege and get a solution by clicking on individuals!

The formalization of Einstein's puzzle in a description logic is just one way to solve it automatically. It is a compact (in the number of signature symbols used) and convenient (close to natural language) presentation of the puzzle. Note however that these kinds of puzzles can be easily formalized in pure propositional logic and solved by SAT solvers. Typically, a riddle can be viewed as a k×n matrix and encoded as a SAT problem with k×n2 propositional variables. For 1 ≤ i ≤ k, 1 ≤ j ≤ n, and 1 ≤ m ≤ n, we consider a variable Pijm to be true iff the (i,j)-entry in the matrix has value m.

Finally, here is the formulation of the riddle from http://en.wikipedia.org/wiki/Zebra_puzzle:

  1. There are five houses.
  2. The Englishman lives in the red house.
  3. The Spaniard owns the dog.
  4. Coffee is drunk in the green house.
  5. The Ukrainian drinks tea.
  6. The green house is immediately to the right of the ivory house.
  7. The Old Gold smoker owns snails.
  8. Kools are smoked in the yellow house.
  9. Milk is drunk in the middle house.
  10. The Norwegian lives in the first house.
  11. The man who smokes Chesterfields lives in the house next to the man with the fox.
  12. Kools are smoked in a house next to the house where the horse is kept.
  13. The Lucky Strike smoker drinks orange juice.
  14. The Japanese smokes Parliaments.
  15. The Norwegian lives next to the blue house.

Now, who drinks water? Who owns the zebra?

In the interest of clarity, it must be added that each of the five houses is painted a different color, has a single inhabitant, and the inhabitants are of different national extractions, own different pets, drink different beverages and smoke different brands of American cigarettes. In statement 6, right refers to the reader's right.