Sudoku

Sudoku

Sudoku

In this example one can see two properties of behavioral programming

• How different heuristics and pieces of knowledge about the problem domain can be used separately to program an application
• How model-checking can be used to help find a desired scenario.

Requirements

In the cells of a 9X9 grid which is also divided into 9 3X3 boxes, place the digits 1-9 such that in each row, column and box, each digit appears exactly once.

Events

• Move: A single event class with 9X9X9 = 721 instances, indicating the writing of a given digit in a given cell. The class has the following data fields:

• • number: the digit written in the cell (1-9)
  • row: The row of the cell (1-9)
  • col: the column of the cell (1-9)
  • boxrow: The row of the 3X3 box in which this cell resides (1-3)
  • boxcol: the column of the 3X3 box in which this cell resides (1-3)

When enough data is provided, the strategies below are sufficient for solving the game. When not enough data is provided, model checking explores the different possibilities until a solution is found.

Playing b-threads

• MakeGivenMoves: This b-thread provides the opening input to the riddle - filling in the known cells.
• DefaultMove: Each of the 81 instances of this b-thread class, is associated with a cell, and requests all possible 9 digits. Once an event occurs, all other events for the cell are blocked.
• DetectWin: This b-thread simply counts until 81 events have been triggered. The correctness of the solution is guaranteed
• EliminateTwoInABox: This b-thread tries to write a number in a cell after the same number was written in two other columns of this box. It does not check if the cell is occopied or if the digit was already written in the present column - this is provided by event-blocking in other b-threads.
• PlaceANumberInARow: With an instance for each digit and each row, this b-thread tries to place a particular digit in the row. It waits till there is only one place to put it, and then requests the corresponding event.
• PlaceANumberInAColumn: With an instance for each digit and each row, this b-thread tries to place a particular digit in the Column. It waits till there is only one place to put it, and then requests the corresponding event.
• EliminateEight: For each cell, an instance of this b-thread checks the possibilities for the cell, and eliminates possibilities as conflicting events occur elsewhere. When the number of remaining possibilities is one, the b-thread requests the remaining digit.

b-threads that support model-checking

PruneWhenNoSolution: This b-thread requests an event at a low priority. If it is triggered, it means that all move events are blocked, hence the game has failed. It then calls the model-checking API to prune the search.

Design Notes

• The b-thread DefaultMove could have been split into two. One that requests the default moves and terminates, and one that waits for any event in a cell and blocks all alternative digits in the cell. The present design works because a pending request of DefaultMove is unified with any granted request due to the stratgies/heuristics b-threads.