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

Grammar and formatting work

Browse Source
This commit is contained in:
Jip J. Dekker 2021-05-20 19:12:01 +10:00
parent 0c5ede4581
commit 097d359724
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
3 changed files with 245 additions and 239 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
assets/glossary.tex
View File

@ -15,7 +15,7 @@
}
\newglossaryentry{gls-ampl}{
name={AMPL: A Mathematical Programming Language},
name={AMPL:\ A Mathematical Programming Language},
description={},
}
@ -130,7 +130,7 @@
}
\newglossaryentry{domain-con}{
name={domain consistent},
name={domain consistent},
description={},
}
@ -256,7 +256,7 @@
}
\newglossaryentry{gls-opl}{
name={OPL: The optimisation modelling language},
name={OPL:\ The optimisation modelling language},
description={},
}

472
chapters/2_background.tex
View File

@ -41,7 +41,7 @@ model.
\end{listing}
\begin{example}%
\label{ex:back-knapsack}
\label{ex:back-knapsack}
Let us consider the following scenario: Packing for a weekend trip, I have to
decide which toys to bring for my dog, Audrey. We only have a small amount of
@ -53,8 +53,8 @@ model.
\begin{equation*}
\text{maximise}~z~\text{subject to}~
\begin{cases}
S \subseteq T \\
z = \sum_{i \in S} joy(i) \\
S \subseteq T \\
z = \sum_{i \in S} joy(i) \\
\sum_{i \in S} space(i) < C \\
\end{cases}
\end{equation*}
@ -84,10 +84,10 @@ introduce \minizinc\ as the leading \cml\ used within this thesis. In
constraint model. We also briefly discuss other solving techniques and the
problem format these techniques expect. \Cref{sec:back-other-languages}
introduces alternative \cmls\ and compares their functionality to \minizinc{}.
Then,\cref{sec:back-term} survey the some closely related technologies in the
field of \glspl{trs}. Finally, \cref{sec:back-mzn-interpreter} explores the
process that the current \minizinc\ interpreter uses to translate a \minizinc\
instance into a solver-level constraint model.
Then,\cref{sec:back-term} survey the closely related technologies in the field
of \glspl{trs}. Finally, \cref{sec:back-mzn-interpreter} explores the process
that the current \minizinc\ interpreter uses to translate a \minizinc{} instance
into a solver-level constraint model.
\section{\glsentrytext{minizinc}}%
\label{sec:back-minizinc}
@ -104,7 +104,7 @@ library of constraints allow users to easily model complex problems.
\end{listing}
\begin{example}%
\label{ex:back-mzn-knapsack}
\label{ex:back-mzn-knapsack}
Let us introduce the language by modelling the problem from
\cref{ex:back-knapsack}. A \minizinc\ model encoding this problem is shown in
@ -140,22 +140,22 @@ and primitive constraints.
Given the assignments
\begin{mzn}
TOYS = {football, tennisball, stuffed_elephant};
toy_joy = [63, 12, 100];
toy_space = [32, 8, 40];
space_left = 44;
TOYS = {football, tennisball, stuffed_elephant};
toy_joy = [63, 12, 100];
toy_space = [32, 8, 40];
space_left = 44;
\end{mzn}
the following model is the result of flattening:
\begin{mzn}
var 0..1: selection_0;
var 0..1: selection_1;
var 0..1: selection_2;
var 0..175: total_joy:: is_defined_var;
constraint int_lin_le([32,8,40],[selection_0,selection_1,selection_2],44);
constraint int_lin_eq([63,12,100,-1],[selection_0,selection_1,selection_2,total_joy],0):: defines_var(total_joy);
solve maximize total_joy;
var 0..1: selection_0;
var 0..1: selection_1;
var 0..1: selection_2;
var 0..175: total_joy:: is_defined_var;
constraint int_lin_le([32,8,40],[selection_0,selection_1,selection_2],44);
constraint int_lin_eq([63,12,100,-1],[selection_0,selection_1,selection_2,total_joy],0):: defines_var(total_joy);
solve maximize total_joy;
\end{mzn}
This \emph{flat} problem will be passed to some \solver{}, which will attempt to
@ -279,13 +279,13 @@ expressions capture common (complex) relations between \variables{}.
\Glspl{global} in the \minizinc\ language are used as function calls. An example
of a \gls{global} is
\begin{mzn}
predicate knapsack(
array [int] of int: w,
array [int] of int: p,
array [int] of var int: x,
var int: W,
var int: P,
);
predicate knapsack(
array [int] of int: w,
array [int] of int: p,
array [int] of var int: x,
var int: W,
var int: P,
);
\end{mzn}
This \gls{global} expresses the knapsack relationship, where the \parameters{}
@ -315,7 +315,7 @@ functions that can be used to transform or combine other expressions. For
example the constraint
\begin{mzn}
constraint not (a + b < c);
constraint not (a + b < c);
\end{mzn}
contains the infix \glspl{operator} \mzninline{+} and \mzninline{<}, and the
@ -383,7 +383,7 @@ parts:
\begin{description}
\item[\mzninline{G}] The generator expression which assigns the values of
collections to identifiers,
collections to identifiers,
\item[\mzninline{F}] an optional filtering condition, which has to evaluate to
\mzninline{true} for the iteration to be included in the array,
\item[\mzninline{E}] and the expression that is evaluation for each iteration
@ -415,34 +415,34 @@ resulting definition. There are three main purposes for \glspl{let}:
\item To name an intermediate expression, so it can be used multiple times or
to simplify the expression. For example, the constraint
\begin{mzn}
constraint let { var int: tmp = x div 2; } in tmp mod 2 == 0 \/ tmp = 0;
\end{mzn}
\begin{mzn}
constraint let { var int: tmp = x div 2; } in tmp mod 2 == 0 \/ tmp = 0;
\end{mzn}
constrains that half of \mzninline{x} is even or zero.
constrains that half of \mzninline{x} is even or zero.
\item To introduce a scoped \variable{}. For example, the constraint
\begin{mzn}
let {var -2..2: slack;} in x + slack = y;
\end{mzn}
\begin{mzn}
let {var -2..2: slack;} in x + slack = y;
\end{mzn}
constrains that \mzninline{x} and \mzninline{y} are at most two apart.
constrains that \mzninline{x} and \mzninline{y} are at most two apart.
\item To constrain the resulting expression. For example, the following
function
\begin{mzn}
function var int: int_times(var int: x, var int: y) =
let {
var int: z;
constraint pred_int_times(x, y, z);
} in z;
\end{mzn}
\begin{mzn}
function var int: int_times(var int: x, var int: y) =
let {
var int: z;
constraint pred_int_times(x, y, z);
} in z;
\end{mzn}
returns a new \variable{} \mzninline{z} that is constrained to be the
multiplication of \mzninline{x} and \mzninline{y} by the relational
multiplication constraint \mzninline{pred_int_times}.
returns a new \variable{} \mzninline{z} that is constrained to be the
multiplication of \mzninline{x} and \mzninline{y} by the relational
multiplication constraint \mzninline{pred_int_times}.
\end{enumerate}
An important detail in flattening \glspl{let} is that any \variables{} that
@ -457,14 +457,14 @@ definitions and in the resulting expression.
\subsection{Reification}%
\label{subsec:back-reification}
With the rich expression language in \minizinc{}, \constraints{} can consist
of complex expressions that do not translate to a single constraint at the
\solver{} level. Instead different parts of a complex expression will be
translated into different \constraints{}. Not all of these constraint will
be globally enforced by the solver. \constraints{} stemming for
sub-expressions will typically be \emph{reified} into a Boolean variable.
\Gls{reification} means that a variable \mzninline{b} is constrained to be true
if and only if a corresponding constraint \mzninline{c(...)} holds.
With the rich expression language in \minizinc{}, \constraints{} can consist of
complex expressions that do not translate to a single constraint at the
\solver{} level. Instead, different parts of a complex expression will be
translated into different \constraints{}. Not all of these \constraints{} will be
globally enforced by the solver. \constraints{} stemming for sub-expressions
will typically be \emph{reified} into a Boolean variable. \Gls{reification}
means that a variable \mzninline{b} is constrained to be true if and only if a
corresponding constraint \mzninline{c(...)} holds.
\begin{example}
Consider the \minizinc\ model:
@ -477,9 +477,9 @@ if and only if a corresponding constraint \mzninline{c(...)} holds.
This model maximises the number of even numbers taken by the elements of the
array \mzninline{x}. In this model the expression \mzninline{x[i] mod 2 == 0}
has to reified. Since the elements have a domain from 1 to 15 and are
has to be reified. Since the elements have a domain from 1 to 15 and are
constrained to take different values, not all elements of \mzninline{x} can
take even values. Instead the solver is tasked to maximise the number of
take even values. Instead, the solver is tasked to maximise the number of
reified variables it can set to \mzninline{true}.
\end{example}
@ -509,33 +509,33 @@ Some expressions in the \cmls\ do not always have a well-defined result.
the constraint should be trivially true.
\end{example}
Part of the semantics of a \cmls\ is the choice as to how to treat these partial
Part of the semantics of a \cmls{} is the choice as to how to treat these partial
functions. Examples of such expressions in \minizinc\ are:
\begin{itemize}
\item Division (or modulus) when the divisor is zero:
\begin{mzn}
x div 0 = @??@
\end{mzn}
\begin{mzn}
x div 0 = @??@
\end{mzn}
\item Array access when the index is outside the given index set:
\begin{mzn}
array1d(1..3, [1,2,3])[0] = @??@
\end{mzn}
\begin{mzn}
array1d(1..3, [1,2,3])[0] = @??@
\end{mzn}
\item Finding the minimum or maximum or an empty set:
\begin{mzn}
min({}) = @??@
\end{mzn}
\begin{mzn}
min({}) = @??@
\end{mzn}
\item Computing the square root of a negative value:
\begin{mzn}
sqrt(-1) = @??@
\end{mzn}
\begin{mzn}
sqrt(-1) = @??@
\end{mzn}
\end{itemize}
@ -550,32 +550,32 @@ in \cmls\ \autocite*{frisch-2009-undefinedness}:
\begin{description}
\item[Strict] \cmls\ employing a ``strict'' undefinedness semantic do not
allow any undefined behaviour during the evaluation of the constraint model.
If during the flattening or solving process an expression is found to be
undefined, then any expressions in which it is used is also marked as
undefined. In the end, this means that the occurrence of a single undefined
expression will mark the full model as undefined.
allow any undefined behaviour during the evaluation of the constraint model.
If during the flattening or solving process an expression is found to be
undefined, then any expressions in which it is used is also marked as
undefined. In the end, this means that the occurrence of a single undefined
expression will mark the full model as undefined.
\item[Kleene] The ``Kleene'' semantic treat undefined expressions as
expressions for which not enough information is available. This if an
expression contains undefined sub-expression, it will only be marked as
undefined if the value of the sub-expression is required to compute its
result. Take for example the expression \mzninline{false -> E}. Here, when
\mzninline{E} is undefined the result of the expression can still be said to
be \mzninline{true}, since the value of \mzninline{E} does not influence the
result of the expression. However, if we take the expression \mzninline{true
/\ E}, then when \mzninline{E} is undefined the overall expression is also
undefined since the value of the expression cannot be determined.
expressions for which not enough information is available. This if an
expression contains undefined sub-expression, it will only be marked as
undefined if the value of the sub-expression is required to compute its
result. Take for example the expression \mzninline{false -> E}. Here, when
\mzninline{E} is undefined the result of the expression can still be said to
be \mzninline{true}, since the value of \mzninline{E} does not influence the
result of the expression. However, if we take the expression \mzninline{true
/\ E}, then when \mzninline{E} is undefined the overall expression is also
undefined since the value of the expression cannot be determined.
\item[Relational] The ``relational'' semantic follows from the fact that all
expressions in \cmls\ will eventually become part of a relational
constraint. So even though a (functional) expression in itself might not
have a well-defined result, we can still decide whether its surrounding
relationship holds. For example, the expression \mzninline{x div 0} is
undefined, but the relationship \mzninline{int_div(x,0,y)} can be said to be
\mzninline{false}. It can be said that the relational semantic will make the
closest relational expression that contains an undefined expression
\mzninline{false}.
expressions in \cmls\ will eventually become part of a relational
constraint. So even though a (functional) expression in itself might not
have a well-defined result, we can still decide whether its surrounding
relationship holds. For example, the expression \mzninline{x div 0} is
undefined, but the relationship \mzninline{int_div(x,0,y)} can be said to be
\mzninline{false}. It can be said that the relational semantic will make the
closest relational expression that contains an undefined expression
\mzninline{false}.
\end{description}
@ -593,7 +593,7 @@ For example, one might deal with a zero divisor using a disjunction:
In this case we expect the undefinedness of the division to be contained within
the second part of the disjunction. This corresponds to ``relational''
semantics. \jip{TODO:\@ This also corresponds to Kleene semantics, maybe I
should use a different example}
should use a different example}
Frisch and Stuckey also show that different \solvers{} often employ different
semantics \autocite*{frisch-2009-undefinedness}. It is therefore important that,
@ -606,11 +606,11 @@ model.
\label{sec:back-solving}
There are many prominent techniques to solve a \constraint{} model, but none of
them will solve a \minizinc\ model directly. Instead a \minizinc\ model get
them will solve a \minizinc\ model directly. Instead, a \minizinc\ model get
translated into \variables{} and \constraints{} of the type that the solver
supports directly.
\minizinc\ was initially designed as an input language for \gls{cp} \solvers{}.
\minizinc{} was initially designed as an input language for \gls{cp} \solvers{}.
These \glspl{solver} often support many of the high-level \constraints{} that
are written in a \minizinc\ model. For \gls{cp} solvers the amount of
translation required can vary a lot. It depends on which \constraints{} the
@ -618,7 +618,7 @@ targeted \gls{cp} \solver{} are directly supported and which \constraints{} have
to be decomposed.
Because \gls{cp} \solvers{} work on a similar level as the \minizinc\ language,
some of the techniques used in \gls{cp} \solvers{} can also be used during the
some techniques used in \gls{cp} \solvers{} can also be used during the
transformation from \minizinc\ to \flatzinc{}. The usage of these techniques can
often help shrink the \glspl{domain} of \variables{} and eliminate or simplify
\constraint{}. \Cref{subsec:back-cp} explains the general method employed by
@ -630,7 +630,7 @@ approaches to finding solutions to \constraint{} models. Although these
they also bring new challenges in to efficiently encode the problem for these
\solvers{}. To understand these challenges in the translations a \minizinc\
model into a solver level \constraint{} model, the remainder of this section
will discuss the other dominant technologies used used by \minizinc\ \solver{}
will discuss the other dominant technologies used by \minizinc\ \solver{}
targets and their input language.
\subsection{Constraint Programming}%
@ -643,13 +643,13 @@ every value in the \gls{domain} all \variables{}. It will not surprise the
reader that this is an inefficient approach. Given, for example, the constraint
\begin{mzn}
constraint a + b = 5;
constraint a + b = 5;
\end{mzn}
It is clear that when the value \mzninline{a} is known, then the value of
\mzninline{b} can be deduced. \gls{cp} is the idea solving \glspl{csp} by
performing an intelligent search by inferring which which values are still
feasible for each \variable{} \autocite{rossi-2006-cp}.
performing an intelligent search by inferring which values are still feasible
for each \variable{} \autocite{rossi-2006-cp}.
To find a solution to a given \gls{csp}, a \gls{cp} \solver{} will perform a
depth first search. At each node, the \solver{} will try and eliminate any
@ -678,10 +678,10 @@ only able to prove that the problem is unsatisfiable by exploring the full
search space.
\Gls{propagation} is not only used when starting the search, but also after
making each search decision. This means that some of the \gls{propagation}
depends on the search decision. Therefore, if the \solver{} needs to reconsider
a search decision, then it must also undo all \gls{domain} changes that were
caused by \gls{propagation} dependent on that search decision.
making each search decision. This means that some \gls{propagation} depends on
the search decision. Therefore, if the \solver{} needs to reconsider a search
decision, then it must also undo all \gls{domain} changes that were caused by
\gls{propagation} dependent on that search decision.
The general most common method in \gls{cp} \solvers{} to achieve this is to keep
track of \gls{domain} changes using a \gls{trail}. For every \gls{domain} change
@ -696,78 +696,78 @@ search decision. Furthermore, because propagation is performed to a
\gls{fixpoint}, it is guaranteed that no duplicate propagation is required.
The solving method used by \gls{cp} \solvers{} is very flexible. A \solver{} can
support many different types of \variables{}: they can range from Boolean,
floating point numbers, and integers, to intervals, sets, and functions.
Similarly, \solvers{} do not all have access to the same propagators. Therefore,
a \gls{csp} modelled for one \solver{} might look very different to an
equivalent \gls{csp} modelled for a different solver. Instead, \cmls{}, like
\minizinc{}, can serve as a standardised form of input for these \solvers{}.
They allow modellers to use high-level constraints that are used directly by the
solver when supported or they are automatically translated to a collection of
equivalent supported constraints otherwise.
support many types of \variables{}: they can range from Boolean, floating point
numbers, and integers, to intervals, sets, and functions. Similarly, \solvers{}
do not all have access to the same propagators. Therefore, a \gls{csp} modelled
for one \solver{} might look very different to an equivalent \gls{csp} modelled
for a different solver. Instead, \cmls{}, like \minizinc{}, can serve as a
standardised form of input for these \solvers{}. They allow modellers to use
high-level constraints that are used directly by the solver when supported, or
they are automatically translated to a collection of equivalent supported
constraints otherwise.
\begin{example}%
\label{ex:back-nqueens}
Consider as an example the N-Queens problem. Given a chess board of size
\(n \times n\), find a placement for \(n\) queen chess pieces such that no queen
can attack another. Meaning only one queen per row, one queen per column, and
one queen per diagonal. The problem can be modelled in \minizinc\ as follows.
\label{ex:back-nqueens}
Consider as an example the N-Queens problem. Given a chess board of size
\(n \times n\), find a placement for \(n\) queen chess pieces such that no queen
can attack another. Meaning only one queen per row, one queen per column, and
one queen per diagonal. The problem can be modelled in \minizinc\ as follows.
\begin{mzn}
int: n;
array [1..n] of var 1..n: q;
\begin{mzn}
int: n;
array [1..n] of var 1..n: q;
constraint all_different(q);
constraint all_different([q[i] + i | i in 1..n]);
constraint all_different([q[i] - i | i in 1..n]);
\end{mzn}
constraint all_different(q);
constraint all_different([q[i] + i | i in 1..n]);
constraint all_different([q[i] - i | i in 1..n]);
\end{mzn}
Since we know that there can only be one queen per column, the decision in the
model left to make is, for every queen, where in the column the piece is placed.
The \constraints{} in the model model the remaining rules of the problem: no two
queen can be placed in the same row, no two queen can be place in the same
upward diagonal, and no two queens can be place in the same downward diagonal.
This model can be directly used in most \gls{cp} \solvers{}, since integer
\variables{} and an \mzninline{all_different} \gls{propagator} are common.
Since we know that there can only be one queen per column, the decision in the
model left to make is, for every queen, where in the column the piece is
placed. The \constraints{} in the model the remaining rules of the problem: no
two queen can be placed in the same row, no two queen can be place in the same
upward diagonal, and no two queens can be place in the same downward diagonal.
This model can be directly used in most \gls{cp} \solvers{}, since integer
\variables{} and an \mzninline{all_different} \gls{propagator} are common.
When solving the problem, initially no values can be eliminated from the
\glspl{domain} of the \variables{}. The first propagation will happen when the
first queen is placed on the board. The search space will then look like this:
When solving the problem, initially no values can be eliminated from the
\glspl{domain} of the \variables{}. The first propagation will happen when the
first queen is placed on the board. The search space will then look like this:
\jip{insert image of nqueens board with one queen assigned.}
\jip{Insert image of n-queens board with one queen assigned.}
Now that one queen is placed on the board the propagators for the
\mzninline{all_different} constraints can start propagating. They can eliminate
all values that are on the same row or diagonal as the queen placed on the
board.
Now that one queen is placed on the board the propagators for the
\mzninline{all_different} constraints can start propagating. They can eliminate
all values that are on the same row or diagonal as the queen placed on the
board.
\jip{insert previous image with all impossible moves marked red.}
\jip{Insert previous image with all impossible moves marked red.}
\end{example}
In \gls{cp} solving there is a trade-off between the amount of time spend
propagating a constraint and the the amount of search that is otherwise
required. The golden standard for a \gls{propagator} is to be \gls{domain-con},
meaning that all values left in the \glspl{domain} of its \variables{} there is
at least one possible variable assignment that satisfies the constraint.
Designing an algorithm that reaches this level of consistency is, however, an
easy task and might require high complexity. Instead it can sometimes be better
to use a propagator with a lower level of consistency. Although it might not
eliminate all possible values of the domain, searching the values that are not
eliminated might take less time than achieving \gls{domain-con}.
propagating a constraint and the amount of search that is otherwise required.
The golden standard for a \gls{propagator} is to be \gls{domain-con}, meaning
that all values left in the \glspl{domain} of its \variables{} there is at least
one possible variable assignment that satisfies the constraint. Designing an
algorithm that reaches this level of consistency is, however, an easy task and
might require high complexity. Instead, it can sometimes be better to use a
propagator with a lower level of consistency. Although it might not eliminate
all possible values of the domain, searching the values that are not eliminated
might take less time than achieving \gls{domain-con}.
This is, for example, the case for integer linear constraints:
\[ \sum_{i} c_{i} x_{i} = d\] where \(c_{i}\) and \(d\) are integer
\parameters{} and \(x_{i}\) are integer \variable{}. For these constraints, no
realistic \gls{domain-con} \gls{propagator} exists. Instead \solvers{} generally
use a \gls{bounds-con} \gls{propagator}, which guarantee only that the minimum
and maximum values in the \glspl{domain} of the \variables{} are used in at
least one possible assignment that satisfies the constraint.
realistic \gls{domain-con} \gls{propagator} exists. Instead, \solvers{}
generally use a \gls{bounds-con} \gls{propagator}, which guarantee only that the
minimum and maximum values in the \glspl{domain} of the \variables{} are used in
at least one possible assignment that satisfies the constraint.
Thus far, we have only considered \glspl{csp}. \gls{cp} solving can, however,
also be used to solve optimisation problems using a method called \gls{bnb}. The
\gls{cp} \solver{} will follow the same method as previously described. However,
when it find a solution, it does not yet know if this solution is optimal. It is
when it finds a solution, it does not yet know if this solution is optimal. It is
merely an incumbent solution. The \solver{} must therefore resume its search,
but it is no longer interested in just any solution, only solutions that have a
better \gls{objective} value. This is achieved by adding a new \gls{propagator}
@ -778,7 +778,7 @@ process does not find any other solutions, then it is proven that there are no
better solutions than the current incumbent solution.
\gls{cp} solvers like Chuffed \autocite{chuffed-2021-chuffed}, Choco
\autocite{prudhomme-2016-choco}, Gecode \autocite{gecode-2021-gecode}, and
\autocite{prudhomme-2016-choco}, \gls{gecode} \autocite{gecode-2021-gecode}, and
OR-Tools \autocite{perron-2021-ortools} have long been one of the leading method
to solve \minizinc\ instances.
@ -793,9 +793,9 @@ using a set of linear equations over continuous variables. In general, a linear
program can be expressed in the form:
\begin{align*}
\text{maximise} \hspace{2em} & \sum_{j=1}^{V} c_{j} x_{j} & \\
\text{maximise} \hspace{2em} & \sum_{j=1}^{V} c_{j} x_{j} & \\
\text{subject to} \hspace{2em} & l_{i} \leq \sum_{j=0}^{V} a_{ij} x_{j} \leq u_{i} & \forall_{i=1}^{C} \\
& x_{i} \in \mathbb{R} & \forall_{i=1}^{V}
& x_{i} \in \mathbb{R} & \forall_{i=1}^{V}
\end{align*}
where \(V\) and \(C\) represent the number of variables and number of
@ -817,7 +817,7 @@ The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all}
Unlike \gls{lp}, there is no algorithm that can solve a mixed integer program in
polynomial time. The general method to solve a mixed integer program is to treat
it as an linear program and find an optimal solution using the simplex method.
it as a linear program and find an optimal solution using the simplex method.
If the \variables{} in the problem that are required to be discrete already have
discrete values, then we have found our optimal solution. Otherwise, we pick one
of the \variables{}. For this \variable{} we create a version of the linear
@ -830,7 +830,7 @@ found.
Much of the power of this solving method comes from bounds that can be inferred
during the process. The solution that the simplex provides an upper bound for
the solution in the current step of the solving process. Similarly, any discrete
solution found in an earlier branches of the search process provide a lower
solution found in an earlier branch of the search process provide a lower
bound. When the upper bound given by the simplex method is lower that the lower
bound from an earlier solution, then we know that any discrete solutions
following from the linear program will be strictly worse than the incumbent.
@ -839,7 +839,7 @@ Over the years \gls{lp} and \gls{mip} \solvers{} have developed immensely.
\solvers{}, such as CBC \autocite{forrest-2020-cbc}, CPLEX
\autocite{cplex-2020-cplex}, Gurobi \autocite{gurobi-2021-gurobi}, and SCIP
\autocite{gamrath-2020-scip}, can solve many complex problems. It is therefore
often worthwhile to encode problem as an mixed integer program to find a
often worthwhile to encode problem as a mixed integer program to find a
solution.
\glspl{csp} can be often be encoded as mixed integer programs. This does,
@ -854,17 +854,17 @@ linear \constraints{} using the \variables{} \(y_{i}\).
\begin{example}
Let us again consider the N-Queens problem from \cref{ex:back-nqueens}. The
following model shows a integer program of this problem.
following model shows an integer program of this problem.
\begin{align}
\text{given} \hspace{2em} & N = {1,\ldots,n} & \\
\text{maximise} \hspace{2em} & 0 & \\
\text{subject to} \hspace{2em} & q_{i} \in N & \forall_{i \in N} \\
& y_{ij} \in \{0,1\} & \forall_{i,j \in N} \\
\label{line:back-mip-channel} & x_{i} = \sum_{j \in N} j * y_{ij} & \forall_{i \in N} \\
\label{line:back-mip-row} & \sum_{i \in N} y_{ij} \leq 1 & \forall_{j \in N} \\
\label{line:back-mip-diag1} & \sum_{i,j \in N. i + j =k} y_{ij} \leq 1 & \forall_{k=3}^{2n-1} \\
\label{line:back-mip-diag2} & \sum_{i,j \in N. i - j =k} y_{ij} \leq 1 & \forall_{k=2-n}^{n-2}
\text{given} \hspace{2em} & N = {1,\ldots,n} & \\
\text{maximise} \hspace{2em} & 0 & \\
\text{subject to} \hspace{2em} & q_{i} \in N & \forall_{i \in N} \\
& y_{ij} \in \{0,1\} & \forall_{i,j \in N} \\
\label{line:back-mip-channel} & x_{i} = \sum_{j \in N} j * y_{ij} & \forall_{i \in N} \\
\label{line:back-mip-row} & \sum_{i \in N} y_{ij} \leq 1 & \forall_{j \in N} \\
\label{line:back-mip-diag1} & \sum_{i,j \in N. i + j =k} y_{ij} \leq 1 & \forall_{k=3}^{2n-1} \\
\label{line:back-mip-diag2} & \sum_{i,j \in N. i - j =k} y_{ij} \leq 1 & \forall_{k=2-n}^{n-2}
\end{align}
@ -907,7 +907,7 @@ instances of the problem with thousands of \variables{} and clauses.
Many real world problems modelled in \cmls\ directly correspond to \gls{sat}.
However, even problems that contain \variables{} with types other than Boolean
can often be encoded as a \gls{sat} problem. Depending of the problem, using a
can often be encoded as a \gls{sat} problem. Depending on the problem, using a
\gls{sat} \solvers{} to solve the encoded problem can still be the most
efficient way to solve the problem.
@ -917,13 +917,13 @@ efficient way to solve the problem.
following.
\begin{align}
\text{given} \hspace{2em} & N = {1,\ldots,n} & \\
\text{find} \hspace{2em} & q_{ij} \in \{\text{true}, \text{false}\} & \forall_{i,j \in N} \\
\label{line:back-sat-at-least}\text{subject to} \hspace{2em} & \exists_{j \in N} q_{ij} & \forall_{i \in N} \\
\label{line:back-sat-row}& \neg q_{ij} \lor \neg q_{ik} & \forall_{i,j \in N} \forall_{k=j}^{n}\\
\label{line:back-sat-col}& \neg q_{ij} \lor \neg q_{kj} & \forall_{i,j \in N} \forall_{k=i}^{n}\\
\label{line:back-sat-diag1}& \neg q_{ij} \lor \neg q_{(i+k)(j+k)} & \forall_{i,j \in N} \forall_{k=1}^{min(n-i, n-j)}\\
\label{line:back-sat-diag2}& \neg q_{ij} \lor \neg q_{(i+k)(j-k)} & \forall_{i,j \in N} \forall_{k=1}^{min(n-i, j)}
\text{given} \hspace{2em} & N = {1,\ldots,n} & \\
\text{find} \hspace{2em} & q_{ij} \in \{\text{true}, \text{false}\} & \forall_{i,j \in N} \\
\label{line:back-sat-at-least}\text{subject to} \hspace{2em} & \exists_{j \in N} q_{ij} & \forall_{i \in N} \\
\label{line:back-sat-row} & \neg q_{ij} \lor \neg q_{ik} & \forall_{i,j \in N} \forall_{k=j}^{n} \\
\label{line:back-sat-col} & \neg q_{ij} \lor \neg q_{kj} & \forall_{i,j \in N} \forall_{k=i}^{n} \\
\label{line:back-sat-diag1} & \neg q_{ij} \lor \neg q_{(i+k)(j+k)} & \forall_{i,j \in N} \forall_{k=1}^{\min(n-i, n-j)} \\
\label{line:back-sat-diag2} & \neg q_{ij} \lor \neg q_{(i+k)(j-k)} & \forall_{i,j \in N} \forall_{k=1}^{\min(n-i, j)}
\end{align}
The encoding of the problem uses a Boolean \variable{} for every position of
@ -938,18 +938,18 @@ efficient way to solve the problem.
A variation on \gls{sat} is the \gls{maxsat} problem. Where in a \gls{sat}
problem all clauses need to be satisfied, this is not the case in a \gls{maxsat}
problem. Instead clauses are given individual weights. The higher the weight,
problem. Instead, clauses are given individual weights. The higher the weight,
the more important the clause is for the overall problem. The goal in the
\gls{maxsat} problem is then to find a assignment for Boolean \variables{} that
\gls{maxsat} problem is then to find an assignment for Boolean \variables{} that
maximises the cumulative weights of the satisfied clauses.
The \gls{maxsat} problem is analogous to a \gls{cop}. Like a \gls{cop}, the aim
of \gls{maxsat} is to find the optimal solution to the problem. The difference
is that the weights are given to the \constraints{} instead of the \variables{}
or a function over them. It is, again, often possible to encode a \gls{cop} as a
\gls{maxsat} problem. A naive approach approach to encode an integer objective
is, for example, to encode each value in the domain as a Boolean variable and
assign that same value to a clause containing just that Boolean variable.
\gls{maxsat} problem. A naive approach to encode an integer objective is, for
example, to encode each value in the domain as a Boolean variable and assign
that same value to a clause containing just that Boolean variable.
For many problems the use of \gls{maxsat} \solvers{} can offer a very successful
method to find the optimal solution to a problem.
@ -962,11 +962,11 @@ are many other \cmls{}. Each \cml{} has its own focus and purpose and comes with
its own strength and weaknesses. Most of the techniques that are discusses in
this thesis can be adapted to these languages.
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
We will now discuss some 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
A notable difference between all 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.
@ -1065,7 +1065,7 @@ scheduled.
\begin{example}
For example the \variable{} declarations and \constraints{}
for a jobshop problem would look like this in an \gls{opl} model:
for a job shop problem would look like this in an \gls{opl} model:
\begin{plain}
ScheduleHorizon = sum(j in Jobs, t in Tasks) duration[j, t];
@ -1163,16 +1163,16 @@ cherished for its adoption of high-level \variable{} types. In addition to all
variable types that are contained in \minizinc{}, \gls{essence} also contains:
\begin{itemize}
\item finite sets of non-iteger types,
\item finite multisets of any type,
\item Finite sets of non-integer types,
\item finite multi-sets of any type,
\item finite (partial) functions,
\item and (regular) partitions of finite types.
\end{itemize}
Since sets, multisets, and functions can be defined on any other type, these
Since sets, multi-sets, and functions can be defined on any other type, these
types can be arbitrary nested and the modeller can define, for example, a
\variable{} that is a set of set of integers. Partitions can be defined for
finite types. These types in \gls{essence} are restricted to Booleans,
\variable{} that is a sets of sets of integers. Partitions can be defined for
finite types. These types in \gls{essence} are restricted to Boolean,
enumerated types, or a restricted set of integers.
\begin{example}
@ -1245,7 +1245,7 @@ the targeted solver.
At the heart of the flattening process lies a \gls{trs}. A \gls{trs}
\autocite{baader-1998-term-rewriting} describes a computational model the full
process can be describe as the application of rules
process can be described as the application of rules
\(l \rightarrow r_{1}, \ldots r_{n}\), that replace a \gls{term} \(l\) with one
or more \glspl{term} \(r_{1}, \ldots r_{n}\). A \gls{term} is an expression with
nested sub-expressions consisting of \emph{function} and \emph{constant}
@ -1259,9 +1259,9 @@ sub-expression.
rewrite logical and operations:
\begin{align*}
(r_{1}):\hspace{5pt}& 0 \land x \rightarrow 0 \\
(r_{2}):\hspace{5pt}& 1 \land x \rightarrow x \\
(r_{3}):\hspace{5pt}& x \land y \rightarrow y \land x
(r_{1}):\hspace{5pt} & 0 \land x \rightarrow 0 \\
(r_{2}):\hspace{5pt} & 1 \land x \rightarrow x \\
(r_{3}):\hspace{5pt} & x \land y \rightarrow y \land x
\end{align*}
From these rules it follows that
@ -1306,9 +1306,9 @@ models: \gls{clp} and \gls{chr}.
\glsreset{clp}
\gls{clp} \autocite{marriott-1998-clp} can be seen as a predecessor of \cmls{}
like \minizinc. A constraint logic program describes the process in which a high
like \minizinc{}. A constraint logic program describes the process in which a high
level constraint model is eventually rewritten into a solver level constraints
and added to a \solver{}. Like in \minizinc, can define \constraint{} predicates
and added to a \solver{}. Like in \minizinc{}, can define \constraint{} predicates
to use in the definition of the \constraint{} model. Different from \minizinc{},
constraint predicates in \gls{clp} can be rewritten in multiple ways. The goal
of a constraint logic program is to rewrite all \constraints{} in such a way
@ -1316,11 +1316,11 @@ that the solver level \glspl{constraint} are all satisfied.
Variables are another notable difference between \cmls\ and \gls{clp}. In
\gls{clp}, like in a conventional \gls{trs}, a variable is merely a name. The
symbol might be replace or equated with a constant symbol, but, different from
symbol might be replaced or equated with a constant symbol, but, different from
\cmls{}, this is not a requirement. A variable can remain a name in the solution
of a constraint logic program. This means that the solution of a constraint
logic program can be a relationship between different variables. In cases where
a instantiated solution is required, a special \mzninline{labeling} constraint
an instantiated solution is required, a special \mzninline{labeling} constraint
can be used to force a variable to take a constant value. Similarly, there is a
\mzninline{minimize} that can be used to find the optimal value for a variable.
@ -1332,7 +1332,7 @@ all constraints are rewritten and no inconsistency is detected between the
solver level constraints that are produced. If all the possible ways of
rewriting the program are tried, but all of them prove to be inconsistent, then
the program itself can be said to be unsatisfiable. Even when a correct
rewriting is found, it is possible to continue the process. This ways you can
rewriting is found, it is possible to continue the process. This way you can
find all possible correct ways to rewrite the program.
To implement this mechanism there is a tight integration between the \solver{},
@ -1385,12 +1385,12 @@ apply the rule.
\item The first rules states that if \texttt{X = Y}, then \texttt{X -> Y} is
logically true. This rule removes the term \texttt{X -> Y}. Since the
constraint is said to be logically true, nothing gets added. \texttt{X
= Y} functions as a guard. This \solver{} builtin \constraint{} is
= Y} functions as a guard. This \solver{} built-in \constraint{} is
required for the rewriting rule to apply.
\item The second rule implements the anti-symmetry of logical implications;
the two implications, \texttt{X -> Y} and \texttt{Y -> X}, are
replaced by a \solver{} builtin, \texttt{X = Y}.
replaced by a \solver{} built-in, \texttt{X = Y}.
\item Finally, the transitivity rule introduces a derived constraint. When
it finds constraints \texttt{X -> Y} and \texttt{Y -> Z}, then it adds
@ -1404,21 +1404,21 @@ apply the rule.
\end{example}
The rules in a \gls{chr} system can be categorised into three different
categories: simplification, propagation, simpagation. The first two rules in the
previous example are simplification rules: they replace some constraint atoms by
others. The final rule in the example was a propagation rule: based on the
existence of certain constraints, new constraints can be introduced. Simpagation
rules are a combination of both types of rules in the form:
categories: simplification, propagation, and simpagation. The first two rules in
the previous example are simplification rules: they replace some constraint
atoms by others. The final rule in the example was a propagation rule: based on
the existence of certain constraints, new constraints can be introduced.
Simpagation rules are a combination of both types of rules in the form:
\[ H_{1}, \ldots H_{l} \backslash H_{l+1}, \ldots, H_{n} \texttt{<=>} G_{1}, \ldots{}, G_{m} | B_{1}, \ldots, B_{o} \]
It is possible to rewrite using a simpagation rule when there are terms matching
\(H_{1}, \ldots, H_{n}\) and there are \solver{} built-ins
\(G_{1}, \ldots{}, G_{m}\). When the simpagation rule is applied, the terms
\(H_{l+1}, \ldots, H_{n}\) are replaced by the terms \(B_{1}, \ldots, B_{o}\).
The terms \(H_{1}, \ldots H_{l}\) are kept in the system. Since simpagation
rules incorporate both the elements of simplication and propagation rules, it is
possible to formulate all rules as simpagation rules.
\(H_{1}, \ldots, H_{n}\) and there are \solver{} built-ins \(G_{1}, \ldots{},
G_{m}\). When the simpagation rule is applied, the terms \(H_{l+1}, \ldots,
H_{n}\) are replaced by the terms \(B_{1}, \ldots, B_{o}\). The terms \(H_{1},
\ldots H_{l}\) are kept in the system. Since simpagation rules incorporate both
the elements of simplification and propagation rules, it is possible to
formulate all rules as simpagation rules.
\subsection{ACD Term Rewriting}%
\label{subsec:back-acd}
@ -1525,7 +1525,7 @@ 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
\variable{}, then this calculation cannot be performed during the flattening
process. Instead, a new \variable{} must be created to represent the value of
the sub-expression and it must be constrained to take the value corresponding to
the sub-expression, and it must be constrained to take the value corresponding to
the expression. The creation of this new \variable{} and defining \constraints{}
happens in one of two ways:
@ -1562,7 +1562,7 @@ happens in one of two ways:
\begin{mzn}
function var int: max(var int: x, var int: y) :: promise_total =
let {
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;
@ -1579,14 +1579,14 @@ the utmost importance. A \flatzinc\ containing extra \variables{} and
\constraints{} 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 \crefrange{subsec:back-cse}{subsec:back-delayed-rew}
we will discuss the most important techniques used to improved the flattening
of the flattened model. In \crefrange{subsec:back-cse}{subsec:back-delayed-rew},
we will discuss the most important techniques used to improve the flattening
process.
\subsection{Common Sub-expression Elimination}%
\label{subsec:back-cse}
Because the evaluation of a \minizinc\ expression cannot have any side-effects,
Because the evaluation of a \minizinc{} expression cannot have any side effects,
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
@ -1601,7 +1601,7 @@ discrete optimisation \autocite{marinov-2005-sat-optimisations,
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
the expression \mzninline{abs(x)} occurs twice. There is however no need to
create two separate \variables{} (and defining \constraints{}) to represent
the absolute value of \mzninline{x}. The same \variable{} can be used to
represent the \mzninline{abs(x)} in both sides of the disjunction.
@ -1616,7 +1616,7 @@ following example.
\begin{mzn}
function var float: pythagoras(var float: a, var float: b) =
let {
let {
var float: x = pow(a, 2);
var float: y = pow(b, 2);
} in sqrt(x + y);
@ -1641,7 +1641,7 @@ normal to evaluate \mzninline{x = pow(i, 2)}. However, the expression defining
\mzninline{y}, \mzninline{pow(i, 2)}, will be found in the \gls{cse} table and
replaced by the earlier stored result: \mzninline{y = x}.
\gls{cse} also has an important interaction with the occurence of reified
\gls{cse} also has an important interaction with the occurrence of reified
constraints. \Glspl{reification} of a \constraint{} are often defined in the
library in terms of complicated decompositions into simpler constraints, or
require specialised algorithms in the target solvers. In either case, it can be
@ -1693,14 +1693,14 @@ be proven \mzninline{true} or \mzninline{false}.
This principle also applies during the flattening of a \minizinc\ model. It is
generally a good idea to detect cases where we can directly change the
\gls{domain} of a \variable{}. Sometimes this might mean that the constraint
does not need to be added at all and that constricting the domain is enough.
\gls{domain} of a \variable{}. Sometimes this might mean that the \constraint{}
does not need to be added at all and that constricting the \gls{domain} is enough.
Tight domains can also allow us to avoid the creation of reified constraints
when the truth-value of a reified constraints can be determined from the
when the truth-value of a reified \constraint{} can be determined from the
\glspl{domain} of variables.
\begin{example}%
\label{ex:back-adj-dom}
\label{ex:back-adj-dom}
Consider the following \minizinc\ model:
\begin{mzn}
@ -1716,7 +1716,7 @@ when the truth-value of a reified constraints can be determined from the
If we however consider the first \constraint{}, then we deduce that
\mzninline{a} must always take a value that is 4 or lower. When the compiler
adjust the domain of \mzninline{a} while flattening the first \constraint{},
adjusts the domain of \mzninline{a} while flattening the first \constraint{},
then the second \gls{constraint} can be simplified. The expression
\mzninline{a > 5} is known to be \mzninline{false}, which means that the
constraint can be simplified to \mzninline{true}.
@ -1754,13 +1754,13 @@ operators. For example the evaluation of the linear constraint \mzninline{x +
This \flatzinc\ model is correct, but, at least for pure \gls{cp} solvers, the
existence of the intermediate variables is likely to have a negative impact on
the \solver{}'s performance. These \solvers{} would likely perform better had
they received the equivalent linear constraint
they directly received the equivalent linear \constraint{}:
\begin{mzn}
constraint int_lin_le([1,2,-1], [x,y,z], 0)
constraint int_lin_le([1,2,-1], [x,y,z], 0)
\end{mzn}
directly. Since many solvers support linear constraints, it is often an
Since many solvers support linear constraints, it is often an
additional burden to have intermediate values that have to be given a value in
the solution.
@ -1778,7 +1778,7 @@ aggregated constraint, the compiler will not flatten the expression. The
compiler will instead perform a search of its sub-expression to collect all
other expressions to form an aggregated constraint. The flattening process
continues by flattening this aggregated constraint, which might still contain
unflattened arguments.
non-flat arguments.
\subsection{Delayed Rewriting}%
\label{subsec:back-delayed-rew}
@ -1818,15 +1818,15 @@ not always clear which order of evaluation is best.
The same problem occurs with \glspl{reification} that are produced during
flattening. Other constraints could fix the domain of the reified \variable{}
and make the \gls{reification} unnecessary. Instead the constraint (or its
and make the \gls{reification} unnecessary. Instead, the constraint (or its
negation) can be flattened in root context. This could avoid the use of a big
decomposition or an expensive propagator.
To tackle this problem, the \minizinc\ compiler employs \gls{del-rew}. When a
linear \constraint{} is aggregated or a relational \gls{reification}
\constraint{} is introduced it is not directly flattened. Instead these
\constraint{} is introduced it is not directly flattened. Instead, these
constraints are appended to the end of the current \gls{ast}. All other
constraints currently still unflattened, that could change the relevant
not yet flattened constraints, that could change the relevant
\glspl{domain}, will be flattened first.
Note that this heuristic does not guarantee that \variables{} have their
@ -1837,9 +1837,9 @@ the \glspl{domain} of \variables{} used by other delayed \constraints{}.
\label{subsec:back-fzn-optimisation}
After the compiler is done flattening the \minizinc\ instance, it enters the
optimisation phase. This phase occurs at the same stage as the as the solver
input language. Depending on the targeted \solver{}, the \minizinc\ flattener
might still understand the meaning of certain constraints. In these cases,
optimisation phase. This phase occurs at the same stage as the solver input
language. Depending on the targeted \solver{}, the \minizinc\ flattener might
still understand the meaning of certain constraints. In these cases,
\gls{propagation} methods (as discussed in \cref{subsec:back-cp}) can be used to
eliminate values from variable \glspl{domain} and simplify \constraints{}.

6
latexindent.yaml Normal file
View File

@ -0,0 +1,6 @@
# verbatim environments specified
# in this field will not be changed at all!
verbatimEnvironments:
mzn: 1
nzn: 1
plain: 1