Modelling with ESSENCE'
|
An extensive documentation of TAILOR and ESSENCE' can be
found here.
Essence' is a declarative modelling language to specify constraint
problems. The problem specification is usually stored in a file with
the ending .eprime and the parameters in a
.param file. An Essence' file consists of the following parts:
- Header (stating the version of Essence')
- Declarations (of constants, parameters, domains, decision
variables) [optional]
- Constraints [optional]
In the following we give some examples to illustrate how to use Essence' for modelling
CSP problems. This page is updated and extended frequently.
- A Simple Example: Send More Money
(basic model structure)
- An Advanced Example: Sudoku
(using matrix datastructures, universal quantifiers)
1. A Simple Example: Send more money
Let's construct an example by modelling the
Send More Money problem,
where one has to find a
solution to the following sum where every letter stands for a distinct
number between 0 and 9:
S E N D +
M O R E
----------
M O N E Y
We start with the header
Our decision variables are S, E, N,
D, M, O, R, Y which are in the domain of 0..9. We state that
S and M must not equal zero and define two
domains: one reaching from 0..9 and the other from 1..9. Domains and
constants can be defined by the letting statement:
language ESSENCE' 1.b.a
letting DOMAIN0 be domain int(0..9)
letting DOMAIN1 be domain int(1..9)
|
Now we can define our decision variables that range over domains
DOMAIN0
and DOMAIN1 by using the find statement.
language ESSENCE' 1.b.a
letting DOMAIN0 be domain int(0..9)
letting DOMAIN1 be domain int(1..9)
find S,M : DOMAIN1,
E,N,D,O,R,Y : DOMAIN0
|
All declarations have been done now and we can define our
constraint. The constraints are stated after such that:
language ESSENCE' 1.b.a
letting DOMAIN0 be domain int(0..9)
letting DOMAIN1 be domain int(1..9)
find S,M : DOMAIN1,
E,N,D,O,R,Y : DOMAIN0
such that
1000*S + 100*E + 10*N + D
+ 1000*M + 100*O + 10*R + E =
10000*M + 1000*O + 100*N + 10*E + Y
|
Finally, we add the constraint, that all letters
have to be different by using an "alldifferent" constraint.
"alldifferent" states that all its arguments have to take
different values.
language ESSENCE' 1.b.a
letting DOMAIN0 be domain int(0..9)
letting DOMAIN1 be domain int(1..9)
find S,M : DOMAIN1,
E,N,D,O,R,Y : DOMAIN0
such that
1000*S + 100*E + 10*N + D
+ 1000*M + 100*O + 10*R + E =
10000*M + 1000*O + 100*N + 10*E + Y ,
alldifferent([S,E,N,D,M,O,R,Y])
|
The code for the Send more money problem can be found here.
2. Advanced Example: Sudoku
Sudoku is a popular puzzle: assign each field
of the 9x9 board a number between (1..9) such that every row, column and 3x3 box contains different
numbers. A sample sudoku puzzle is given below.
|
One way of modelling this problem is to encode every field of the board as a decision variable
ranging from (1..9). To specify the constraints on the rows and columns of the board more easily,
we collect all decision variables by a matrix(array) datastructure: we define a two-dimensional
matrix (array) board, whose indices both range from (1..9), giving us a representation
of the 9x9 board.
This means that board[2,3] holds the value of the field positioned in row 2 at column 3 of the board
(in the example to the right board[2,3] is assigned the value 2).
To make our lives easier, we explicitly define the domain (1..9) to be RANGE.
Since each decision variable of the matrix (also) ranges from (1..9), the matrix-elements' domain is specified
by the keyword of to be RANGE.
So we get the first piece of our Essence' Sudoku-problem-model as follows.
|
language ESSENCE' 1.b.a
letting RANGE be domain int(1..9)
find board: matrix indexed by [RANGE, RANGE] of RANGE
|
Let us now focus on the constraints for the puzzle: the first constraint states that
each row of the board has to contain different values. This can be done by imposing
the alldifferent constraint on every row of board. We can
either write down alldifferent(board[1]), ... alldifferent(board[9]),
or just collect these constraints in a universal quantification, using forall.
forall is somewhat similiar to for-loops in
programming languages such as Java: in our example below it states that forall rows,
where row can take any value between (1..9), the expression
after the . has to hold. So it just corresponds to writing down all 9 cases
of alldifferent(board[1]), ... alldifferent(board[9]).
language ESSENCE' 1.b.a
letting RANGE be domain int(1..9)
find board: matrix indexed by [RANGE, RANGE] of RANGE
such that
forall row : int(1..9) .
alldifferent(board[row,..])
|
Then we want to impose alldifferent on all columns of the board.
language ESSENCE' 1.b.a
letting RANGE be domain int(1..9)
find board: matrix indexed by [RANGE, RANGE] of RANGE,
columns : matrix indexed by [RANGE, RANGE] of RANGE
such that
$ all rows have to be different
forall row : RANGE .
alldifferent(field[row,..]),
$ all columns have to be different
forall col : RANGE .
alldifferent(field[..,col]),
|
Now we have imposed alldifferent on both the rows and columns of
the board. It remains to state that every 3x3 box of the board contains
9 different numbers. This is quite hard to state generally. One way would be to
define another matrix with each box as row and impose alldifferent
on it, just as we have done with the columns. Another way is to simply specify
that no element in a 3x3 box may be equal to another. This is
expressed by a double-nested forall expression.
language ESSENCE' 1.b.a
letting RANGE be domain int(1..9)
find board: matrix indexed by [RANGE, RANGE] of RANGE,
columns : matrix indexed by [RANGE, RANGE] of RANGE
such that
$ all rows have to be different
forall row : RANGE .
alldifferent(field[row,..]),
$ all columns have to be different
forall col : RANGE .
alldifferent(field[..,col]),
forall i,j : int(0..2) .
forall col1,col2,row1,row2 : int(1..3) .
((col1 != col2) /\ (row1 != row2)) =>
(board[row1+(i*3), col1+(j*3)]
!= board[row2+(i*3), col2+(j*3)])
|
Now we need to specify initial values for our sudoku. Since every sudoku has
different values, these constants are parameters and to make our lives easier, we
specify them in a separate file, the parameter file (which we will do
one step later). Still, we need to declare the parameter values in our problem file:
we simply define a matrix of constants of the same size as the board which we
call values.
Additionally, we need to think of a way of representing unassigned boards, which we simply
denote with an assignement of 0. This means that
values[1,1] = 0 states that the board at index (1,1) has no
value assigned, and values[2,2]=4 states that board (2,2) has value 4.
Hence all elements of values range over the domain (0..9), which we
define as a new domain called VALUES. Finally, we need to assign
the constant values to the board:
if an element of values does not equal 0, then the
element of board at the same position equals the value of
this element of values.
language ESSENCE' 1.b.a
given values : matrix indexed by [RANGE,RANGE] of VALUES
letting RANGE be domain int(1..9)
letting VALUES be domain int(0..9)
find board: matrix indexed by [RANGE, RANGE] of RANGE,
columns : matrix indexed by [RANGE, RANGE] of RANGE
such that
$ all rows have to be different
forall row : RANGE .
alldifferent(field[row,..]),
$ all columns have to be different
forall col : RANGE .
alldifferent(field[..,col]),
forall i,j : int(0..2) .
forall col1,col2,row1,row2 : int(1..3) .
((col1 != col2) /\ (row1 != row2)) =>
(board[row1+(i*3), col1+(j*3)]
!= board[row2+(i*3), col2+(j*3)])
forall row,col : RANGE .
(values[row,col] > 0) =>
(board[row,col] = values[row,col])
|
Now all we need to do is specify our parameter values for our sudoku instance.
This is done by writing it into a parameter file with the file extension .param.
A parameter file for our sudoku problem could look like this (the sudoku instance is given in
the comment):
language ESSENCE' 1.b.a
$ 5 3 0 | 0 7 0 | 0 0 0
$ 6 0 0 | 1 9 5 | 0 0 0
$ 0 9 8 | 0 0 0 | 0 6 0
$ ---------------------
$ 8 0 0 | 0 6 0 | 0 0 3
$ 4 0 0 | 8 0 3 | 0 0 1
$ 7 0 0 | 0 2 0 | 0 0 6
$ ---------------------
$ 0 6 0 | 0 0 0 | 2 8 0
$ 0 0 0 | 4 1 9 | 0 0 5
$ 0 0 0 | 0 8 0 | 0 7 9
letting values be [ [ 5, 3, 0, 0, 7, 0, 0, 0 ,0 ],
[ 6, 0, 0, 1, 9, 5, 0, 0, 0 ],
[ 0, 9, 8, 0, 0, 0, 0, 6, 0 ],
[ 8, 0, 0, 0, 6, 0, 0, 0, 3 ],
[ 4, 0, 0, 8, 0, 3, 0, 0, 1 ],
[ 7, 0, 0, 0, 2, 0, 0, 0, 6 ],
[ 0, 6, 0, 0, 0, 0, 2, 8, 0 ],
[ 0, 0, 0, 4, 1, 9, 0, 0, 5 ],
[ 0, 0, 0, 0, 8, 0, 0, 7, 9 ]]
|
The code for the Sudoku problem file can be found here at sudoku.eprime
and the parameter file for sudoku: sudoku1.param.
More examples can be found here.
|