Sudoku

Tip

Use the icon in the top right to see the source code for this page.

Example instance

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

Predicate Summary

Name	Definition	Type
sudoku/3	Describes a sudoku board. The value of cell (X,Y) is V.
initial/3	Initial values of the sudoku board. The value of cell (X,Y) is V.
pos/2	The cell (X,Y) is in the sudoku board.
subgrid/3
val/1	The value V is a possible value for a cell.

Dependency Graph

flowchart LR
    val/1(["val/1"])
    pos/2(["pos/2"])
         val/1 --> pos/2
    subgrid/3(["subgrid/3"])
         pos/2 --> subgrid/3
    sudoku/3(["sudoku/3"])
         initial/3 --> sudoku/3
         pos/2 --> sudoku/3
         val/1 --> sudoku/3
    initial/3(["initial/3"])
    classDef all fill:#00000000
    class __tmp,val/1,pos/2,subgrid/3,sudoku/3,initial/3, all;
    classDef out stroke:#52BF54,stroke-width:3px;
    class __tmp,sudoku/3, out;
    classDef aux stroke:#848484,stroke-width:0.2px;
    class __tmp,val/1,pos/2,subgrid/3,initial/3, aux;
    classDef in stroke:#9178C6,stroke-width:3px;
    class initial/3, in;

Encodings

examples/sudoku/encoding.lp

Source

% # Sudoku Puzzle
%   Uses the well known [puzzle](https://en.wikipedia.org/wiki/Sudoku)
%

#const dim = 3.
val(1..dim*dim).
pos(X,Y) :- val(X), val(Y).

%*
#sudoku(X,Y,V).
Describes a sudoku board. The value of cell (X,Y) is V.
#parameters
- X: the row of the cell
- Y: the column of the cell
- V: the value of the cell

*%
%*
#initial(X,Y,V).
Initial values of the sudoku board. The value of cell (X,Y) is V.


#parameters
- X: the row of the cell
- Y: the column of the cell
- V: the value of the cell
*%
%*
#pos(X,Y).
The cell (X,Y) is in the sudoku board.

#parameters
- X: the row of the cell
- Y: the column of the cell
*%
%*
#val(V).
The value V is a possible value for a cell.

#parameters
- V: the value
*%


subgrid(X,Y,(((X-1)/dim)*dim+((Y-1)/dim))) :- pos(X,Y).

% A choice rule for each cell
1 { sudoku(X,Y,V) : val(V) } 1 :- pos(X,Y).

%## Constraints
:- sudoku(X,Y,V), sudoku(X',Y,V), X != X'.
:- sudoku(X,Y,V), sudoku(X,Y',V), Y != Y'.
:- sudoku(X,Y,V), sudoku(X',Y',V), subgrid(X,Y,S), subgrid(X',Y',S), (X,Y)!=(X',Y').

sudoku(X,Y,V) :- initial(X,Y,V).

%## Shows

#show .
#show sudoku/3.

Encoding

Sudoku Puzzle

Uses the well known puzzle

#const dim = 3.
val(1..dim*dim).
pos(X,Y) :- val(X), val(Y).
subgrid(X,Y,(((X-1)/dim)*dim+((Y-1)/dim))) :- pos(X,Y).

A choice rule for each cell

1 { sudoku(X,Y,V) : val(V) } 1 :- pos(X,Y).

Constraints

:- sudoku(X,Y,V), sudoku(X',Y,V), X != X'.
:- sudoku(X,Y,V), sudoku(X,Y',V), Y != Y'.
:- sudoku(X,Y,V), sudoku(X',Y',V), subgrid(X,Y,S), subgrid(X',Y',S), (X,Y)!=(X',Y').
sudoku(X,Y,V) :- initial(X,Y,V).

Shows

#show .
#show sudoku/3.

---

Glossary

sudoku(X,Y,V)

Describes a sudoku board. The value of cell (X,Y) is V.

Parameter	Description
X	the row of the cell
Y	the column of the cell
V	the value of the cell

References

examples/sudoku/encoding.lp

  1 { sudoku(X,Y,V) : val(V) } 1 :- pos(X,Y).

  :- sudoku(X,Y,V), sudoku(X',Y,V), X != X'.

  :- sudoku(X,Y,V), sudoku(X',Y,V), X != X'.

  :- sudoku(X,Y,V), sudoku(X,Y',V), Y != Y'.

  :- sudoku(X,Y,V), sudoku(X,Y',V), Y != Y'.

  :- sudoku(X,Y,V), sudoku(X',Y',V), subgrid(X,Y,S), subgrid(X',Y',S), (X,Y)!=(X',Y').

  :- sudoku(X,Y,V), sudoku(X',Y',V), subgrid(X,Y,S), subgrid(X',Y',S), (X,Y)!=(X',Y').

  sudoku(X,Y,V) :- initial(X,Y,V).

  #show sudoku/3.

initial(X,Y,V)

Initial values of the sudoku board. The value of cell (X,Y) is V.

Parameter	Description
X	the row of the cell
Y	the column of the cell
V	the value of the cell

References

examples/sudoku/encoding.lp

  sudoku(X,Y,V) :- initial(X,Y,V).

pos(X,Y)

The cell (X,Y) is in the sudoku board.

Parameter	Description
X	the row of the cell
Y	the column of the cell

References

examples/sudoku/encoding.lp

  pos(X,Y) :- val(X), val(Y).

  subgrid(X,Y,(((X-1)/dim)*dim+((Y-1)/dim))) :- pos(X,Y).

  1 { sudoku(X,Y,V) : val(V) } 1 :- pos(X,Y).

subgrid(A, B, C)

References

examples/sudoku/encoding.lp

  subgrid(X,Y,(((X-1)/dim)*dim+((Y-1)/dim))) :- pos(X,Y).

  :- sudoku(X,Y,V), sudoku(X',Y',V), subgrid(X,Y,S), subgrid(X',Y',S), (X,Y)!=(X',Y').

  :- sudoku(X,Y,V), sudoku(X',Y',V), subgrid(X,Y,S), subgrid(X',Y',S), (X,Y)!=(X',Y').

val(V)

The value V is a possible value for a cell.

Parameter	Description
V	the value

References

examples/sudoku/encoding.lp

  val(1..dim*dim).

  pos(X,Y) :- val(X), val(Y).

  pos(X,Y) :- val(X), val(Y).

  1 { sudoku(X,Y,V) : val(V) } 1 :- pos(X,Y).