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

Fix typos from examiner feedback

Browse Source
This commit is contained in:
Jip J. Dekker 2021-10-25 10:57:42 +11:00
parent a5c8823b40
commit b22e75b0cf
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
10 changed files with 41 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
assets/glossary.tex
View File

@ -425,7 +425,7 @@
\newglossaryentry{gls-mip}{
name={mixed integer programming (MIP)},
description={
A solving technique that tries to find the \gls{opt-sol} for a \cmodel{} containing a mixture of Integer and floating point \glspl{variable} subject to \glspl{constraint} in the form of linear (in\nobreakdash)equations.
A solving technique that tries to find the \gls{opt-sol} for a \cmodel{} containing a mixture of Integer and floating point \glspl{variable} subject to \glspl{constraint} in the form of linear (in\nobreakdash-)equations.
Mixed integer programming is extensively studied and there are many successful \glspl{solver} dedicated to solving mixed integer programs.
See \cref{subsec:back-mip}.
}

2
assets/listing/back_tsp.mzn
View File

@ -4,4 +4,4 @@ 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]]);
solve minimize sum(i in CITIES) (cost[i, next[i]]);

10
chapters/1_introduction.tex
View File

@ -71,11 +71,11 @@ We design and evaluate an architecture for \cmls{} that can accommodate the mode
Let us now study the different ways of constraint modelling in more detail, starting with one of the most commonly used \cmls{}: \glsxtrshort{ampl}.
\glsxtrshort{ampl} was originally designed as a common interface to different \gls{mip} \solvers{}.
The language provides a natural way to define numeric \variables{} and express \constraints{} in the form of linear (in\nobreakdash)equations as described by the class of problem.
The language provides a natural way to define numeric \variables{} and express \constraints{} in the form of linear (in\nobreakdash-)equations as described by the class of problem.
The same \glsxtrshort{ampl} model can then be used for different \solvers{}.
\glsxtrshort{ampl} was later extended to include other \solver{} targets, including \gls{cp} and quadratic \solvers{}.
As such, additional types of \constraints{} for these problem classes have been added to the language, removing the restriction that \constraints{} must be linear (in\nobreakdash)equations.
As such, additional types of \constraints{} for these problem classes have been added to the language, removing the restriction that \constraints{} must be linear (in\nobreakdash-)equations.
Let us introduce the \glsxtrshort{ampl} language by modelling the ``open shop'' problem.
In the open shop problem, the goal is to schedule jobs with multiple tasks.
@ -105,10 +105,10 @@ As such, \glsxtrshort{ampl} cannot rewrite all models for all its \solvers{}.
For example, since the model in \cref{lst:intro-open-shop} uses the \mzninline{or} \gls{operator} (see lines \ref{line:intro:or:first} and \ref{line:intro:or:second}), it can only be encoded for \solvers{} that support \glsxtrshort{ampl}'s \gls{cp} interface.
Although they do support the \gls{rewriting} of models between different problem classes, other traditional \cmls{}, such as \gls{essence} and \glsxtrshort{opl}, exhibit the same problems.
They do not provide any way to capture common concepts, and, apart from changing the implementation of \glsxtrshort{opl} or \gls{essence}, the \solver{} is unable to influence their preferred encoding.
They do not provide any way to capture common concepts, and, apart from changing the implementation of \glsxtrshort{opl} or \gls{essence}, the \solver{} is unable to influence the encoding of the \instance{}.
\gls{clp}, as used for example in the \gls{sicstus} language, offers a very different mechanism to create a \cmodel{}.
In \gls{clp} the main method to formulate a \cmodel{} and how to search for a solution it through the use of so-called \constraint{} predicates.
In \gls{clp} the main method to formulate a \cmodel{} and to search for a solution is through the use of so-called \constraint{} predicates.
For example, the concepts of one task preceding another and non-overlapping of tasks could be defined in Prolog as follows.
\begin{minted}[
@ -215,7 +215,7 @@ In particular:
\section{Research Aims and Contributions}
Research into \gls{rewriting} of \cmls{}, as well as model transformation in general, has shown that it is difficult to achieve both high performance and generality.
We address these issues by reconsidering the rewriting process from the ground up to make the transformation efficient while accommodating the optimization techniques required to produce high-quality \gls{slv-mod}.
We address these issues by reconsidering the rewriting process from the ground up to make the transformation efficient while accommodating the optimization techniques required to produce high-quality \glspl{slv-mod}.
In order to adapt \cmls{} for modern day requirements, this thesis aims to \textbf{design, implement, and evaluate a modern architecture for functional \cmls{}}.
Crucially, this architecture will allow us to:

26
chapters/2_background.tex
View File

@ -86,7 +86,7 @@ Its expressive language and extensive library of \glspl{global} allow users to e
The model then declares its \variables{}.
\Lref{line:back:knap:sel} declares the main \variable{} \mzninline{selection}, which represents the selection of toys to be packed.
This is \(S\) in our earlier model.
We also declare the \variable{} \mzninline{total_joy}, on \lref{line:back:knap:tj}, which is functionally defined to be the summation of all the joy for the toy picked in our selection.
We also declare the \variable{} \mzninline{total_joy}, on \lref{line:back:knap:tj}, which is functionally defined to be the summation of all the joy for the toys picked in our selection.
The model then contains a \constraint{}, on \lref{line:back:knap:con}, which ensures we do not exceed the given capacity.
Finally, it states the goal for the \solver{}: to maximize the value of the \variable{} \mzninline{total_joy}.
@ -175,7 +175,7 @@ Variable declarations are stated in the form \mzninline{@\(T\)@: @\(I\)@ = @\(E\
\item and the modeller can functionally define the value using an expression \(E\).
\end{itemize}
The syntax \mzninline{= @\(E\)@} is optional.
It is omitted when a \variable{} has is not functionally defined, or when a \parameter{} is a \prbpar{} and assigned externally.
It is omitted when a \variable{} is not functionally defined, or when a \parameter{} is a \prbpar{} and assigned externally.
The identifier used in a top-level variable declaration must be unique.
Two declarations with the same identifier result in an error during the \gls{rewriting} process.
@ -344,14 +344,14 @@ If the expression is a \gls{variable}, then the expression is rewritten to an \g
Otherwise, the \gls{rewriting} replaces the \gls{array} access expression by the chosen element of the \gls{array}.
\paragraph{Comprehensions} \Gls{array} \glspl{comprehension} are expressions which allows modellers to construct \gls{array} objects.
The generation of new \gls{array} structures allows modellers adjust, combine, filter, or order values from within the \minizinc{} model.
The generation of new \gls{array} structures allows modellers to adjust, combine, filter, or order values in the \minizinc{} model.
\Gls{comprehension} expressions \mzninline{[@\(E\)@ | @\(G\)@ where @\(F\)@]} consist of three parts:
\begin{description}
\item[\(G\)] The \gls{generator} expression which assigns the values of collections to identifiers,
\item[\(F\)] an optional filtering condition, which decided whether the iteration to be included in the \gls{array},
\item[\(E\)] and the expression that is evaluated for each iteration when the filtering condition succeeds.
\item[\(G\)] The \gls{generator} expression which assigns the values of collections to identifiers;
\item[\(F\)] an optional filtering condition, which decides whether the iteration is included in the \gls{array}; and
\item[\(E\)] the expression that is evaluated for each iteration when the filtering condition succeeds.
\end{description}
The following example constructs an \gls{array} that contains the tripled even values of an \gls{array} \mzninline{x}.
@ -692,7 +692,7 @@ If the search process finds another \gls{sol}, then the incumbent \gls{sol} is u
If the search process does not find any other \glspl{sol}, then it is proven that a better \gls{sol} than the current incumbent \gls{sol} cannot exist.
It is an \gls{opt-sol}.
\gls{cp} solvers like \gls{chuffed} \autocite{chu-2011-chuffed}, Choco \autocite{prudhomme-2016-choco}, \gls{gecode} \autocite{schulte-2019-gecode}, and OR-Tools \autocite{perron-2021-ortools} have long been one of the leading methods to solve \minizinc\ instances.
\gls{cp} solvers like \gls{chuffed} \autocite{chu-2011-chuffed}, Choco \autocite{prudhomme-2016-choco}, \gls{gecode} \autocite{schulte-2019-gecode}, and OR-Tools \autocite{perron-2021-ortools} have long been among the leading methods to solve \minizinc\ instances.
\subsection{Mathematical Programming}%
\label{subsec:back-mip}
@ -701,7 +701,7 @@ It is an \gls{opt-sol}.
Mathematical programming \solvers{} are the most prominent solving technique employed in \gls{or} \autocite{schrijver-1998-mip}.
At its foundation lies \gls{lp}.
A linear program describes a problem using \constraints{} in the form of linear (in\nobreakdash)equations over continuous \variables{}.
A linear program describes a problem using \constraints{} in the form of linear (in\nobreakdash-)equations over continuous \variables{}.
In general, a linear program can be expressed in the following form.
\begin{align*}
@ -725,7 +725,7 @@ In \gls{lp} our \variables{} must be continuous.
If we require that one or more take an integer value (\(x_{i} \in \mathbb{Z}\)), then the problem becomes \glsxtrshort{np}-hard.
The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all} \variables{} must take an integer value).
Unlike \gls{lp}, there is not an algorithm that solves a mixed integer program in polynomial time.
Unlike \gls{lp}, there is no algorithm that solves a mixed integer program in polynomial time.
We can, however, adapt \gls{lp} solving methods to solve a mixed integer program.
We do this by treating the mixed integer program as a linear program and find an \gls{opt-sol}.
If the \variables{} happen to take integer values in the \gls{sol}, then we have found an \gls{opt-sol} to the mixed integer program.
@ -746,7 +746,7 @@ These \solvers{} are therefore prime targets to solve \minizinc{} \instances{}.
To solve an \instance{} of a \cmodel{}, it can be rewritten into a mixed integer program.
This process is known as \gls{linearization}.
It does, however, come with its challenges.
Many \minizinc{} models contain \constraint{} that are not linear (in\nobreakdash)equations.
Many \minizinc{} models contain \constraint{} that are not linear (in\nobreakdash-)equations.
The translation of a single such \constraint{} can introduce many linear \constraints{} and \glspl{avar}.
For example, when a \constraint{} reasons about the value that a variable takes, the \gls{linearization} process introduces indicator variables.
An indicator variable \(y_{i}\) is a \gls{avar} that for a \variable{} \(x\) take the value 1 if \(x = i\) and 0 otherwise.
@ -907,10 +907,10 @@ Different types of \solvers{} can also have access to different types of \constr
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 the modeller is required to use the language functionality that is compatible with the targeted \solver{}; in this case, all expression have to be linear (in\nobreakdash)equations.
In the \gls{ampl} language this means that the modeller is required to use the language functionality that is compatible with the targeted \solver{}; in this case, all expression have to be linear (in\nobreakdash-)equations.
In \minizinc{} the modeller is not constrained in the same way.
It can use the viewpoint of choosing, from each city, to which city to go next.
They can use the viewpoint of choosing, from each city, to which city to go next.
A \mzninline{circuit} \gls{global} is then used to enforce that these decisions form a single path over all cities.
When targeting a \gls{mip} \solver{}, the \gls{decomp} of the \mzninline{circuit} \constraint{} will use a similar method to Miller--Tucker--Zemlin.
@ -1050,7 +1050,7 @@ Since sets, multi-sets, and functions can be defined on any other type, these ty
Notably, the \texttt{together} function tests whether two elements are in the same part of a partition.
A \minizinc{} model for the same problem can be found in \cref{lst:back-mzn-sgp}.
It starts similarly to the \gls{essence} model, with the declaration of the \parameters{} and a type for the golfers.
It starts similarly to the \gls{essence} model, with the declarations of the \parameters{} and a type for the golfers.
The differences start from the declaration of the \variables{}.
The \minizinc{} model is unable to use a set of partitions and instead uses an \gls{array} of sets.
Each set represents a single group in a single week.

10
chapters/3_rewriting.tex
View File

@ -8,7 +8,7 @@
\section{Architecture Overview}
\label{sec:rew-arch}
\noindent{}\Gls{rewriting} a \minizinc{} instance into \gls{slv-mod} may often seem like a simple \gls{trs}.
\noindent{}\Gls{rewriting} a \minizinc{} instance into a \gls{slv-mod} may often seem like a simple \gls{trs}.
In reality, however, \minizinc{} is quite a complex language, and producing a good \gls{slv-mod} is far from trivial.
Thus, in practice, this rewriting process is a highly complex task that needs to carefully track interactions between \constraints{} and how they affect \variables{}.
@ -51,7 +51,7 @@ We have developed a prototype of this toolchain, and present experimental valida
This section introduces the two sub-languages of \minizinc{} at the core of the new architecture we have developed.
\microzinc{} is a simple language used to define transformations to be performed by the \interpreter{}.
It is simplified subset of \minizinc{}.
It is a simplified subset of \minizinc{}.
The transformation are represented in the language through the use of function definitions.
A function of type \mzninline{var bool}, describing a relation, can be defined as a \gls{native} \constraint{}.
Otherwise, a function body must be provided for \gls{rewriting}.
@ -69,12 +69,12 @@ Furthermore, \nanozinc{} allows for \constraints{} to be ``attached'' to a \vari
As a small syntactic difference with \flatzinc{}, \constraints{} and \variable{} declarations in \nanozinc{} can be freely interleaved.
The core of the syntax of \microzinc{} is defined in \cref{fig:rew-uzn-syntax}.
In \microzinc{} it is specifically used to mark functions that are \gls{native} to the target \solver{}.
Function declarations without an expression body are used to mark functions that are \gls{native} to the target \solver{}.
We have omitted the definitions of \syntax{<mzn-type-inst>} and \syntax{<ident>}, which can be assumed to be the same as the definition of \syntax{<type-inst>} and \syntax{<ident>} in the \minizinc{} grammar, see \cref{ch:minizinc-grammar}.
While we omit the typing rules here for space reasons, we will assume that in well-typed \microzinc{} programs conditions of expressions are \parameters{}.
This means that the where conditions \syntax{<exp>} in \glspl{comprehension}, the conditions \syntax{<exp>} in \gls{conditional} expressions, and the \syntax{<literal>} index in \gls{array} accesses must have \mzninline{par} type.
In \minizinc{} the use of \variables{} in these positions is allowed, and these expressions are rewritten to function calls.
We will discuss how the same transformation takes place in when translating \minizinc{} to \microzinc{}.
We will discuss how the same transformation takes place when translating \minizinc{} to \microzinc{}.
\begin{figure}
\begin{grammar}
@ -471,7 +471,7 @@ Our prototype implementation of the \microzinc{}/\nanozinc{} framework consists
The \gls{compiler} translates \minizinc{} into a \gls{byte-code} encoding of \microzinc{}.
The compiler currently supports a significant subset of the full \minizinc{} language.
The missing features, such floating point values and complex output statements, require additional engineering effort, but do not require new technology.
The missing features, such as floating point values and complex output statements, require additional engineering effort, but do not require new technology.
The \gls{interpreter} evaluates \microzinc{} \gls{byte-code} and \nanozinc{} programs based on the \gls{rewriting} system introduced in this section.
It can read \parameters{} from a file or via an \glsxtrshort{api}.

18
chapters/4_half_reif.tex
View File

@ -62,7 +62,7 @@ This is, however, not an issue since in this case the value can just be assigned
\end{mzn}
However, independent of the value of \mzninline{b1}, if \mzninline{b2} takes the value \true{}, then it can never make the disjunction \false{}.
Therefore, \gls{propagation} of the disjunction can never force \mzninline{b2} to take the value \false{}.
Therefore, \gls{propagation} of the disjunction can never force \mzninline{b1} to take the value \false{}.
Consequently, this means using \gls{half-reif} is \gls{eqsat}.
\Gls{rewriting} using \gls{half-reif} will result in the following model.
@ -93,7 +93,7 @@ Since Boolean expressions in \minizinc{} can be used in, for example, integer ex
To systematically analyse whether Boolean expressions can be \gls{half-reified}, we study the monotonicity of \constraints{} w.r.t.\@ an expression.
A relation \( r(\ldots{}, a, \ldots{}) \) is said to be \gls{monotone} w.r.t.\@ its argument \(a\) when given two possible values for \(a\), \(x\) and \(y\), if \(x \geq{} y\) and all other arguments to \(r\) remain the same, then \(r(\ldots{}, x, \ldots{}) \geq{} r(\ldots{}, y, \ldots{})\).
The relation is said to be \gls{antitone} w.r.t.\@ its argument \(a\) if given two possible values for \(a\), \(x\) and \(y\), if \(x \geq{} y\) and all other arguments to \(r\) remain the same, then \(r(\ldots{}, x, \ldots{}) \leq{} r(\ldots{}, y, \ldots{}) \).
Where, for clarification, we assume \( \false{} < \true{} \).
For clarification, here we assume that \( \false{} < \true{} \).
Using these definitions, we introduce additional distinctions in the context of expressions.
Before, we would merely distinguish between \rootc{} context and non-\rootc{} context.
@ -105,7 +105,7 @@ Now, we will categorize the latter into the following three contexts.
\item[\negc{}] An expression is in \negc{} context when the enclosing \constraint{} (in \rootc{} context) is \textbf{antitone} w.r.t.\@ the expression.
\item[\mixc{}] An expression is in \mixc{} context when the enclosing \constraint{} (in \rootc{} context) is \textbf{neither} monotone, nor antitone w.r.t.\@ the expression.
\item[\mixc{}] An expression is in \mixc{} context when the enclosing \constraint{} (in \rootc{} context) is \textbf{neither} monotone nor antitone w.r.t.\@ the expression.
\end{description}
@ -149,7 +149,7 @@ Only full \gls{reif} can be used for expressions that are in this context.
\end{mzn}
This \constraint{} forces either \mzninline{x} or \mzninline{y}, but not both, to take the value five.
The equalities in this constraint are in \mixc{} context, because whether \mzninline{y} can and must take the value 5 now directly depends on if \mzninline{x} has already taken the value five, and vice versa.
The equalities in this constraint are in \mixc{} context, because whether \mzninline{y} can and must take the value 5 now directly depends on whether \mzninline{x} has already taken the value five, and vice versa.
As such, when \mzninline{x} takes the value five it forces \mzninline{y} to not take the value five.
This means we cannot use a \gls{half-reif}, since it does not enforce the negated \constraint{}.
\end{example}
@ -285,7 +285,7 @@ It is, however, not as straightforward to construct its full \gls{reif}.
In addition to the \gls{half-reified} \gls{cnf}, a generic \gls{reif} would require the implication \(\neg \texttt{b} \implies \neg c\).
Based on the \gls{cnf} of \(c\), this would result in the following logical formula.
\[ \neg b \implies \neg c = \forall_{i} b \lor \neg \exists_{j} lit_{ij} \]
This formula, however, is not direct set of clauses.
This formula, however, is not a direct set of clauses.
Rewriting this formula would result in the following \gls{cnf}.
\[ \neg b \implies \neg c = \forall_{i,j} b \lor lit_{ij} \]
It adds a new binary clause for every literal in the original \gls{cnf}.
@ -337,7 +337,7 @@ The partiality context is the context in which this condition is placed.
\end{mzn}
In this fragment, we study the context of the division expression \mzninline{y div x}.
The expression itself return an integer \variable{}, and it used on the left-hand side of a less than \constraint{}.
The expression itself return an integer \variable{}, and it is used on the left-hand side of a less than \constraint{}.
This result is therefore in a \negc{} context: it is only forced to take a smaller value.
This is its value context.
@ -441,7 +441,7 @@ These functions track and combine the contexts in which a value is used in an im
Most changes in the context of \microzinc{} expressions stem from the (Call) rule.
A call expression can change the context in which its arguments should be evaluated.
As an input to the inference process, a ``argCtx'' function is used to give the context of the arguments of a function, given the function itself and the context of the call.
As an input to the inference process, an ``argCtx'' function is used to give the context of the arguments of a function, given the function itself and the context of the call.
A definition for this function for the \minizinc{} \glspl{operator} can be found in \cref{alg:arg-ctx}.\footnote{We use \minizinc{} \gls{operator} syntax instead of \microzinc{} identifiers for brevity and clarity.}
Although a standard definition for the ``argCtx'' function may cover the most common cases, it does not cover user-defined functions.
@ -512,7 +512,7 @@ Otherwise, the \compiler{} follows the following steps to try to introduce the m
\item If \(ctx\) is \posc{} or \negc{}, then change \(ctx\) to \mixc{} and return to step 1.
\item Finally, if none of the earlier steps were successful, then the compilation fails.
Note that this can only occur when there is not a definition for the \gls{reif} of a \constraint{}, i.e., neither a \gls{native} constraint nor a \gls{decomp}.
Note that this can only occur when there is no definition for the \gls{reif} of a \constraint{}, i.e., neither a \gls{native} constraint nor a \gls{decomp}.
\end{enumerate}
The (Access) and (ITE) rules show the context inference for \gls{array} access and \gls{conditional} expressions respectively.
@ -1031,7 +1031,7 @@ These adjustments happen similar to the adjustments of the general algorithm: ex
In our second configuration the \mzninline{all_different} \constraint{} is enforced using the \gls{decomp} shown in \cref{lst:half-alldiff}.
The \mzninline{!=} \constraints{} produced by this redefinition are \gls{reified}.
Their conjunction then represent the \gls{reif} of the \mzninline{all_different} \constraint{}.
Their conjunction then represents the \gls{reif} of the \mzninline{all_different} \constraint{}.
\begin{listing}
\mznfile{assets/listing/half_alldiff.mzn}

2
chapters/4_half_reif_preamble.tex
View File

@ -2,7 +2,7 @@
\minizinc{} allows us to write complex \constraints{} that in the process of \gls{rewriting} result in multiple \constraints{} that reason about each other.
However, using a \gls{reif} \(b \leftrightarrow{} c\), that determines whether a \constraint{} \(c\) holds, can slow the \solver{} down.
Even in \gls{cp} \solvers{}, few \glspl{reif} are \gls{native} to the \solvers{}, and the \glspl{propagator}, for the ones that are, are often weak.
Generally, the \glspl{decomp} of \gls{reified} \constraint{} also result in numerous \gls{native} \constraints{} and \variables{}.
Generally, the \glspl{decomp} of \gls{reified} \constraints{} also result in numerous \gls{native} \constraints{} and \variables{}.
It is thus important that \gls{rewriting} avoids the use of \gls{reif}, whenever it is not required.
In this chapter we present an extended \gls{reif} analysis to help minimize the required \solver{} effort.

6
chapters/5_incremental.tex
View File

@ -217,7 +217,7 @@ However, it can lead to slightly unexpected behaviour when using \parameter{} fu
\paragraph{Parametric neighbourhood selection predicates}
Since there are many well-known ways to makes a selection of a set of \glspl{neighbourhood}, we define standard \gls{neighbourhood} selection strategies as predicates that are parametric over the \glspl{neighbourhood} they should apply.
Since there are many well-known ways to make a selection of a set of \glspl{neighbourhood}, we define standard \gls{neighbourhood} selection strategies as predicates that are parametric over the \glspl{neighbourhood} they should apply.
For example, we can define a strategy \mzninline{basic_lns} that applies a \gls{lns} \gls{neighbourhood}.
Since \mzninline{on_restart} now also includes the initial search, we apply the \gls{neighbourhood} only if the current status is not \mzninline{START}.
However, we again face the problem that in \minizinc{} we cannot pass functions or predicates as arguments.
@ -273,7 +273,7 @@ For adaptive \gls{lns}, a simple strategy is to change the size of the \gls{neig
The \gls{meta-optimization} algorithms we have seen so far rely on the default behaviour of \minizinc{} \solvers{} to use \gls{bnb} for optimization: when a new \gls{sol} is found, the \solver{} adds a \constraint{} to the remainder of the search to only accept better \glspl{sol}, as defined by the \gls{objective} in the \mzninline{minimize} or \mzninline{maximize} clause of the \mzninline{solve} item.
When combined with \glspl{restart} and \gls{lns}, this is equivalent to a simple hill-climbing search method.
We can use the constructs introduced above to implement alternative search method such as simulated annealing.
We can use the constructs introduced above to implement alternative search method, such as simulated annealing.
We use the \mzninline{restart_without_objective} \gls{annotation}, in particular, to tell the solver not to add the \gls{bnb} \constraint{} on \gls{restart}.
It will still use the declared \gls{objective} to decide whether a new \gls{sol} is globally the best one seen so far, and only output those.
This maintains the convention of \minizinc{} \solvers{} that the last \gls{sol} printed at any point in time is the currently best known one.
@ -371,7 +371,7 @@ This essentially \textbf{turns the new functions into \gls{native} \constraints{
The \gls{neighbourhood} predicate can then be added as a \constraint{} to the \gls{slv-mod}.
The evaluation is performed by hijacking the solver's own capabilities: It will perform the evaluation of the new functions by propagating the \gls{native} \constraints{}.
To compile a \gls{meta-optimization} algorithms to a \gls{slv-mod}, the \gls{rewriting} process performs the following four simple steps.
To compile a \gls{meta-optimization} algorithm to a \gls{slv-mod}, the \gls{rewriting} process performs the following four simple steps.
\begin{enumerate}
\item It replaces the \gls{annotation} \mzninline{::on_restart("X")} with a call to predicate \mzninline{X}.

4
chapters/5_incremental_preamble.tex
View File

@ -1,6 +1,6 @@
\noindent{}In previous chapters, we explored \gls{rewriting} as a definitive linear process, where an \instance{} of a \cmodel{} is translated into a \gls{slv-mod}, for which a \solver{} produces \glspl{sol}.
However, to solve large-scale real-world problems, we often need to use \gls{meta-optimization} algorithms that solve very similar problems multiple times.
While improvements of the \gls{rewriting} process, such as the ones discussed in previous chapters, can increase the performance of these approaches, the overhead of completely\gls{rewriting} an almost identical \instance{} time and again may still prove prohibitive.
While improvements of the \gls{rewriting} process, such as the ones discussed in previous chapters, can increase the performance of these approaches, the overhead of completely \gls{rewriting} an almost identical \instance{} time and again may still prove prohibitive.
\Gls{meta-optimization} warrants direct support from the \cml{} architecture.
In this chapter, we introduce the following two methods to provide this support.
@ -20,4 +20,4 @@ We first introduce examples of \gls{meta-optimization} algorithms and how they c
In \Cref{sec:inc-solver-extension}, we introduce the method to rewrite these \gls{meta-optimization} definitions into efficient \glspl{slv-mod} and the minimal extension required from the target \gls{solver}.
Then, \Cref{sec:inc-incremental-compilation} introduces the alternative method.
It extends the architecture presented in the previous chapters with an incremental \constraint{} modelling interface.
Finally, \Cref{sec:inc-experiments} reports on the experimental results of both approaches.
Finally, \Cref{sec:inc-experiments} reports on the experimental results of both approaches.

2
chapters/6_conclusions.tex
View File

@ -3,7 +3,7 @@
%************************************************
\noindent{}\Gls{rewriting} in \cmls{}, such as \minizinc{}, makes it easier to express \glspl{dec-prb}.
They allow the modeller to reason at a high-level when specifying the problem.
They allow the modeller to reason at a high level when specifying the problem.
\Gls{rewriting} is then able to create a model for a range of potential \solvers{}.
Although the importance of creating \glspl{slv-mod} that can be solved efficiently is well-known, changes in the usage of these languages are raising questions about the time required to perform this transformation.
First, \constraint{} models are now often solved using low-level \solvers{}, such as \gls{mip} and \gls{sat}.