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

Fix all concrete feedback from Andreas

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-07 17:10:25 +10:00
parent a139905a20
commit b7d0a3e3a3
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
6 changed files with 34 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
assets/mzn/back_knapsack.mzn
View File

@ -2,14 +2,14 @@
enum TOYS;@\Vlabel{line:back:knap:toys}@
array[TOYS] of int: toy_joy;@\Vlabel{line:back:knap:joy}@
array[TOYS] of int: toy_space;@\Vlabel{line:back:knap:space}@
int: space_left;@\Vlabel{line:back:knap:left}@
int: total_space;@\Vlabel{line:back:knap:left}@
% Decision variables
var set of TOYS: selection;@\Vlabel{line:back:knap:sel}@
var int: total_joy = sum(toy in selection)(toy_joy[toy]);@\Vlabel{line:back:knap:tj}@
% Constraints
constraint sum(toy in selection)(toy_space[toy]) < space_left;@\Vlabel{line:back:knap:con}@
constraint sum(toy in selection)(toy_space[toy]) < total_space;@\Vlabel{line:back:knap:con}@
% Goal
solve maximize total_joy;@\Vlabel{line:back:knap:obj}@

6
assets/packages.tex
View File

@ -2,7 +2,7 @@
\emergencystretch=1em
\usepackage{fvextra}
\usepackage{csquotes}
\usepackage[australian]{babel}
\usepackage[english]{babel}
\usepackage{hyperref}
\hypersetup{bookmarksnumbered}
\usepackage{xspace}
@ -85,8 +85,8 @@
}
\newcommand{\Vlabel}[1]{\label[line]{#1}\hypertarget{#1}{}}
\newcommand{\lref}[1]{\hyperlink{#1}{\FancyVerbLineautorefname~\ref*{#1}}}
\newcommand{\Lref}[1]{\hyperlink{#1}{\FancyVerbLineautorefname~\ref*{#1}}}
\newcommand{\lref}[1]{\FancyVerbLineautorefname~\hyperlink{#1}{\ref*{#1}}}
\newcommand{\Lref}[1]{\titlecap{\FancyVerbLineautorefname}~\hyperlink{#1}{\ref*{#1}}}
\newcommand{\lrefrange}[2]{\FancyVerbLineautorefname{}s~\hyperlink{#1}{\ref*{#1}}--\hyperlink{#2}{\ref*{#2}}}
\newcommand{\Lrefrange}[2]{Lines~\hyperlink{#1}{\ref*{#1}}--\hyperlink{#2}{\ref*{#2}}}

41
chapters/2_background.tex
View File

@ -4,6 +4,8 @@
\input{chapters/2_background_preamble}
\glsresetall{}
\section{Introduction to Constraint Modelling Languages}
\label{sec:back-intro}
@ -13,22 +15,24 @@ For example, an assembly language allows you to abstract from the machine instru
And, early imperative programming languages, like FORTRAN, were the first to offer abstraction from the processor architecture of the targeted system.
Consequently, in current times, writing a computer program requires little knowledge of how the targeted computer system operates.
Freuder states that the ``Holy Grail'' of programming languages would be where the user merely states the problem, and the computer solves it and that constraint modelling is one of the biggest steps towards this goal to this day \autocite*{freuder-1997-holygrail}.
In \cmls{}, different from imperative (and even other declarative) languages, the modeller does not describe how to solve the problem, but rather provides the problem requirements; therefore, it could be said that a \cmodel{} actually describes the \gls{sol} to the problem.
\Citeauthor{freuder-1997-holygrail} states that the ``Holy Grail'' of programming languages would be where the user merely states the problem, and the computer solves it and that constraint modelling is one of the biggest steps towards this goal to this day \autocite*{freuder-1997-holygrail}.
\Cmls{} operate different from other computer languages.
The modeller does not describe how to solve a problem, but rather formalises the requirements of the problem.
It could be said that a \cmodel{} actually describes the answer to the problem.
In a \cmodel{}, instead of specifying the manner in which we can find the \gls{sol}, we give a concise description of the problem.
The elements of a \cmodel include \parameters{}, what we already know; \variables{}, what we wish to know; and \constraints{}, the relationships that should exist between them.
Through the variation of \parameters{}, a \cmodel{} can describe a full class of problems.
A specific problem is captured by a \instance{}, the combination of a \cmodel{} with a complete \gls{parameter-assignment} (\ie{}, a mapping from all parameters to values).
The type of combinatorial problems described by \cmodels{} are called \gls{dec-prb}.
The type of problem described by a \cmodel{} is called a \gls{dec-prb}.
The goal of a \gls{dec-prb} is to find a \gls{sol}: an complete \gls{variable-assignment} that satisfy the \constraints{}.
Or, when this is not possible, prove that no such \gls{assignment} exists.
Many \cmls{} also support the modelling of \gls{opt-prb}, where a \gls{dec-prb} is augmented with an \gls{objective}.
In this case the goal is to find a \gls{sol} that satisfies all \constraints{} while minimising (or maximising) the value of the \gls{objective}.
Although a \cmodel{} does not contain any instructions on how to find a suitable \gls{sol}, \instances{} of \cmodels{} can generally be given to a dedicated \solver{}.
The \solver{} will use a dedicated algorithm that finds a \gls{sol} that fits the requirements of the \instance{}.
The \solver{} uses a dedicated algorithm that finds a \gls{sol} that fits the requirements of the \instance{}.
\begin{example}%
\label{ex:back-knapsack}
@ -43,7 +47,7 @@ The \solver{} will use a dedicated algorithm that finds a \gls{sol} that fits th
\begin{cases}
S \subseteq T \\
z = \sum_{i \in S} joy(i) \\
\sum_{i \in S} space(i) < C \\
\sum_{i \in S} space(i) \leq{} C \\
\end{cases}
\end{equation*}
@ -72,11 +76,6 @@ The \solver{} will use a dedicated algorithm that finds a \gls{sol} that fits th
\minizinc{} is a high-level, solver- and data-independent modelling language for discrete satisfiability and optimisation problems \autocite{nethercote-2007-minizinc}.
Its expressive language and extensive library of \glspl{global} allow users to easily model complex problems.
\begin{listing}
\mznfile{assets/mzn/back_knapsack.mzn}
\caption{\label{lst:back-mzn-knapsack} A \minizinc\ model describing a 0-1 knapsack problem}
\end{listing}
\begin{example}%
\label{ex:back-mzn-knapsack}
@ -98,6 +97,11 @@ Its expressive language and extensive library of \glspl{global} allow users to e
Finally, it states the goal for the \solver{}: to maximise the value of the \variable{} \mzninline{total_joy}.
\end{example}
\begin{listing}
\mznfile{assets/mzn/back_knapsack.mzn}
\caption{\label{lst:back-mzn-knapsack} A \minizinc\ model describing a 0-1 knapsack problem}
\end{listing}
One might note that, although more textual and explicit, the \minizinc\ model definition is very similar to our earlier mathematical definition.
A \minizinc{} model cannot be solved solved directly.
@ -106,7 +110,7 @@ Type of \variables{} and \constraints{} are said to be \gls{native} to the \solv
Given complete \gls{parameter-assignment}, a \minizinc{} model can form a \minizinc{} instance.
The process to transform a \minizinc{} instance into a \gls{slv-mod} is a called \gls{rewriting}.
This \gls{slv-mod} created by \minizinc{} are generally in the form of \flatzinc{}.
\Glspl{slv-mod} for \minizinc{} \solvers{} are generally represented in \flatzinc{}.
\flatzinc{} can be seen as a strict subset of \minizinc{} specifically chosen to represent \glspl{slv-mod}.
It is the primary way in which \minizinc{} communicates with \solvers{}.
@ -130,16 +134,16 @@ It is the primary way in which \minizinc{} communicates with \solvers{}.
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
[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{}.
The \solver{} will attempt to determine an \gls{assignment} to each \variable{} \mzninline{solection_i} and \mzninline{total_joy} that satisfies all constraints and maximises \mzninline{total_joy}.
If this is not possible, then it will report that there is no such \gls{assignment}.
This \gls{slv-mod} is then passed to a \solver{}.
The \solver{} attempts to determine a complete \gls{variable-assignment}, \mzninline{selection_@\(i\)@} and \mzninline{total_joy}, that satisfies all constraints and maximises \mzninline{total_joy}.
If there is no such \gls{assignment}, then it reports that the \gls{slv-mod} is \gls{unsat}.
\end{example}
@ -159,7 +163,8 @@ These items are not constrained to occur in any particular order.
We will briefly discuss the most important model items.
Note that these items will already refer to \minizinc{} expressions, which will be discussed in \cref{subsec:back-mzn-expr}.
For a detailed overview of the structure of \minizinc{} models the full syntactic structure of \minizinc{} 2.5.5 can be consulted in \cref{ch:minizinc-grammar}.
Nethercote et al.\ and Marriott et al.\ offer a detailed discussion of the \minizinc{} and \zinc{} language, its predecessor, respectively \autocite*{nethercote-2007-minizinc,marriott-2008-zinc}.
\Citeauthor{nethercote-2007-minizinc} offer a detailed discussion of the \minizinc{} \autocite*{nethercote-2007-minizinc}.
And, much of its history can be learned by the description of its predecessor, \zinc{} \autocite{marriott-2008-zinc}.
\paragraph{Declaration Items} Values in \minizinc{} are declared in the form \mzninline{@\(T\)@: @\(I\)@ = @\(E\)@}, where:
\begin{itemize}

4
chapters/4_half_reif.tex
View File

@ -57,7 +57,7 @@ The complex expressions language used in \cmls{}, such as \minizinc{}, often req
If the Boolean expression \mzninline{pred(...)} is seen in a non-root context, then a new Boolean \variable{} \mzninline{b} is introduced to replace the expression, its \emph{control} \variable{}.
The flattener then enforces a \constraint{} \mzninline{pred_reif(...,b)}, which binds the \variable{} to be the \emph{truth-value} of the expression (\ie\ \mzninline{b <-> pred(...)}).
Feydy et al.\ show that although the usage of \gls{reification} in the flattening process is well-understood, it suffers from certain weaknesses:
\citeauthor{feydy-2011-half-reif} show that although the usage of \gls{reification} in the flattening process is well-understood, it suffers from certain weaknesses:
\begin{enumerate}
\item Many \glspl{reification} are created in the rewriting of partial expressions to accommodate \minizinc{}'s relational semantics.
@ -826,7 +826,7 @@ The control \variable is thus used to communicate any change in context.
We now present experimental evaluation of the presented \gls{half-reif} techniques.
First, to show the benefit of implementing propagators for half-reified constraint, we compare their performance against their decompositions.
To do this, we recreate two experiments presented by Feydy et al.\ in the original \gls{half-reif} paper in a modern \gls{cp} solver, \gls{chuffed}.
To do this, we recreate two experiments presented by \citeauthor{feydy-2011-half-reif} in the original \gls{half-reif} paper in a modern \gls{cp} solver, \gls{chuffed}.
In the experiment, we use propagators implemented according to the principles described in this paper.
No new algorithm has been devised to perform the propagation.
The propagator of the original constraint is merely adjusted to influence and watch a control \variable{}.

4
chapters/4_half_reif_preamble.tex
View File

@ -1,4 +1,4 @@
\noindent{}Feydy et al.\ introduced the notion of \gls{half-reif} as an improvement over the use of \gls{reification} \autocite*{feydy-2011-half-reif}.
\noindent{}\citeauthor{feydy-2011-half-reif} introduced the notion of \gls{half-reif} as an improvement over the use of \gls{reification} \autocite*{feydy-2011-half-reif}.
They show that some of the problems and expenses of the use of \gls{reification} can be mitigated using this technique.
In addition, the creation of propagators for \glspl{half-reif} of constraints can often be an easy process.
It is not always possible, however, to use a \gls{half-reif} instead of a \gls{reification}.
@ -8,7 +8,7 @@ The chosen subset omits let-expressions, which can complicate the process.
An identifier for the same expression can suddenly occur in multiple locations.
This chapter re-evaluates the usage of \gls{half-reif} and provides the first full implementation of a flattener for \minizinc{} with support for \gls{half-reif}.
In \cref{sec:half-intro,sec:half-propagation} we introduce the core concepts of \gls{half-reif} and propagators for half-reified \constraints{}, as discussed by Feydy et al.
In \cref{sec:half-intro,sec:half-propagation} we introduce the core concepts of \gls{half-reif} and propagators for half-reified \constraints{}, as discussed by \citeauthor{feydy-2011-half-reif}.
An additional benefit of \gls{half-reif} is that its decomposition can be significantly smaller than the decomposition of a \gls{reification}.
\Cref{sec:half-decomposition} shows the benefits of \gls{half-reif} when writing decompositions for \gls{mip} and \gls{sat} \solvers{}.
In \cref{sec:half-context} we introduce our new context analysis algorithm: a way to determine where \gls{half-reif} can be used in \microzinc{}, and by extend \minizinc{}.

4
chapters/A2_benchmark.tex
View File

@ -265,7 +265,7 @@ The incremental experiments presented in \cref{sec:inc-experiments} are based on
\end{multicols}
\paragraph{Prize Collecting Path} This problem was introduced in by Feydy et al.\ in the original paper on \gls{half-reif} \autocite*{feydy-2011-half-reif}.
\paragraph{Prize Collecting Path} This problem was introduced in by \citeauthor{feydy-2011-half-reif} in the original paper on \gls{half-reif} \autocite*{feydy-2011-half-reif}.
In this thesis it is used to benchmark the implementation of a propagator for the \gls{half-reif} of the \mzninline{element} constraint.
This experiment is shown in \cref{sec:half-experiments}.
\Cref{lst:bench-prize} shows a \minizinc{} model that can be used to solve the problem.
@ -280,7 +280,7 @@ The data and original model are available at:
\caption{\label{lst:bench-prize} A \minizinc{} model for the Prize Collecting Path problem}
\end{listing}
\paragraph{QCP-Max} This problem was introduced in by Feydy et al.\ in the original paper on \gls{half-reif} \autocite*{feydy-2011-half-reif}.
\paragraph{QCP-Max} This problem was introduced in by \citeauthor{feydy-2011-half-reif} in the original paper on \gls{half-reif} \autocite*{feydy-2011-half-reif}.
In this thesis it is used to benchmark the implementation of a propagator for the \gls{half-reif} of the \mzninline{all_different} constraint.
This experiment is shown in \cref{sec:half-experiments}.
\Cref{lst:bench-qcpmax} shows a \minizinc{} model that can be used to solve the problem.