Sudoku

Note

View the source code for this example here.

Sudoku is a logic puzzle where the objective is to fill a 4x4 or 9x9 grid with digits so that each column, each row, and each of the nine 2x2 or 3x3 subgrids contains all of the digits from 1 to 4 / 9. In ASP solvers for this problem are often implemented using a generate and test approach. Explaining queries for encodings like this can be challenging since they often lead to big explanation graphs containing many nodes. To address this, asplain's pruning fuctionality can be used to reduce the size of the explanation graph and make an interpretation easier.

Illustration of a sudoku Instance

Usage

Basic Explanation (No Pruning):

asplain examples/sudoku/encoding.lp examples/sudoku/instance4x4.lp --query "sudoku(3,2,1)"

asplain examples/sudoku/encoding.lp examples/sudoku/instance9x9.lp --query "sudoku(2,2,2)"

Simplified Explanation (CHANGES + ORPHANS Pruning):

asplain examples/sudoku/encoding.lp examples/sudoku/instance4x4.lp --query "sudoku(3,2,1)" --prune CHANGES --prune ORPHANS

asplain examples/sudoku/encoding.lp examples/sudoku/instance9x9.lp --query "sudoku(2,2,2)" --prune CHANGES --prune ORPHANS

Dynamic tags

Instead of annotating the encoding with static tags, dynamic tags can be used to tag the nodes in the explanation graph based on their relation to other nodes.

asplain examples/sudoku/encoding.lp examples/sudoku/instance4x4-no-tags.lp --query "sudoku(1,1,2)" --dynamic-tags examples/sudoku/dynamic-tags.lp

Encodings

Base Encoding:

% @label("The solution has value {} in position ({},{})",(N,X,Y,)) :: sudoku(X,Y,N)
% @label("The problem has the initial value {} at position ({},{})",(N,X,Y,)) :: initial(X,Y,N)
% @label("The cell ({},{}) is part of subgrid {}",(X1,Y1,S)) :: subgrid(X1,Y1,S)
% @label("{} is a number",(N,)) :: number(N)

dim(dim).
number(1..dim*dim).

% @label("Initals assign cell ({},{}) the value {}",(X,Y,N,))
sudoku(X,Y,N) :- initial(X,Y,N).
% @label("Choose a value for cell ({},{})",(X,Y,))
{sudoku(X,Y,N): number(N)} :- number(X), number(Y).
% Cardinality
% @label("Cell ({},{}) cannot have two different values",(X,Y,))
% @hide
:- number(X), number(Y), sudoku(X,Y,N), sudoku(X,Y,N2), N>N2.
% @label("Cell ({},{}) has value {} so it's defined",(X,Y,V,))
% @hide
defined(X,Y):- sudoku(X,Y,V).
% @label("Cell ({},{}) has to be defined",(X,Y,))
% @hide
:- number(X), number(Y), not defined(X,Y).

%## Sudoku Rules

% @label("Number {} cannot be multiple times in the row {}, but appears in columns {} and {}",(N,Y,X1,X2,))
:- sudoku(X1,Y,N), sudoku(X2,Y,N), X1>X2.
% @label("Number {} cannot be multiple times in the column {}, but appears in rows {} and {}",(N,X,Y1,Y2,))
:- sudoku(X,Y1,N), sudoku(X,Y2,N), Y1>Y2.

% @label("Cell ({},{}) is in subgrid {}",(X,Y,S,))
subgrid(X,Y,S) :- number(X), number(Y), S=(((X-1)/dim)*dim+((Y-1)/dim)).
% @label("Subgrid {} cannot have value {} in both cell ({},{}) and ({},{})",(S,V,X,Y,X2,Y2,))
:- sudoku(X,Y,V), sudoku(X2,Y2,V), subgrid(X,Y,S), subgrid(X2,Y2,S), (X,Y)<(X2,Y2).

#show sudoku/3.
#show initial/3.

Instance 4x4:

#const dim=2.


% @removable
initial(1,1,1).
% @removable
initial(4,2,2).
% @removable
initial(2,3,1).
% @removable
initial(3,4,2).

Instance 9x9:

#const dim=3.

% @removable
initial(5,1,8).
% @removable
initial(6,2,7).
% @removable
initial(7,1,4).
% @removable
initial(8,2,2).
% @removable
initial(8,1,6).
% @removable
initial(9,2,9).
% @removable
initial(3,3,9).
% @removable
initial(4,3,3).
% @removable
initial(6,3,6).
% @removable
initial(7,3,5).
% @removable
initial(8,3,7).
% @removable
initial(1,4,7).
% @removable
initial(2,4,6).
% @removable
initial(4,4,4).
% @removable
initial(7,4,9).
% @removable
initial(8,4,3).
% @removable
initial(2,5,3).
% @removable
initial(3,5,2).
% @removable
initial(4,5,8).
% @removable
initial(7,5,7).
% @removable
initial(9,5,5).
% @removable
initial(1,6,9).
% @removable
initial(2,6,1).
% @removable
initial(3,6,8).
% @removable
initial(8,6,4).
% @removable
initial(9,6,6).
% @removable
initial(1,7,6).
% @removable
initial(5,7,7).
% @removable
initial(6,7,8).