This repository has been archived by the owner on Oct 23, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathstarting_out.tex
200 lines (172 loc) · 9.4 KB
/
starting_out.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
Remember that we defined a \emph{combinatorial problem} as finding, among a
finite set of objects, one that satisfies a set of constraints. Therefore,
every variable of our problem will have an assigned a finite set
of its possible values, also called its \emph{domain}.
Essence Prime supports two basic variable types: Boolean and integer. Booleans
by definition already have a finite domain, as they will be either true or false.
For integer variables, we will need to specifically define their domain.
The syntax for giving a name to a domain is simple:
$$\texttt{letting \textbf{name} be domain \textbf{range}}$$
Where \texttt{\textbf{name}} is the identifier and \texttt{\textbf{range}}
defines the possible integers. Possible ranges could be \texttt{int(0..9)},
\texttt{int(1,3,5,7,9)} or \texttt{int(1..4,6..9)}. A variable will be defined
using the \texttt{find} keyword instead. For example, to declare a variable
that can go from 0 to 10, you would say \texttt{find x: int(0..10)}. A Boolean
variable would be declared as \texttt{find y: bool}.
Variables can also be grouped into matrices, which can be indexed by any domain.
The syntax to declare a matrix is:
$$\texttt{letting \textbf{name} : matrix indexed by \textbf{dimensions} of \textbf{data type}}$$
where \texttt{\textbf{dimensions}} should be a list of domains in which each
element will be defining one dimension of the matrix. For example,
\texttt{[int(0..10),int(5,6), int(6..12)]} would define a 3-dimensional matrix
with a rather strange indexing. Finally, the \texttt{\textbf{data type}} will
be a domain that restricts what potential values the variables in the matrix
can take. This implicitly means that all variables in the matrix will need to
have the same possible potential values.
\begin{figure}
\begin{lstlisting}
language ESSENCE' 1.0 @\label{line-language}@
letting valid_range be domain int(1..10)
find vector : matrix indexed by [int(1..3)] of valid_values
such that@\label{line-suchthat}@
vector[1] < vector[2],
vector[2] < vector[3]
\end{lstlisting}
\caption{A toy problem}
\label{fig-toyexample}
\end{figure}
Figure~\ref{fig-toyexample} shows our first model with these concepts in
action. The first line is expressing what version of the language we are
using. In this case, it is Essence Prime version 1.0. We are trying to find an
increasing sequence of 3 values, where each one of them can take a value from 1
to 10. After defining all the variables, domains and constants,
Line~\ref{line-suchthat} defines that everything that comes later on is a
comma-separated sequence of constraints.
If we write this model down in a file called \texttt{toy.eprime}, we can ask
Savile Row for a model:
$$\texttt{\$savilerow -run-solver -solutions-to-stdout toy.eprime}$$
If Savile Row is correctly installed, it should say something similar to
Figure~\ref{fig-output1}. Note that our \texttt{vector} matrix has been filled
up with values that respect the constraints that we have imposed. Note that
there are two time measurements, \texttt{minion} and \texttt{Savile Row}. The
former refers to the time taken by the background solver to solve the problem,
while the latter refers to the translation time needed by Savile Row to adapt
the model to the specifics of the solver. In this case, minion is a constraints
solver, the default for Savile Row.
\begin{figure}
\begin{verbatim}
Created output file for domain filtering toy.eprime.minion
Created output file toy.eprime.minion
language ESSENCE' 1.0
$ Minion SolverNodes: 4
$ Minion SolverTotalTime: 0.000304
$ Minion SolverTimeOut: 0
$ Savile Row TotalTime: 0.054
letting vector be [1, 2, 3]
----------
Created information file toy.eprime.info
\end{verbatim}
\caption{Savile Row output from Figure~\ref{fig-toyexample}}
\label{fig-output1}
\end{figure}
More specifics of the performance and result will be written to the file with
the \texttt{.info} extension. If we omit the \texttt{-solutions-to-stdout} flag
in the command line, the solution will be also written in a file.
\section{Optimally Moving Out}
As our first fully fledged example, imagine that you are emigrating to a new country. For
your journey, the airline will be limiting the total weight of your luggage to
50kg. To make sure you do not forget anything, you made a list of all the
items that you will need. Sadly their total weight surpasses the allowed limit,
so you will need to decide which elements you leave behind.
In this scenario the smart thing to do is to use all the available weight. So
you start by making a list of the elements and their weight to figure out what
is the best combination.
Figure~\ref{fig-knapsack1param} shows how we can express this list in Essence Prime.
% TODO - move explicit names down
The astute reader will have noticed that the file extension in
Figure~\ref{fig-knapsack1param} is \texttt{param} instead of \texttt{eprime}.
We will generally express the data for our problem, or the \emph{instance}, in
one file with the \texttt{.param} extension. The constraints of the problem
will reside in the \emph{problem} file, with the \texttt{.eprime} extension.
This split between data and constraints is not enforced, but is generally
useful. Imagine that your friend is also emigrating with you, and therefore
has to take the same kind of decision. By being able to separate the data in a
separate instance file, we will modularise the problem and avoid the inherent
problems of copy-pasting code around.
%It would still be a valid problem if the data and constraints both resided in
%the \texttt{luggage.eprime}.
%named \texttt{my\_luggage.param}. You can see it in
%Figure~\ref{fig-knapsack1param}.
%file (Figure~\ref{fig-knapsack1}), named
%\texttt{luggage.eprime}.
%\texttt{friend\_luggage.param}
\begin{figure}
\begin{lstlisting}
language ESSENCE' 1.0
letting weights=[10, 30, 25, 12, 5, 15, 28] @\label{line-weights}@
\end{lstlisting}
\caption{Our \emph{instance}: The contents of the file
\texttt{my\_luggage.param}, listing all weights}
\label{fig-knapsack1param}
\end{figure}
The second line of Figure~\ref{fig-knapsack1param} lists the
weights of our objects. We use the \texttt{letting} keyword to define a new
variable named \texttt{weights}, which is a list of integers. We know it
is a list because the values are wrapped in square brackets.
Now that we have recorded the weights of all the elements we want carry with us,
we can model the problem very concisely with Essence Prime. Figure~\ref{fig-knapsack1}
shows how this could be done.
\begin{figure}
\begin{lstlisting}
language ESSENCE' 1.0
letting weight_limit be 50
given weights : matrix indexed by [int(0..objects)] of int(1..) @\label{line-given1dmatrix}@
find choosen : matrix indexed by [int(0..objects)] of bool @\label{line-find1dmatrix}@
such that
(sum i : int(0..objects) . choosen[i] * weights[i]) = weight_limit @\label{line-sumconstraint}@
\end{lstlisting}
\caption{Our \emph{problem}: The contents of the \texttt{luggage.eprime}
file, with a model able to decide what to bring with us.}
\label{fig-knapsack1}
\end{figure}
In addition to the \texttt{letting} and \texttt{find} keywords, there is one
more important keyword: \texttt{given}. It is used to specify that the data is
coming from an instance file. In Figure~\ref{fig-knapsack1},
Line~\ref{line-given1dmatrix} is `reading' the one-dimensional \texttt{weights}
matrix. Note though that the \texttt{objects} identifier is being
\emph{implicitly} defined here. It will be an integer that will take the value
of the length of the input matrix. For example, considering
Figure~\ref{fig-knapsack1param} as input it will take the value 6.
Now, Line~\ref{line-find1dmatrix} starts with the \texttt{find} keyword.
It also defines a one-dimensional matrix, but now made of Boolean variables. As
we have used the \texttt{find} keyword, remember that the value for each
variable will have to be found by the solver. The length of the matrix is the
same as the \texttt{weights} matrix, so as you can imagine the value of each
cell in this matrix will decide if we take each corresponding object in our
luggage or not. For example, if \texttt{choosen[i] = true}, it will mean that
we will take the \texttt{i}th object.
Finally, we have to tell the solver the restrictions we are operating under.
Line~\ref{line-sumconstraint} accomplishes that, restricting that the sum of
the objects we take is exactly equal as the weight limit.
The \texttt{sum} operator goes through all the objects via the temporary
variable \texttt{i}. For each object it adds the multiplication of
\texttt{choosen[i] * weights[i]} to the sum. The astute reader will see that
the types here do not match: \texttt{choosen[i]} is a Boolean, while
\texttt{weights[i]} is an integer. In this situation, Savile Row will be
intelligent enough to automatically cast the Booleans to a 0/1.
\begin{itemize}
\item explain intuitively how the solver approaches the solution of the problem
\item show how to execute SR and get a solution
\item consider the full knapsack problem by considering the monetary value of each object
and maximizing the cost of everything we select while respecting the weigth limit
\end{itemize}
\section{Basic building blocks}
what is an instance or a problem
How to define a variable and a constraint
\section{Solving a Problem}
Pick a toy problem to demonstrate everything
Invoking SR from the command line
\section{Optimising a Solution}
optimisation
% calcudoku might be a nice twist on the classic sudoku puzzle
%https://newdoku.com/include/print.php?n=3&lang=en&op=1&nd=1