Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Work on the flattening section

Browse Source
This commit is contained in:
Jip J. Dekker 2021-05-16 15:18:41 +10:00
parent 7c131f7412
commit cc5d1fd016
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
3 changed files with 237 additions and 119 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
assets/acronyms.tex
View File

@ -49,3 +49,5 @@
\newacronym[see={[Glossary:]{gls-trs}}]{trs}{TRS\glsadd{gls-trs}}{Term Rewriting
System}
\newacronym{tsp}{TSP\glsadd{gls-trs}}{Travelling Salesperson Problem}

2
assets/packages.tex
View File

@ -44,8 +44,6 @@ BoldItalicFont=*-BoldItalic,
\usepackage{amssymb}
\usepackage{unicode-math}
\renewcommand{\thefootnote}{\fnsymbol{footnote}}
% References
\usepackage[
style=apa,

352
chapters/2_background.tex
View File

@ -637,6 +637,11 @@ We will now discuss some of the other prominent \cmls{} and will compare them to
\minizinc\ to indicate to the reader where techniques might have to be adjusted
to fit other languages.
A notable difference between all these these languages and \minizinc\ is that
only \minizinc\ allows modellers to extend the language using their own
(user-defined) functions. In other \cmls\ the modeller is restricted to the
expressions and functions provided by the language.
\subsection{AMPL}%
\label{sub:back-ampl}
@ -660,7 +665,8 @@ has even been extended to allow the usage of certain \glspl{global} when using a
\begin{example}
The following
If we consider the well-known \gls{tsp}, then we might model this problem in
\gls{ampl} as follows:
\begin{plain}
set Cities ordered;
@ -682,6 +688,15 @@ has even been extended to allow the usage of certain \glspl{global} when using a
sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (j,i) in Paths} X[j,i] >= 2;
\end{plain}
This model shows that the \gls{ampl} syntax has many features similar to
\minizinc{}. Like \minizinc{}, \gls{ampl} has an extensive expression
language, which includes \gls{generator} expressions and a vast collection of
\glspl{operator}. The building block of the model are also similar:
\gls{parameter} declarations, \gls{variable} declarations, \glspl{constraint},
and a solving goal.
The same problem can be modelled in \minizinc\ as follows:
\begin{mzn}
enum CITIES;
array[CITIES, CITIES] of int: cost;
@ -693,8 +708,20 @@ has even been extended to allow the usage of certain \glspl{global} when using a
solve minimize sum(i in CITIES) (cost[i, next[CITIES]]);
\end{mzn}
Even though the \gls{ampl} is similar to \minizinc{}, the models could not be
more different. The main reason for this difference is the level at which
these models are written. The \gls{ampl} model is written to target a
\gls{mip} solver. In the \gls{ampl} language this means that you can only use
the language functionality that is compatible with the targeted \gls{solver};
in this case, all expression have to be linear equations. In \minizinc\ the
modeller is not constrained in the same way. The modeller is always encouraged
to create high-level \gls{constraint} models. It is the job of the
\gls{solver}'s \minizinc\ library to transform the high-level constraints into
compatible \gls{solver}-level \glspl{constraint}.
\end{example}
\subsection{OPL}%
\label{sub:back-opl}
@ -708,66 +735,71 @@ Resources and activities are separate objects in the \gls{opl}. This allows
users express resource scheduling \glspl{constraint} in an incremental and more
natural fashion. When solving a scheduling problem, the \gls{opl} makes use of
specialised \gls{interval} \glspl{variable}, which represent when a task will be
scheduled. For example the \gls{variable} declarations and \glspl{constraint}
for a jobshop problem would look like this in an \gls{opl} model:
scheduled.
\begin{plain}
ScheduleHorizon = sum(j in Jobs, t in Tasks) duration[j, t];
Activity task[j in Jobs, t in Tasks] (duration[j,t]);
Activity makespan;
UnaryResource tool[Machines];
\begin{example}
For example the \gls{variable} declarations and \glspl{constraint}
for a jobshop problem would look like this in an \gls{opl} model:
minimize makespan.end
subject to {
forall (j in Jobs)
task[j,nbTasks] precedes makespan;
\begin{plain}
ScheduleHorizon = sum(j in Jobs, t in Tasks) duration[j, t];
Activity task[j in Jobs, t in Tasks] (duration[j,t]);
Activity makespan;
UnaryResource tool[Machines];
forall (j in Jobs)
forall (t in 1..nbTasks-1)
task[j, t] precedes task[j, t+1];
minimize makespan.end
subject to {
forall (j in Jobs)
task[j,nbTasks] precedes makespan;
forall (j in Jobs)
forall (t in Tasks)
task[j, t] requires tool[resource[j, t]];
};
\end{plain}
forall (j in Jobs)
forall (t in 1..nbTasks-1)
task[j, t] precedes task[j, t+1];
The equivalent declarations and \glspl{constraint} would look like this in
\minizinc{}:
forall (j in Jobs)
forall (t in Tasks)
task[j, t] requires tool[resource[j, t]];
};
\end{plain}
\begin{mzn}
int: horizon = sum(j in Jobs, t in Tasks)(duration[j,t]);
var 0..horizon: makespan;
array[JOB,TASK] of var 0..maxt: start;
The equivalent declarations and \glspl{constraint} would look like this in
\minizinc{}:
constraint forall(j in Jobs, t in 1..nbTasks-1) (
start[j,t] + duration[j,t] <= start[j,t+1]
);
\begin{mzn}
int: horizon = sum(j in Jobs, t in Tasks)(duration[j,t]);
var 0..horizon: makespan;
array[JOB,TASK] of var 0..maxt: start;
constraint forall(j in Jobs) (
start[j, nbTasks] + duration[j, nbTasks] <= makespan
);
constraint forall(j in Jobs, t in 1..nbTasks-1) (
start[j,t] + duration[j,t] <= start[j,t+1]
);
constraint forall(m in Machines) (
disjunctive(
[start[j,t] | j in Jobs, t in Tasks where resource[j,t] == m],
[duration[j,t] | j in Jobs, t in Tasks where resource[j,t] == m],
)
);
constraint forall(j in Jobs) (
start[j, nbTasks] + duration[j, nbTasks] <= makespan
);
solve minimize makespan;
\end{mzn}
constraint forall(m in Machines) (
disjunctive(
[start[j,t] | j in Jobs, t in Tasks where resource[j,t] == m],
[duration[j,t] | j in Jobs, t in Tasks where resource[j,t] == m],
)
);
Note that the \minizinc{} model does not have explicit Activity variables. It
must instead use \glspl{variable} that represent the start times of the activity
and a \gls{variable} to represent the time at which all activities are finished.
The \gls{opl} model also has the advantage that it can first create resource
objects and then use the \texttt{requires} keyword to force tasks on the same
machine to be mutually exclusive. In \minizinc{} the same requirement is
implemented through the use of \mzninline{disjunctive} constraints. Although
this has the same effect, all mutually exclusive jobs have to be combined in a
single statement in the model. This can make it harder in \minizinc\ to write
the correct \gls{constraint} and its meaning might be less clear.
solve minimize makespan;
\end{mzn}
Note that the \minizinc{} model does not have explicit Activity variables. It
must instead use \glspl{variable} that represent the start times of the activity
and a \gls{variable} to represent the time at which all activities are finished.
The \gls{opl} model also has the advantage that it can first create resource
objects and then use the \texttt{requires} keyword to force tasks on the same
machine to be mutually exclusive. In \minizinc{} the same requirement is
implemented through the use of \mzninline{disjunctive} constraints. Although
this has the same effect, all mutually exclusive jobs have to be combined in a
single statement in the model. This can make it harder in \minizinc\ to write
the correct \gls{constraint} and its meaning might be less clear.
\end{example}
The \gls{opl} also contains a specialised search syntax that can be used to
instruct its solvers \autocite{van-hentenryck-2000-opl-search}. This syntax
@ -797,10 +829,6 @@ search mechanism and that the \gls{solver} reasons about search on the same
level as the \gls{opl} model. It is therefore not possible to connect other
\glspl{solver} to \gls{opl}.
The \gls{opl} does not allow modellers to create their own (user-defined)
functions. A modeller is restricted to the \gls{global} constraint library
provided by the \gls{opl}'s standard library.
\subsection{Essence}%
\label{sub:back-essence}
@ -822,66 +850,69 @@ types can be arbitrary nested and the modeller can define, for example, a
finite types. These types in \gls{essence} are restricted to Booleans,
enumerated types, or a restricted set of integers.
For example, the Social Golfers Problem, can be modelled in \gls{essence} as
follows:
\begin{example}
Consider, for example, the Social Golfers Problem, can be modelled in
\gls{essence} as follows:
\begin{plain}
language Essence 1.3
\begin{plain}
language Essence 1.3
given w, g, s : int(1..)
given w, g, s : int(1..)
letting Golfers be new type of size g * s
letting Golfers be new type of size g * s
find sched : set (size w) of
partition (regular, numParts g, partSize s) from Golfers
find sched : set (size w) of
partition (regular, numParts g, partSize s) from Golfers
such that
such that
forAll g1, g2 : Golfers, g1 < g2 .
(sum week in sched . toInt(together({g1, g2}, week))) <= 1
\end{plain}
forAll g1, g2 : Golfers, g1 < g2 .
(sum week in sched . toInt(together({g1, g2}, week))) <= 1
\end{plain}
In \minizinc{} the same problem could be modelled as:
In \minizinc{} the same problem could be modelled as:
\begin{mzn}
include "globals.mzn";
\begin{mzn}
include "globals.mzn";
int: g;
int: w;
int: s;
int: g;
int: w;
int: s;
enum: golfers = anon_enum(g * s);
enum: golfers = anon_enum(g * s);
set of int: groups = 1..g;
set of int: rounds = 1..w;
array [rounds, groups] of var set of golfers: group;
set of int: groups = 1..g;
set of int: rounds = 1..w;
array [rounds, groups] of var set of golfers: group;
constraint forall (r in rounds, g in groups) (
card(group[r, g]) = s
);
constraint forall (r in rounds, g in groups) (
card(group[r, g]) = s
);
constraint forall(r in rounds) (
all_disjoint(g in groups)(group[r, g])
);
constraint forall(r in rounds) (
all_disjoint(g in groups)(group[r, g])
);
constraint forall (a, b in golfers where a < b) (
sum (r in rounds, g in groups) (
{a, b} subset group[r, g]
) <= 1
);
\end{mzn}
constraint forall (a, b in golfers where a < b) (
sum (r in rounds, g in groups) (
{a, b} subset group[r, g]
) <= 1
);
\end{mzn}
Note that, through the \gls{essence} type system, the first 2 \glspl{constraint}
in the \minizinc{} are implied in the \gls{essence} model. This is an example
where the use of high-level types can help give the modeller create more concise
models.
Note that, through the \gls{essence} type system, the first 2
\glspl{constraint} in the \minizinc{} are implied in the \gls{essence} model.
This is an example where the use of high-level types can help give the
modeller create more concise models.
These high-level variables are often not directly supported by the
\glspl{solver} that is employed to solve \gls{essence} instances. To solve the
problem, not only do the \glspl{constraint} have to be translated to
\glspl{constraint} supported by the solver, but also all \glspl{variable} have
to be translated to a combination of \glspl{constraint} and \glspl{variable}
compatible with the targeted solver.
\end{example}
The high-level variables available in \gls{essence} are often not directly
supported by the \glspl{solver} that is employed to solve \gls{essence}
instances. To solve the problem, not only do the \glspl{constraint} have to be
translated to \glspl{constraint} supported by the solver, but also all
\glspl{variable} have to be translated to a combination of \glspl{constraint}
and \glspl{variable} compatible with the targeted solver.
\section{Term Rewriting}%
\label{sec:back-term}
@ -1135,32 +1166,119 @@ and the call itself is a constraint primitive for the target \gls{solver}.
To arrive at a flat model, the flattening process will transverse the
declarations, \glspl{constraint}, and the solver goal and flatten any expression
contained in these items. The flattening of an expression is a recursive
process. \Gls{parameter} literals and \gls{variable} identifiers are already
flat. For any other kind of expression, its arguments are first flattened. If
the expression itself is a constraint primitive, then it is ready
contained in these items. During the flattening of an expression, the expression
rewritten into other \minizinc\ expressions according to the decomposition given
in the target \gls{solver}'s \minizinc\ library. Enforced by \minizinc{}'s type
system, at most one rule applies for any given constraint. The flattening of
expressions is performed bottom-up, we flatten any sub-expression before its
parent expression. For instance, in a call each argument is flattened before the
call itself is flattened.
\jip{This should say something about introducing relational reified constraints.}
An exception to this bottom-up approach is the flattening of \gls{generator}
expressions. Expression containing \glspl{generator}, such as array
\glspl{comprehension} and loops, have to be instantiated before their
sub-expression can be flattened. The compiler exhaustively binds the values of
the \gls{generator} to the specified identifiers. For each iteration the
compiler flattens the sub-expression and collects its result. Once the
\gls{generator} is exhausted, the compiler can flatten its surrounding
expression using the collected values.
The decomposition system in \minizinc\ is defined in terms of functions
declarations. Any call, whose declaration has a function body, will eventually
be replaced by an instantiation of this function body using the arguments to the
call. Calls are, however, not the only type of expression that are decomposed
during the flattening process. Other expression, like \gls{operator}
expressions, variable array access, and if-then-else expressions, might also
have to be decomposed for the targeted \gls{solver}. During the flattening
process, these expressions are rewritten into equivalent call expressions that
will start the decomposition process.
A notable effect of the flattening is that sub-expression are replaced by
literals or identifiers. If the expression contains only \glspl{parameter}, then
the flattening of the expression is merely a calculation to find the value of
the literal to be put in its place. If, however, the expression contains a
\gls{variable}, then this calculation cannot be performed during the flattening
process. Instead, a new \gls{variable} must be created to represent the value of
the sub-expression and it must be constrained to take the value corresponding to
the expression. The creation of this new \gls{variable} and defining
\glspl{constraint} happens in one of two ways:
\begin{itemize}
\item For Boolean expressions in a reified context, the new \gls{variable} is
inserted by the flattening process itself. To constrain this
\gls{variable}, the flattener will then add a new reified constraint.
This constraint contains a call a variation of the call that would have
been generated for the expression in root context. The name of the
function is appended with \mzninline{_reif} and an extra Boolean
\gls{variable} argument is added to the call. The definition of this
constraint should implement the reification of the original expression:
setting the additional argument to \mzninline{true} if the constraint is
satisfied, and \mzninline{false} otherwise. For example, the constraint
in \minizinc{}
\begin{mzn}
constraint b \/ this_call(x, y);
\end{mzn}
will during flattening be turned into:
\begin{mzn}
var bool: i1;
constraint this_call_reif(x, y, i1);
constraint b \/ i1
\end{mzn}
\item For other expressions, the \gls{variable} and defining
\glspl{constraint} are introduced in the definition of the function
itself. For example, the definition of the \mzninline{max} function in
the standard library, which calculates the maximum of two values, is
defined as:
\begin{mzn}
function var int: max(var int: x, var int: y) :: promise_total =
let {
var max(lb(x),lb(y))..max(ub(x),ub(y)): m ::is_defined_var;
constraint int_max(x,y,m) ::defines_var(m);
} in m;
\end{mzn}
Using a \gls{let} it explicitly creates a new \gls{variable}, constrains
this \gls{variable} to take to correct value, and returns the newly
created \gls{variable}.
\end{itemize}
These are the basic steps that are followed to flatten \minizinc\ instance. This
is, however, not the complete process. The quality of a \flatzinc\ model is of
the utmost importance. A \flatzinc\ containing extra \glspl{variable} and
\glspl{constraint} that do not add any information to the solving process might
exponentially slow down the solving process. Therefore, the \minizinc\
flattening process is extended using many techniques to help improve the quality
of the flattened model. In the remainder of this section we will discuss the
most important techniques utilised in the flattener.
\paragraph{Common Sub-expression Elimination}
Because the evaluation of a \minizinc\ expression cannot have any side-effects,
In some cases, it is even possible to not generate definitions in the first
place through the use of \gls{cse}. This simplification is a well understood
technique that originates from compiler optimisation \autocite{cocke-1970-cse}
and has proven to be very effective in discrete optimisation
\autocite{marinov-2005-sat-optimisations, araya-2008-cse-numcsp}, including
during the evaluation of \cmls\ \autocite{rendl-2009-enhanced-tailoring}.
it is possible to reuse the same result for equivalent expressions. This
simplification is a well understood technique that originates from compiler
optimisation \autocite{cocke-1970-cse} and has proven to be very effective in
discrete optimisation \autocite{marinov-2005-sat-optimisations,
araya-2008-cse-numcsp}, including during the evaluation of \cmls\
\autocite{rendl-2009-enhanced-tailoring}.
For instance, in the constraint\\
\begin{mzn}
constraint (abs(x)*2 >= 20) \/ (abs(x)+5 >= 15);
\end{mzn}
\begin{example}
For instance, in the constraint
the expression \mzninline{abs(x)} is occurs twice. There is however no need to
create two separate \glspl{variable} (and defining \glspl{constraint}) to
represent the absolute value of \mzninline{x}. The same \gls{variable} can be
used to represent the \mzninline{abs(x)} in both sides of the disjunction.
\begin{mzn}
constraint (abs(x)*2 >= 20) \/ (abs(x)+5 >= 15);
\end{mzn}
the expression \mzninline{abs(x)} is occurs twice. There is however no need to
create two separate \glspl{variable} (and defining \glspl{constraint}) to
represent the absolute value of \mzninline{x}. The same \gls{variable} can be
used to represent the \mzninline{abs(x)} in both sides of the disjunction.
\end{example}
Seeing that the same expression occurs multiple times is not always easy. Some
expressions only become syntactically equal during evaluation, as in the