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

Does it ever end?

Browse Source
This commit is contained in:
Jip J. Dekker 2021-05-11 15:31:51 +10:00
parent aae2191bf0
commit 1c4b9b4eb1
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
7 changed files with 185 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
assets/acronyms.tex
View File

@ -1,6 +1,9 @@
\newacronym[see={[Glossary:]{gls-ampl}}]{ampl}{AMPL\glsadd{gls-cbls}}{A
Mathematical Programming Language}
\newacronym[see={[Glossary:]{gls-ast}}]{ast}{AST\glsadd{gls-ast}}{Abstract
Syntax Tree}
\newacronym[see={[Glossary:]{gls-cbls}}]{cbls}{CBLS\glsadd{gls-cbls}}{Constraint-Based
Local Search}

9
assets/glossary.tex
View File

@ -19,6 +19,11 @@
description={},
}
\newglossaryentry{gls-ast}{
name={Abstract Syntax Tree},
description={},
}
\newglossaryentry{annotation}{
name={annotation},
description={},
@ -144,8 +149,8 @@
description={},
}
\newglossaryentry{linear-programming}{
name={linear programming},
\newglossaryentry{linear-program}{
name={linear program},
description={},
}

BIN
assets/img/back_compilation_structure.pdf Normal file
View File

Binary file not shown.

10
assets/packages.tex
View File

@ -181,6 +181,7 @@ outputdir=build,
fontsize=\scriptsize,
]{minizinc}}{\end{minted}}
% TODO: Fix the nanozinc sytax highlighting/formatting
\newcommand{\nzninline}[1]{\mintinline[fontsize=\small,escapeinside=@@]{minizinc}{#1}}
\newenvironment{nzn}{\VerbatimEnvironment{}\begin{minted}[
@ -191,3 +192,12 @@ outputdir=build,
escapeinside=@@,
fontsize=\scriptsize,
]{minizinc}}{\end{minted}}
\newenvironment{plain}{\VerbatimEnvironment{}\begin{minted}[
autogobble=true,
breaklines,
breakindent=4em,
numbers=none,
escapeinside=@@,
fontsize=\scriptsize,
]{text}}{\end{minted}}

192
chapters/2_background.tex
View File

@ -370,7 +370,8 @@ referenced by expression.
\Gls{array} \glspl{comprehension} are expressions can be used to compose
\gls{array} objects. This allows modellers to create \glspl{array} that are not
given directly as input to the model or are a declared collection of \glspl{variable}.
given directly as input to the model or are a declared collection of
\glspl{variable}.
\Gls{generator} expressions, \mzninline{[E | G where F]}, consist of three
parts:
@ -384,8 +385,8 @@ parts:
when the filtering condition succeeds.
\end{description}
The following example composes an \gls{array} that contains the doubled even values of
an \gls{array} \mzninline{x}.
The following example composes an \gls{array} that contains the doubled even
values of an \gls{array} \mzninline{x}.
\begin{mzn}
[ xi * 2 | xi in x where x mod 2 == 0]
@ -394,7 +395,7 @@ an \gls{array} \mzninline{x}.
The evaluated expression will be added to the new array. This means that the
type of the array will primarily depend on the type of the expression. However,
in recent versions of \minizinc\ both the collections over which we iterate and
the filtering condition could have a \gls{variable} type. Since we then cannot
the filtering condition could have a \gls{variable} type. Since we then cannot
decide during flattening if an element is present in the array, the elements
will be made of a \gls{optional} type. This means that the solver still will
decide if the element is present in the array or if it takes a special
@ -407,7 +408,7 @@ resulting definition. There are three main purposes for \glspl{let}:
\begin{enumerate}
\item To name an intermediate expression, so it can be used multiple times or
to simplify the expression. For example, the constraint
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;
@ -423,7 +424,8 @@ resulting definition. There are three main purposes for \glspl{let}:
constrains that \mzninline{x} and \mzninline{y} are at most two apart.
\item To constrain the resulting expression. For example, the following function
\item To constrain the resulting expression. For example, the following
function
\begin{mzn}
function var int: int_times(var int: x, var int: y) =
@ -531,41 +533,81 @@ undefined expression gets replaced by an equivalent model that is still valid
under a strict semantic. Essentially eliminating the existence of undefined
expressions in the \gls{solver} model.
\section{The Current \glsentrytext{minizinc} Interpreter}%
\section{Compiling \glsentrytext{minizinc}}%
\label{sec:back-mzn-interpreter}
For version 2.5.5 of the \minizinc\ bundle, the \texttt{minizinc} executable is
officially provided tool to solve \minizinc\ instances. A modeller provides the
\texttt{minizinc} executable with a \minizinc\ model, the ground data required
to instantiate the model, and a \gls{solver} definition. Primarily the
\gls{solver} definition defines the \minizinc\ library used to flatten the
\minizinc\ instance and the way in which the \gls{solver} is to be executed. The
process of the \texttt{minizinc} executable can be categorised into the
following stages:
Traditionally the compilation process is split into three sequential parts: the
\emph{frontend}, the \emph{middle-end}, and the \emph{backend}. It is the job of
the frontend to parse the user input, report on any errors or inconsistencies in
the input, and transform it into an internal representation. The middle-end
performs the main translation in a target-independent fashion. It converts the
internal representation at the level of the compiler frontend to another
internal representation as close to the level required by the compilation
targets. The final transformation to the format required by the compilation
target are performed by the backend. When a compiler is separated into these few
steps, then adding support for new language or compilation target only require
the addition of a frontend or backend respectively.
\begin{description}
\item[Parsing] \texttt{minizinc} parses the input data, the \minizinc\ model,
and the \gls{solver} library.
\item[Type checking] \texttt{minizinc} ensures the type consistency of the
\minizinc\ model, making sure that the types of all expressions match their
declarations and is allowed in the locations where they are used. \\ In the
process of type checking the model, all identifiers and calls are connected to
the declaration that they refer to.
\item[Flattening] \jip{TODO:\@ This should have something}
\item[Optimisation] Given the generated \flatzinc{} model, \texttt{minizinc}
will try optimise this model to try and reduce the number of
\glspl{constraint} and size of the \glspl{domain} of \glspl{variable} in the
\flatzinc\ model.
\item[Solving] The optimised \flatzinc\ model is given to the \gls{solver}.
Any solutions found by the \gls{solver} are communicated back to the user.
\end{description}
\begin{figure}[ht]
\centering
\includegraphics[width=\linewidth]{assets/img/back_compilation_structure}
\caption{\label{fig:back-mzn-comp} The compilation structure of the \minizinc\
compiler.}
\end{figure}
\jip{TODO:\@ Description of the flattening process}
The \minizinc\ compilation process categorised in the same three categories, as
shown in \cref{fig:back-mzn-comp}. In the frontend, a \minizinc\ model is first
parsed together with its data into an \gls{ast}. The process will then analyse
the \gls{ast} to discover the types of all expressions used in the instance. If
an inconsistency is discovered, then an error is reported to the user. Finally,
the frontend will also preprocess the \gls{ast}. This process is used to rewrite
expressions into a common form for the middle-end, \eg\ remove the ``syntactic''
sugar. For instance, replacing the usage of enumerated types by normal integers.
\jip{TODO:\@ Description of the techniques used during the optimisation phase}
The middle-end contains the most important two processes: the flattening and the
optimisation. During the flattening process the high-level (\minizinc{})
constraint model is rewritten into a solver level (\flatzinc{}) constraint
model. It could be noted that the flattening step depends on the compilation
target to define its solver level constraints. Even though the information
required for this step is target dependent, we consider it part of the
middle-end as the mechanism is the same for all compilation targets. A full
description of this process will follow in \cref{subsec:back-flattening}. Once a
solver level constraint model is constructed, the \minizinc\ compiler will try
to optimise this model: shrink domains of variables, remove constraints that are
proven to hold, and remove variables that have become unused. These optimisation
techniques are discussed in \cref{subsec:back-fzn-optimisation}.
\subsection{Propagation}%
\label{sub:back-propagation}
The backend will convert the internal solver level constraint model into a
format that can be used by the targeted \gls{solver}. Given the formatted
artefact, a solver process, controlled by the backend, can then be started.
Whenever the solver process produces a solution, the backend will reconstruct
the solution to the specification of the original \minizinc{} model.
\subsection{Flattening}%
\label{subsec:back-flattening}
The goal of the flattening process is to arrive at a ``flat'' constraint model:
it only contains constraints that consist of a singular call instruction, all
arguments to calls are \gls{parameter} literals or \gls{variable} identifiers,
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
\paragraph{Delayed Rewriting}
\paragraph{Reification}
\paragraph{Common Sub-expression Elimination}
\paragraph{Constraint Aggregation}
\subsection{Optimisation}%
\label{subsec:back-fzn-optimisation}
\section{Other Constraint Modelling Languages}%
\label{sec:back-other-languages}
@ -582,6 +624,61 @@ to fit other languages.
\subsection{AMPL}%
\label{sub:back-ampl}
One of the most used \cmls\ is \gls{ampl} \autocite{fourer-2003-ampl}. As the
name suggest, \gls{ampl} was designed to allow modellers to express problems
through the use of mathematical equations. It is therefore also described as an
``algebraic modelling language''. Specifically an \gls{ampl} model generally
describes a \gls{linear-program}. In a \gls{linear-program} the \glspl{variable}
can take any value from a continuous range and the \gls{objective} and
\glspl{constraint} can only use linear function over \glspl{variable} (\ie\
\(\sum c_{i} x_{i}\), where all \(c_{i}\) are \glspl{parameter} and all
\(x_{i}\) are \glspl{variable}).
Depending on the \gls{solver} targeted by \gls{ampl}, the language can give the
modeller access to additional functionality. For \glspl{solver} that have a
\gls{mip} solving method, the modellers can require \glspl{variable} to be
integers. Different types of \glspl{solver} can also have access to different
types of constraints, such as quadratic and non-linear constraints. \gls{ampl}
has even been extended to allow the usage of certain \glspl{global} when using a
\gls{cp} \gls{solver} \autocite{fourer-2002-amplcp}.
\begin{example}
The following
\begin{plain}
set Cities ordered;
set Paths := {i in Cities, j in Cities: ord(i) < ord(j)};
param cost {Paths} >= 0;
var Take {Paths} binary;
param n := card {Cities};
set SubSets := 0 .. (2**n - 1);
set PowerSet {k in SubSets} := {i in Cities: (k div 2**(ord(i)-1)) mod 2 = 1};
minimize TotalCost: sum {(i,j) in Paths} cost[i,j] * Take[i,j];
subj to Tour {i in S}:
sum {(i,j) in Paths} Take[i,j] + sum {(j,i) in Paths} Take[j,i] = 2;
subj to SubtourElimation {k in SubSet diff {0,2**n-1}}:
sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (i,j) in Paths} X[i,j] +
sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (j,i) in Paths} X[j,i] >= 2;
\end{plain}
\begin{mzn}
enum CITIES;
array[CITIES, CITIES] of int: cost;
array[CITIES] of var CITIES: next;
constraint circuit(next);
solve minimize sum(i in CITIES) (cost[i, next[CITIES]]);
\end{mzn}
\end{example}
\subsection{OPL}%
\label{sub:back-opl}
@ -598,7 +695,7 @@ 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:
\begin{minted}[autogobble=true]{text}
\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;
@ -617,7 +714,7 @@ for a jobshop problem would look like this in an \gls{opl} model:
forall (t in Tasks)
task[j, t] requires tool[resource[j, t]];
};
\end{minted}
\end{plain}
The equivalent declarations and \glspl{constraint} would look like this in
\minizinc{}:
@ -665,11 +762,11 @@ modeller more control over the search in comparison to the
modellers to select predefined \glspl{search-heuristic} already implemented in
the solver. Take, for example, the following \gls{opl} search definition:
\begin{minted}[autogobble=true]{text}
\begin{plain}
search {
try x < y | y >= x endtry;
}
\end{minted}
\end{plain}
This search strategy will ensure that we first try and find a solution where the
\gls{variable} \mzninline{x} takes a value smaller than \mzninline{y}, if it
@ -712,7 +809,7 @@ enumerated types, or a restricted set of integers.
For example, the Social Golfers Problem, can be modelled in \gls{essence} as
follows:
\begin{minted}[autogobble=true]{text}
\begin{plain}
language Essence 1.3
given w, g, s : int(1..)
@ -726,7 +823,7 @@ such that
forAll g1, g2 : Golfers, g1 < g2 .
(sum week in sched . toInt(together({g1, g2}, week))) <= 1
\end{minted}
\end{plain}
In \minizinc{} the same problem could be modelled as:
@ -773,7 +870,7 @@ compatible with the targeted solver.
\section{Term Rewriting}%
\label{sec:back-term}
At the heart of the flattening process lies a \glsaccesslong{trs}. A \gls{trs}
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 \(l \rightarrow r\), that
replace a \gls{term} \(l\) with another \gls{term} \(r\). A \gls{term} is an
@ -785,9 +882,9 @@ captures a term sub-expression. For example, the following \gls{trs} consists of
some (well-known) rules to handle logical and:
\begin{align*}
(r_{1}):& 0 \land x \rightarrow 0 \\
(r_{2}):& 1 \land x \rightarrow x \\
(r_{3}):& 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
@ -812,10 +909,11 @@ any \(0\), then the result will be \(0\); otherwise, the result will be \(1\).
\subsection{Constraint Handling Rules}%
\label{sub:back-chr}
\gls{chr} are a special kind of \glspl{trs} designed to work on constraint models.
\subsection{Constraint Logic Programming}%
\label{subsec:back-clp}
\subsection{ACD Term Rewriting}%
\label{subsec:back-acd}
\section{Constraint Logic Programming}%
\label{sec:back-clp}

19
chapters/A2_benchmark.tex Normal file
View File

@ -0,0 +1,19 @@
%************************************************
\chapter{Experiment Resources}%
\label{ch:benchmarks}
%************************************************
All experiments included in this thesis were conducted on a dedicated node in a
computation cluster. The machine operates using a \textbf{Intel Xeon 8260}
\gls{cpu}, which has 24 non-hyperthreaded cores, and has access to
\textbf{268.55 GB} of \gls{ram}. Each experimental test was given exclusive
access to a single \gls{cpu} core and access to sufficient \gls{ram}.
\section{Software}%
\label{sec:bench-soft}
\section{MiniZinc Models}%
\label{sec:bench-models}
\section{Other Programs}%
\label{sec:bench-programs}

1
dekker_thesis.tex
View File

@ -106,6 +106,7 @@ following publication:
\appendix{}
\include{chapters/A1_minizinc_grammar}
\include{chapters/A2_benchmark}
\backmatter{}
\printbibliography{}