[an error occurred while processing this directive] [an error occurred while processing this directive]

Sudoku in OWL

( Ref: see the following SWIG discussion: http://lists.w3.org/Archives/Public/semantic-web/2006Jan/0077.html )

To demonstrate how a Sudoku Puzzle can be represented in OWL and then solved using an OWL-DL reasoner, we consider a simple example. The Sudoku grid below is of dimensions 4 X 4, and has four sub-grids each of dimension 2 X 2. The numbers in bold are known beforehand (i.e., represent inputs) to the puzzle.


Creating a Sudoku OWL Ontology

The OWL Ontology to represent the grid and rules of the puzzle is modeled as follows:

(a). Create OWL Individuals Vg_ij (1 <= g <= n, 1 <=  i , j <= sqroot(n), here n = 4, g = sub-grid index, i = row index, j = column index) to represent specific values in various cells of the grid. For example, create individuals (V1_11, V1_12, V1_21, V1_22) to represent values in the cells of the first sub-grid.

(b). Create OWL Individuals 1, 2, 3, 4 to represent possible values for cells in the grid. Make all four individuals mutually distinct using owl:AllDifferent.

(c). Make all the individuals in a particular row (/column) of the entire grid mutually distinct using owl:AllDifferent, e.g., make the set of individuals corresponding to the values in the first row -- (V1_11, V1_12, V2_11, V2_12)  mutually distinct.

(d). Also, make all the individuals in a particular sub-grid mutually distinct using owl:AllDifferent, e.g., make the set of individuals corresponding to the values in the first sub-grid (V1_11, V1_12, V1_21, V1_22) mutually distinct.

(e). Make the top concept, owl:Thing, a rdfs:subclassOf  the OWL Enumeration {1,2,3,4} using owl:oneOf. This implies that each individual Vg_ij in the ontology is forced to be owl:sameAs one of the individuals (1,2,3,4).

We can now specify input values for grid cells, e.g., make individual V1_12 owl:sameAs individual 4, etc...

Thats it! The final OWL Ontology should look like this*. You can now feed this Sudoku OWL ontology into a sound and complete OWL-DL reasoner (which supports nominals), such as Pellet, and the reasoner would infer values for various individuals Vg_ij based on the input specified and the constraints imposed by the axioms. The output is the following inferences: "V1_11 owl:sameAs 3", "V1_21 owl:sameAs 2"...."V4_22 owl:sameAs 3".

*Note that in the generated ontology, we have introduced a dummy class Cg_ij for each individual Vg_ij of the grid, so that the demo used below displays the solution (same individuals) as instances of the dummy class.

Try the Pellet demo here to see the results!

How this works

Consider the individual V3_12 that represents the cell (1,2) in sub-grid 3 (lower-left sub-grid).  By (b), (e), V3_12 must be owl:sameAs exclusively 1 or 2 or 3 or 4. Also, because of (c), and (d), V3_12 cannot be the same as any other individual in the same row or the same column, or within the same sub-grid.

Now the reasoner is forced to select an individual among the set (1,2,3,4) to be same as V3_12. When it tries V3_12 = 1 (i.e., V3_12 owl:sameAs 1), it discovers a contradiction or clash in the ontology because it knows V3_21 = 1 (same sub-grid clash), similarly, when it tries V3_12 = 2, it discovers a contradiction again because it knows V4_11 = 2 (same row clash), and finally, when it tries V3_12 = 4, it discovers another contradiction since it knows V1_12 = 4 (same column clash) . Thus, the reasoner is forced to infer that V3_12 = 3. The same reasoning can be applied to the remaining cell values. Hence, based on the inputs specified and the constraints of the problem, the reasoner is iteratively forced to select the correct individuals 1-4 for all the unknown cell values of the puzzle.

Play with this using Swoop / Pellet

The nightly build of Swoop (online demo) since 01/11/06 has the option to play Sudoku.  See "Advanced->Play Sudoku" under the main menu  (sample screenshot below). We also make use of the debugging/explanations techniques for OWL ontologies to provide (natural language) explanations for the answers found by Pellet.