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

Before dinner editing

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-29 19:00:31 +10:00
parent 8f94781ac1
commit 4f614b1a6c
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
12 changed files with 110 additions and 105 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
abstract_gp.txt
View File

@ -1,5 +1,5 @@
Real world problems, such as scheduling and routing problems, are often solved by creating high-level models.
These high-level models are automatically rewritten to input suitable for dedicated solver programs.
These high-level models are rewritten to input suitable for dedicated solver programs.
This thesis proposes an architecture for the rewriting process that makes it significantly more efficient and its results easier to solve.
It also supports solving more challenging real world problems that require solving a sequence of related high-level models.
This defines a new state of the art for model rewriting.

39
assets/glossary.tex
View File

@ -7,7 +7,7 @@
}
\newglossaryentry{gls-ampl}{
name={AMPL:\ A Mathematical Programming Language},
name={A Mathematical Programming Language (AMPL)},
description={AMPL is a \gls{cml} originally designed to serve as a common input language for mathematical \glspl{solver} (e.g., \gls{lp} and \gls{mip}). It has later been extended for other types of \glspl{solver}. See \cref{sub:back-ampl}.},
}
@ -68,7 +68,7 @@
\newglossaryentry{bnb}{
name={branch and bound},
description={A search method to find a \gls{opt-sol}. After an initial \gls{sol} is found, the search continuously looks for \glspl{sol} for which the \gls{objective} will return a better value than the incumbent \gls{sol}. If it is such a \gls{sol} cannot exist, then the final incumbent \gls{sol} is a \gls{opt-sol}.},
description={A search method to find a \gls{opt-sol}. After an initial \gls{sol} is found, the search continuously looks for \glspl{sol} for which the \gls{objective} will return a better value than the incumbent \gls{sol}. If it finds that such a \gls{sol} cannot exist, then the final incumbent \gls{sol} is a \gls{opt-sol}.},
}
\newglossaryentry{byte-code}{
@ -93,7 +93,7 @@
\newglossaryentry{boundsz-con}{
name={bounds($\mathbb{Z}$) consistent},
description={A \gls{propagator} is bounds($\mathbb{Z}$) consistent when it tightens the \gls{bounds} such that they can satisfy the \gls{constraint}.},
description={A \gls{propagator} is bounds($\mathbb{Z}$) consistent when it tightens the integer \gls{bounds} such that they can satisfy the \gls{constraint}.},
}
\newglossaryentry{gls-cbc}{
@ -127,7 +127,7 @@
}
\newglossaryentry{gls-cnf}{
name={conjunctive normal form},
name={conjunctive normal form (CNF)},
description={The formulation of a Boolean formula as a conjunction of disjunctions of Boolean literals. This is a standardized format for \gls{gls-sat} problems.},
}
@ -172,7 +172,7 @@
\newglossaryentry{gls-cse}{
name={common sub-expression elimination},
description={A technique stemming from programming language to avoid duplicate computation. In \glspl{cml} this technique is used to avoid the creation of duplicate \glspl{variable} and \glspl{constraint}. See \cref{subsec:back-cse}.},
description={A technique stemming from programming languages to avoid duplicate computation. In \glspl{cml} this technique is used to avoid the creation of duplicate \glspl{variable} and \glspl{constraint}. See \cref{subsec:back-cse}.},
}
\newglossaryentry{confluence}{
@ -223,12 +223,12 @@
\newglossaryentry{del-rew}{
name={delayed rewriting},
description={A technique using during \gls{rewriting}. It delays the \gls{rewriting} of \glspl{constraint} whose \gls{decomp} can change based on information that can become available later during the process.},
description={A technique used during \gls{rewriting}. It delays the \gls{rewriting} of \glspl{constraint} whose \gls{decomp} can change based on information that can become available later during the process.},
}
\newglossaryentry{domain}{
name={domain},
description={A set of value that a \gls{variable} can take without violating any \glspl{constraint} in the problem.},
description={A set of values that a \gls{variable} can take without violating any \glspl{constraint} in the problem.},
}
\newglossaryentry{domain-con}{
@ -297,16 +297,16 @@
description={See \gls{half-reif}.},
}
\newglossaryentry{implication-chain}{
name={implication chain},
description={Multiple implication \glspl{constraint} linked together through a \gls{variable} on opposite sides of the implication, such as \mzninline{A -> B} and \mzninline{B -> C}. If the linking \gls{variable} is not used elsewhere in the \gls{model}, then the \glspl{constraint} can be simplified through the use of \gls{chain-compression}.},
}
\newglossaryentry{incremental-rewriting}{
name={incremental rewriting},
description={The \gls{rewriting} of an \gls{instance} that is continuously changed.},
description={The (repeated) \gls{rewriting} of an \gls{instance} that is continuously changed.},
}
\newglossaryentry{implication-chain}{
name={implication chain},
description={Multiple implication \glspl{constraint} linked together through a \glspl{variable} on opposite sides of the implication, such as \mzninline{A -> B} and \mzninline{B -> C}. When a linking \gls{variable} is not used, the \glspl{constraint} can be simplified through the use of \gls{chain-compression}.},
}
\newglossaryentry{int-sol}{
name={intermediate solution},
@ -409,7 +409,7 @@
\newglossaryentry{gls-mip}{
name={mixed integer programming},
description={
A solving technique 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-)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-)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}.
}
@ -417,7 +417,7 @@
\newglossaryentry{native}{
name={native},
description={\glspl{constraint} and \gls{variable} types are said to be native to a \gls{solver} when they can be directly used as input for the \gls{solver}.},
description={\Glspl{constraint} and \gls{variable} types are said to be native to a \gls{solver} when they can be directly used as input for the \gls{solver}.},
}
\newglossaryentry{nanozinc}{
@ -437,7 +437,7 @@
\newglossaryentry{obj-cp}{
name={Objective-CP},
description={A library for the Objective-C programming language to provide constraint modelling functionality\autocite{hentenryck-2013-objcp}.},
description={A library for the Objective-C programming language to provide constraint modelling functionality \autocite{hentenryck-2013-objcp}.},
}
\newglossaryentry{openwbo}{
@ -451,8 +451,8 @@
}
\newglossaryentry{gls-opl}{
name={OPL:\ The optimization modelling language},
description={A \gls{cml} aimed at combining the powers of mathematical programming and \gls{cp}. The OPL is excels at the modelling of scheduling problems. See \cref{sub:back-opl}.},
name={optimization modelling language (OPL)},
description={A \gls{cml} aimed at combining the powers of mathematical programming and \gls{cp}. OPL excels at the modelling of scheduling problems. See \cref{sub:back-opl}.},
}
\newglossaryentry{opt-prb}{
@ -472,7 +472,7 @@
\newglossaryentry{opt-sol}{
name={optimal solution},
description={A \gls{sol} in an \gls{opt-prb} for which it has been proven that other \gls{sol} of higher quality do not exist.},
description={A \gls{sol} in an \gls{opt-prb} for which it has been proven that other \gls{sol} of higher quality, assessed using an \gls{objective}, do not exist.},
}
\newglossaryentry{restart}{
@ -611,7 +611,6 @@
name={rewriting},
description={
The process of transforming a \gls{model} \gls{instance} into an \gls{eqsat} \gls{slv-mod} is referred to as rewriting.
This happens primarily through the application of \glspl{decomp}.
}
}
@ -689,5 +688,5 @@
\newglossaryentry{zinc}{
name={Zinc},
description={The predecessor of \gls{minizinc}. In comparison to \gls{minizinc}, Zinc contained more features such as pattern matching and tuples, but was not \gls{solver}-independent.},
description={The predecessor of \gls{minizinc} \autocite{marriott-2008-zinc}. In comparison to \gls{minizinc}, Zinc contained more features such as pattern matching and tuples, but was not \gls{solver}-independent.},
}

6
assets/listing/inc_hill_climb.mzn Normal file
View File

@ -0,0 +1,6 @@
predicate hill_climbing() =
if status() != START then
_objective < sol(_objective);
elseif status() = UNSAT then
complete();
endif;

2
assets/listing/inc_pareto.mzn
View File

@ -9,7 +9,7 @@ predicate pareto_optimal(var int: obj1, var int: obj2) =
nsol = 0
elseif status() = UNSAT then
complete() % we are finished!
elsif status() = SAT then
elseif status() = SAT then
nsol = sol(nsol) + 1 /\
s1[nsol] = sol(obj1) /\
s2[nsol] = sol(obj2)

8
chapters/1_introduction.tex
View File

@ -100,9 +100,9 @@ Finally, \lrefrange{line:intro:con:start}{line:intro:con:end} express the \const
The \glsxtrshort{ampl} model provides a clear definition of the problem class, but it can be argued that its meaning is hard to decipher.
\glsxtrshort{ampl} does not provide any way to capture common concepts, such as one task preceding another or that two tasks cannot overlap in our example.
Moreover, the process to encode an \instance{} into a \gls{slv-mod} all happens ``behind the scenes''.
The \solver{} cannot specify how, for example, an operator is best rewritten.
The \solver{} cannot specify how, for example, an \gls{operator} is best rewritten.
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} 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.
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.
@ -158,7 +158,7 @@ For example, a modeller could create the following \minizinc{} function to expre
All functionality in the \minizinc{} language is eventually expressed using function calls.
The \solver{}, then, has the decision to choose if this call is a \gls{native} \constraint{}, or how this call is rewritten.
Each \solver{} supplies its own library of \minizinc{} function definitions for common \constraints{}.
For example, the logical \mzninline{or}-operator, which was only supported for \gls{cp} \solvers{} in \glsxtrshort{ampl}, could be defined in the \minizinc{} library for a \gls{mip} \solver{} using the following definition.
For example, the logical \mzninline{or}-\gls{operator}, which was only supported for \gls{cp} \solvers{} in \glsxtrshort{ampl}, could be defined in the \minizinc{} library for a \gls{mip} \solver{} using the following definition.
\begin{mzn}
predicate bool_or(var bool: x, var bool: y) =
@ -245,7 +245,7 @@ Overall, this thesis makes the following contributions.
This model includes a novel method of tracking of \constraints{} created as part of functional dependencies, ensuring the correct removal of unnecessary \constraints{}.
\item It presents an analysis technique to reason about in what (\gls{reified}) form a \constraint{} should be considered.
This analysis allows for the design and implementation of techniques to automatically introduce \gls{half-reified} \constraints{} in \minizinc{}, including a technique to simplify \glspl{slv-mod} by efficiently eliminating \glspl{implication-chain}.
This analysis allows for the design and implementation of techniques that introduce \gls{half-reified} \constraints{} in \minizinc{}, including a technique to simplify \glspl{slv-mod} by efficiently eliminating \glspl{implication-chain}.
\item It proposes two novel methods to reduce the overhead of using \cmls{} in incremental techniques: \gls{rbmo} and the \gls{incremental-rewriting} of changing \instances{} through an incremental interface.

8
chapters/2_background.tex
View File

@ -599,7 +599,7 @@ A \solver{} can support many types of \variables{}: they can range from Boolean,
Similarly, \solvers{} do not all have implementations for the same \glspl{propagator}.
Therefore, a \gls{slv-mod} for one \solver{} looks very different from an \gls{eqsat} \gls{slv-mod} for a different \solver{}.
\Cmls{}, like \minizinc{}, serve as a standardized form of input for these \solvers{}.
They allow modellers to always use \glspl{global} and depending on the \solver{} they are either used directly, or they are automatically rewritten using a \gls{decomp}.
They allow modellers to always use \glspl{global} and depending on the \solver{} they are either used directly, or they are rewritten using a \gls{decomp}.
\begin{example}%
\label{ex:back-nqueens}
@ -620,7 +620,7 @@ They allow modellers to always use \glspl{global} and depending on the \solver{}
\end{mzn}
The \variables{} in the \gls{array} \mzninline{q} decide for each column in which row the queen is placed.
This automatically restricts every column to only have a single queen.
This restricts every column to only have a single queen.
As such, the queen will not be able to attack vertically.
The \constraints{} model the remaining rules of the problem: two queens cannot be placed in the same row, two queens cannot be placed in the same upward diagonal, and two queens cannot be placed in the same downward diagonal.
For many \gls{cp} \solvers{} this model is close to a \gls{slv-mod}, since integer \variables{} and an \mzninline{all_different} \gls{propagator} are common.
@ -1337,7 +1337,7 @@ The creation of this \gls{avar} and defining \constraints{} happens in one of tw
constraint b \/ i1
\end{mzn}
\noindent{}Rewriting then continues with the \mzninline{this_call_reif} function (if its declaration has a body), as well as the disjunction operator.
\noindent{}Rewriting then continues with the \mzninline{this_call_reif} function (if its declaration has a body), as well as the disjunction \gls{operator}.
\item For non-Boolean expressions, the \gls{avar} and defining \constraints{} are introduced in the definition of the function itself.
For example, the \mzninline{max} function in the standard library, which calculates the maximum of two values, is defined as follows.
@ -1513,7 +1513,7 @@ It is therefore important that equalities are found early in the \gls{rewriting}
\label{subsec:back-aggregation}
Complex \minizinc{} expressions sometimes result in the creation of many \glspl{avar} to represent intermediate results.
This is in particular \true{} for linear and Boolean equations that are generally written using \minizinc{} operators.
This is in particular \true{} for linear and Boolean equations that are generally written using \minizinc{} \glspl{operator}.
\begin{example}%
\label{ex:back-agg}

2
chapters/3_rewriting.tex
View File

@ -133,7 +133,7 @@ The translation from \minizinc{} to \microzinc{} involves the following steps.
\begin{enumerate}
\item Transform all expressions that are valid in \minizinc{} but not in \microzinc{}.
This includes simple cases such as replacing operator expressions, like \mzninline{x+y}, by function calls, \mzninline{int_plus(x,y)}, and replacing generators in calls, like \mzninline{sum(x in A)(x)}, by \glspl{comprehension}, \mzninline{sum([x|x in A])}.
This includes simple cases such as replacing \gls{operator} expressions, like \mzninline{x+y}, by function calls, \mzninline{int_plus(x,y)}, and replacing generators in calls, like \mzninline{sum(x in A)(x)}, by \glspl{comprehension}, \mzninline{sum([x|x in A])}.
As mentioned above, \gls{conditional} expressions where the decision is made by a \variable{} are also not directly supported in \microzinc{}.
These expressions are therefore also replaced by function calls that are possibly decomposed.
An expression \mzninline{if x then A else B endif}, where \mzninline{x} is a \variable{}, is replaced the following call.

22
chapters/4_half_reif.tex
View File

@ -443,7 +443,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.
A definition for this function for the \minizinc{} operators can be found in \cref{alg:arg-ctx}.\footnote{We use \minizinc\ operator syntax instead of \microzinc{} identifiers for brevity and clarity.}
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.
To address this issue, we introduce the \glspl{annotation} \mzninline{promise_ctx_monotone} and \mzninline{promise_ctx_antitone} to represent the operations \changepos{} and \changeneg{} respectively.
@ -454,8 +454,8 @@ However, we currently do not provide such analysis and annotate functions by han
\begin{example}
Consider the user-defined \minizinc{} implementation of a logical implication in \cref{lst:half-impli}.
The \glspl{annotation} placed on the argument of the \mzninline{impli} function will apply the same context transformations as the \mzninline{->} operator shown in \cref{alg:arg-ctx}.
In terms of context analysis, this function now is equivalent to the \minizinc{} operator.
The \glspl{annotation} placed on the argument of the \mzninline{impli} function will apply the same context transformations as the \mzninline{->} \gls{operator} shown in \cref{alg:arg-ctx}.
In terms of context analysis, this function now is equivalent to the \minizinc{} \gls{operator}.
\end{example}
\begin{listing}
\mznfile{assets/listing/half_impli.mzn}
@ -463,7 +463,7 @@ However, we currently do not provide such analysis and annotate functions by han
\end{listing}
\begin{algorithm}
\KwIn{A \minizinc{} operator \(op\) and calling context \(ctx\)}
\KwIn{A \minizinc{} \gls{operator} \(op\) and calling context \(ctx\)}
\KwOut{A tuple containing the contexts of the arguments \(\tuple{ctx_{1}, \ldots{}, ctx_{n}}\)}
@ -490,7 +490,7 @@ However, we currently do not provide such analysis and annotate functions by han
\Return{\tuple{\mixc, \ldots, \mixc}}
}
}
\caption{\label{alg:arg-ctx} Definition of the ``argCtx'' function for \minizinc{} operators.}
\caption{\label{alg:arg-ctx} Definition of the ``argCtx'' function for \minizinc{} \glspl{operator}.}
\end{algorithm}
The context in which the result of a call expression is used must also be considered.
@ -862,7 +862,7 @@ It would always be better to encounter the expression in a context that results
This avoids creating both a full \gls{reif} and a \gls{half-reif} of the same expression.
In the \microzinc{} \interpreter{}, this problem is resolved by only keeping the result of their joint context.
The context recorded in the \gls{cse} table and the found context are joined using the join operator, as described in \cref{fig:half-join}.
The context recorded in the \gls{cse} table and the found context are joined using the join \gls{operator}, as described in \cref{fig:half-join}.
If this context is different from the recorded context, then the expression is re-evaluated in the joint context and its result kept in the \gls{cse} table.
All usages of the previously recorded \gls{cvar} are replaced by the new result.
The dependency tracking, through the use of \constraints{} attached to \variables{}, ensures that all defining \constraints{} are removed from the model.
@ -929,9 +929,9 @@ If it is found that for an expression that is about to be \gls{half-reified} the
The expression is \gls{reified} and replaces the existing \gls{half-reified} expression.
\begin{example}
Consider for example the \mzninline{=} operator on integers, which \microzinc{} represents as an \mzninline{int_eq} call.
When its expression is negated, pushing the negation inwards will result in a \mzninline{!=} operator, a \mzninline{int_ne} call.
The opposite happens when a negation is pushed inwards for an expression using \mzninline{!=} operator.
Consider for example the \mzninline{=} \gls{operator} on integers, which \microzinc{} represents as an \mzninline{int_eq} call.
When its expression is negated, pushing the negation inwards will result in a \mzninline{!=} \gls{operator}, a \mzninline{int_ne} call.
The opposite happens when a negation is pushed inwards for an expression using \mzninline{!=} \gls{operator}.
So to ensure that a \negc{} occurrence of \mzninline{int_eq} and a \posc{} occurrence of \mzninline{int_ne} use the same \gls{cvar} they are both mapped to \mzninline{int_eq} in the \gls{cse} table.
The mapping ensures that the context is correctly transformed when accessing the \gls{cse} table for an \mzninline{int_ne} call.
\end{example}
@ -1002,7 +1002,7 @@ First, to show the benefit of implementing \glspl{propagator} for \gls{half-reif
We recreate two experiments presented by \textcite{feydy-2011-half-reif} in the original \gls{half-reif} paper in a modern \gls{cp} solver, \gls{chuffed}.
We adapt the \glspl{propagator} for the non-\gls{reified} \constraints{} to take into account the \gls{cvar}, by reusing the code for checking and pruning as described in \cref{sec:half-propagation}.
Additionally, we assess the effects of automatically detecting and introducing \glspl{half-reif} during the \gls{rewriting} process.
Additionally, we assess the effects of detecting and introducing \glspl{half-reif} during the \gls{rewriting} process.
We rewrite and solve 200 \minizinc{} \instances{} for several \solvers{} with and without the use of \gls{half-reif}.
We then analyse the trends in the generated \glspl{slv-mod} and their solving performance.
@ -1140,7 +1140,7 @@ Finally, statistics for \gls{rewriting} the \instances{} for a \gls{maxsat} \sol
Unlike linearization, \gls{half-reif} does not significantly reduce the number of \constraints{} and, although still significant, the number of \glspl{reif} is reduced by only slightly over ten percent.
We also see that the \gls{booleanization} library is explicitly defined in terms of \glspl{half-reif}.
Some \constraints{} manually introduce \mzninline{_imp} call as part of their definition.
Even when we do not automatically introduce \glspl{half-reif}, they are still introduced by other \constraints{}.
Even when \gls{rewriting} does not introduce \glspl{half-reif}, they are still introduced by the \glspl{decomp} of other \constraints{}.
Furthermore, \gls{chain-compression} does not seem to have any effect.
Since all \glspl{half-reif} are defined in terms of clauses, the implications normally removed using \gls{chain-compression} are instead aggregated into larger clauses.
Surprisingly, \gls{half-reif} slightly reduces the \gls{rewriting} time as it reduces the workload.

2
chapters/4_half_reif_preamble.tex
View File

@ -20,4 +20,4 @@ In \cref{sec:half-intro,sec:half-propagation} we introduce the core concepts of
\Cref{sec:half-decomposition} shows the benefits of \gls{half-reif} when writing \glspl{decomp} 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 extension \minizinc{}.
Then, in \cref{sec:half-rewriting}, we elaborate on how using \gls{half-reif} changes the \gls{rewriting} process.
Finally, the effects of \glspl{propagator} for \gls{half-reified} \constraints{} and the automatic introduction of \gls{half-reif} is analysed in \cref{sec:half-experiments}.
Finally, the effects of \glspl{propagator} for \gls{half-reified} \constraints{} and the introduction of \gls{half-reif} is analysed in \cref{sec:half-experiments}.

78
chapters/5_incremental.tex
View File

@ -66,6 +66,8 @@ This extension is based on the constructs introduced in \minisearch{}, as summar
\subsection{Meta-Optimization in MiniSearch}\label{sec:inc-minisearch}
\glsreset{neighbourhood}
\minisearch{} introduced a \minizinc{} extension that enables modellers to express \gls{meta-optimization} inside a \minizinc{} model.
A \gls{meta-optimization} algorithm in \minisearch{} typically solves a given \minizinc{} model, performs some calculations on the \gls{sol}, adds new \constraints{} and then solves again.
@ -77,7 +79,7 @@ In \minisearch{} these definitions can make use of the following function.
function int: sol(var int: x)
\end{mzn}
It returns the value that variable \mzninline{x} was assigned to in the previous \gls{sol} (similar functions are defined for Boolean, float, and set variables).
It returns the value that variable \mzninline{x} was assigned to in the previous \gls{sol} (similar functions are defined for Boolean, float, and set \variables{}).
This allows the \gls{neighbourhood} to be defined in terms of the previous \gls{sol}.
In addition, a \gls{neighbourhood} definition will typically make use of the random number generators available in \minizinc{}.
@ -119,6 +121,8 @@ We define a few additional \minizinc{} \glspl{annotation} and functions that
\subsection{Restart Annotation}
\glsreset{restart}
Instead of the complex \minisearch{} definitions, we propose to add support for \glspl{meta-optimization} that are purely based on the notion of \glspl{restart}.
A \gls{restart} happens when a solver abandons its current search efforts, returns to its initial \gls{search-space}, and begins a new exploration.
Many \gls{cp} \solvers{} already provide support for controlling their restarting behaviour.
@ -145,7 +149,7 @@ The proposed \glspl{annotation} are shown in \cref{lst:inc-restart-ann}.
The \mzninline{restart_on_solution} \gls{annotation} tells the solver to restart immediately for each \gls{sol}, rather than looking for the best one in each restart.
The \mzninline{restart_without_objective} tells it not to add \gls{bnb} \constraints{} on the \gls{objective}.
The other \mzninline{restart_X}\glspl{annotation} define different strategies for restarting the search when a \gls{sol} cannot be found (these strategies have already been part of the \minizinc{} standard library since version 2.2.0).
The other \mzninline{restart_X} \glspl{annotation} define different strategies for restarting the search when a \gls{sol} cannot be found. (These strategies have already been part of the \minizinc{} standard library since version 2.2.0).
The \mzninline{timeout} \gls{annotation} gives an overall time limit for the search.
Finally, the \mzninline{restart_limit} stops the search after a certain number of \glspl{restart}.
@ -156,7 +160,7 @@ Finally, the \mzninline{restart_limit} stops the search after a certain number o
\subsection{Advanced Meta-Optimization Algorithms}
Although using just \gls{restart} \glspl{annotation} by themselves allows us to run the basic \gls{lns}, more advanced \gls{meta-optimization} algorithms will require more than reapplying the same \gls{neighbourhood} time after time.
Although using just \gls{restart} \glspl{annotation} by themselves allows us to run a basic \gls{lns}, more advanced \gls{meta-optimization} algorithms will require more than reapplying the same \gls{neighbourhood} time after time.
It is, for example, often beneficial to use several \gls{neighbourhood} definitions within the same \instance{}.
Different \glspl{neighbourhood} may be able to improve different aspects of a \gls{sol} at different phases of the search.
Adaptive \gls{lns} \autocite{ropke-2006-adaptive, pisinger-2007-heuristic} is a variant of \gls{lns} that keeps track of the \glspl{neighbourhood} that led to improvements and favours them for future iterations.
@ -190,8 +194,8 @@ Function \mzninline{status} returns the status of the previous restart, namely:
The function \mzninline{last_val} allows modellers to access the last value assigned to a \variable{}.
Like \mzninline{sol}, it has versions for all basic \variable{} types.
If \mzninline{status()=SAT \/ status{}=OPT}, then \mzninline{last_val(x)} and \mzninline{sol(x)} return the same value.
However, if \mzninline{status()=UNSAT \/ status{}=UNKNOWN}, but \mzninline{x} was still (at some point) assigned during search, then that value will be returned by \mzninline{last_val(x)}, whereas \mzninline{sol(x)} will still return the value from the last \gls{sol}.
If \mzninline{status()=SAT \/ status()=OPT}, then \mzninline{last_val(x)} and \mzninline{sol(x)} return the same value.
However, if \mzninline{status()=UNSAT \/ status()=UNKNOWN}, but \mzninline{x} was still (at some point) assigned during search, then that value will be returned by \mzninline{last_val(x)}, whereas \mzninline{sol(x)} will still return the value from the last \gls{sol}.
The value is undefined when \mzninline{status()=START} or when \mzninline{x} was not present during the last \gls{restart}.
If a \variable{} \mzninline{x} is assigned immediately after each restart (before any \glspl{search-decision}), then it is guaranteed that \mzninline{last_val(x)} will return this value after the next restart.
@ -209,7 +213,7 @@ Therefore, we identify each \variable{} using their variable path \autocite{leo-
The path of a \variable{} is designed to give a unique identifier to a \variable{} when an \instance{} is rewritten multiple times.
The \variable{} path is mostly dependent on the \parameter{} arguments to the calls and the value of iterators for which the \variable{} is introduced.
As such, this mechanism will between \glspl{restart} correctly identify the \variables{} for each call to the nullary function in the \mzninline{on_restart} \gls{annotation}.
However, it can lead to slightly unexpected behaviour when using \parameter{} function arguments that do not relate to the \mzninline{avar} introduced in the function.
However, it can lead to slightly unexpected behaviour when using \parameter{} function arguments that do not relate to the \gls{avar} introduced in the function.
\paragraph{Parametric neighbourhood selection predicates}
@ -282,25 +286,21 @@ Therefore, we introduce the following function that can be used to signal to the
function var bool: complete();
\end{mzn}
\noindent{}When the \variable{} returned by this function \gls{fixed} to \true{}, then the search is complete.
\noindent{}When the \variable{} returned by this function is \gls{fixed} to \true{}, then the search is complete.
If any \gls{sol} was found, it is declared an \gls{opt-sol}.
With \mzninline{restart_without_objective}, the \gls{restart} predicate is now responsible for constraining the \gls{objective}.
Note that a simple hill-climbing (for minimization) can still be defined easily in this context as follows.
\begin{mzn}
predicate hill_climbing() =
if status() != START then
_objective < sol(_objective);
elseif status() = UNSAT then
complete();
endif;
\end{mzn}
Note that a simple hill-climbing (for minimization) can still be defined easily in this context as shown in \cref{lst:inc-hill-climb}.
It takes advantage of the fact that the declared \gls{objective} is available through the built-in \variable{} \mzninline{_objective}.
\begin{listing}
\mznfile{assets/listing/inc_hill_climb.mzn}
\caption{\label{lst:inc-hill-climb}A predicate implementing a simple hill climbing search for minimization.}
\end{listing}
A more interesting example is a simulated annealing strategy.
When using this strategy, the sequence of \glspl{sol} that the \solver{} finds are not required to steadily improve in quality.
Instead, the \solver{} can produce \glspl{sol} that potentially with a potentially reduced objective value.
Instead, the \solver{} can produce \glspl{sol} that potentially reduce the objective value.
Over time, we decrease the amount by which a \gls{sol} can decrease objective value until we are only looking for improvements.
This \gls{meta-optimization} can help the \solver{} to quickly approximate the \gls{opt-sol}.
\Cref{lst:inc-sim-ann} show how this strategy is also easy to express using \gls{rbmo}.
@ -318,14 +318,14 @@ Any subsequent \gls{sol} must improve the quality of this \gls{objective}.
If there does not exist such a \gls{sol}, then we move on to the next important \gls{objective}.
We then look for a \gls{sol} that improves the quality of this \gls{objective}, without decreasing the quality of more important \glspl{objective}.
We then repeat this process until we reach the least important \gls{objective}, and we cannot find \glspl{sol} that improve it any longer.
A predicate that implements lexicographic search is shown in \cref{lst:inc-lex-min}.
\begin{listing}
\mznfile{assets/listing/inc_lex_min.mzn}
\caption{\label{lst:inc-lex-min}A predicate implementing lexicographic search.}
\end{listing}
The lexicographic tracks the active \gls{objective} using the \mzninline{stage} \variable{}.
A predicate that implements lexicographic search is shown in \cref{lst:inc-lex-min}.
This predicate tracks the active \gls{objective} using the \mzninline{stage} \variable{}.
Initially, the stage is set to one: it tries to find an \gls{opt-sol} for the first \gls{objective}.
Whenever we find a \gls{sol} we keep the same \mzninline{stage} value, but constrain the \gls{search-space} to find a better \gls{sol}.
When there does not exist a better \gls{sol}, we increase the value of the \mzninline{stage}, but ensure the \glspl{objective} keep their optimal value.
@ -345,11 +345,11 @@ There is a maximum number we can handle, \mzninline{ms}.
At the start the number of \glspl{sol} is zero.
If we do not find any \glspl{sol}, then we finish the entire search.
Otherwise, we record that we have one more \gls{sol}.
We store the \gls{sol} values in \mzninline{s1} and \mzninline{s2} \glspl{array}.
We store the \gls{sol} values in the \mzninline{s1} and \mzninline{s2} \glspl{array}.
Before each \gls{restart} we add \constraints{} removing Pareto dominated \glspl{sol}, based on each previous \gls{sol}.
Additionally, we maintain the \glspl{sol} stored in \mzninline{s1} and \mzninline{s2} by assigning them to their previous value and avoid search on the unused spaces in the \glspl{array} by assignment them to the lower bound of their respective \gls{objective}.
Additionally, we maintain the \glspl{sol} stored in \mzninline{s1} and \mzninline{s2} by assigning them to their previous value and avoid search on the unused spaces in the \glspl{array} by assigning them to the lower bound of their respective \gls{objective}.
It should be noted that the \glspl{sol} found by this search will still contain dominated \gls{sol}, so an additional filtering step would be needed to compute only non-dominated \glspl{sol}.
It should be noted that the \glspl{sol} found by this search will still contain dominated \glspl{sol}, so an additional filtering step would be needed to compute only non-dominated \glspl{sol}.
\section{Rewriting of Meta-Optimization Algorithms}\label{sec:inc-solver-extension}
@ -369,7 +369,7 @@ It has to compute the correct value whenever a predicate is evaluated.
Instead, the \gls{rewriting} scheme presented below uses a limited form of partial evaluation: \parameters{} that are known during \gls{rewriting} will be fully evaluated; those only known during the solving, such as the result of a call to any of the new functions (\mzninline{sol}, \mzninline{status}, etc.), are replaced by \variables{}.
This essentially \textbf{turns the new functions into \gls{native} \constraints{}} for the target \solver{}.
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 automatically perform the evaluation of the new functions by propagating the \gls{native} \constraints{}.
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.
@ -451,7 +451,7 @@ Second, the \solver{} needs to be able to parse the new \constraints{} \mzninlin
During solving, the \solver{} needs to execute the new constraints as follows.
\begin{description}
\item[\mzninline{status(s)}] Record the status of the previous \gls{restart}, and fix \mzninline{s} to the recorded status.
\item[\mzninline{status(s)}] Record the status of the last \gls{restart}, and fix \mzninline{s} to the recorded status.
\item[\mzninline{sol(x, sx)} (variants)] Constrain \mzninline{sx} to be equal to the value of \mzninline{x} in the incumbent \gls{sol}.
If a \gls{sol} has not yet been found, then it does not constrain \mzninline{sx}.
\item[\mzninline{last_val(x, lx)} (variants)] Constrain \mzninline{lx} to take the last value assigned to \mzninline{x} during search.
@ -535,10 +535,10 @@ The new items can be added to the program, and the \gls{rewriting} can proceed a
Removing an item, however, is not so simple.
A \variable{} can only be removed if it is not used in any \constraints{}.
When we remove a \constraint{}, all effects the \constraint{} had on the \nanozinc{} program have to be undone.
This includes results of \gls{propagation}, \gls{cse} and other simplifications.
This includes results of \gls{propagation}, \gls{cse}, and other simplifications.
\begin{example}\label{ex:inc-incremental}
Consider the following \minizinc\ fragment:
Consider the following \minizinc{} fragment.
\begin{mzn}
constraint x < 10;
@ -566,7 +566,7 @@ The \gls{trail} records all changes to the \nanozinc{} program:
These changes can be caused by the \gls{rewriting} of a \constraint{}, \gls{propagation}, or \gls{cse}.
When a \constraint{} is removed, its corresponding changes are undone by reversing all actions recorded on the \gls{trail} up to the point where the \constraint{} was added.
In order to limit the amount of \gls{trail}ing required, the programmer must create explicit ``choice points'' to which the system state can be reset.
In order to limit the amount of \gls{trail}ing required, the modeller must create explicit ``choice points'' to which the system state can be reset.
In particular, this means that until the first choice point is created \gls{rewriting} can be performed without any \gls{trail}ing.
\begin{example}\label{ex:inc-trail}
@ -686,11 +686,11 @@ The overall time out for each run is 120 seconds.
The \gls{gbac} problem comprises courses having a specified number of credits and lasting a certain number of periods, load limits of courses for each period, prerequisites for courses, and preferences of teaching periods for professors.
A detailed description of the problem is given in \autocite{chiarandini-2012-gbac}.
The main decisions are to assign courses to periods, which is done via the \variables{} \mzninline{period_of} in the \minizinc{} model.
\cref{lst:inc-free-period} shows the neighbourhood chosen, which fixes the periods of all courses according to the previous \gls{sol}, except for one randomly selected period.
\Cref{lst:inc-free-period} shows the neighbourhood chosen, which fixes the periods of all courses according to the previous \gls{sol}, except for one randomly selected period.
\begin{listing}[b]
\mznfile{assets/listing/inc_gbac_neighbourhood.mzn}
\caption{\label{lst:inc-free-period}\gls{gbac}: \gls{neighbourhood} freeing all courses in a period.}
\caption{\label{lst:inc-free-period}\gls{gbac} \gls{neighbourhood} freeing all courses in a period.}
\end{listing}
\begin{figure}
@ -702,7 +702,7 @@ The main decisions are to assign courses to periods, which is done via the \vari
\includegraphics[width=\columnwidth]{assets/img/inc_obj_chuffed_gbac.pdf}
\caption{\label{subfig:inc-obj-chuffed-gbac}\gls{chuffed}}
\end{subfigure}
\caption{\label{fig:inc-obj-gbac}\gls{gbac}: integral of cumulative objective value of solving 5 \instances{}.}
\caption{\label{fig:inc-obj-gbac}\gls{gbac} integral of cumulative objective value of solving 5 \instances{}.}
\end{figure}
The results for the \gls{gbac} in \cref{fig:inc-obj-gbac} show that the overhead introduced by \gls{gecode} using \gls{rbmo} compared to replaying the \glspl{neighbourhood} is quite low.
@ -722,7 +722,7 @@ These orders can then be freely reassigned to any other slab.
\begin{listing}
\mznfile{assets/listing/inc_steelmillslab_neighbourhood.mzn}
\caption{\label{lst:inc-free-bin}Steel mill slab: \gls{neighbourhood} that frees all orders assigned to a selected slab.}
\caption{\label{lst:inc-free-bin}Steel mill slab \gls{neighbourhood} that frees all orders assigned to a selected slab.}
\end{listing}
@ -735,10 +735,10 @@ These orders can then be freely reassigned to any other slab.
\includegraphics[width=\columnwidth]{assets/img/inc_obj_chuffed_steelmillslab.pdf}
\caption{\label{subfig:inc-obj-chuffed-steelmillslab}\gls{chuffed}}
\end{subfigure}
\caption{\label{fig:inc-obj-steelmillslab}Steel mill slab: integral of cumulative objective value of solving 5 \instances{}.}
\caption{\label{fig:inc-obj-steelmillslab} Steel mill slab integral of cumulative objective value of solving 5 \instances{}.}
\end{figure}
\Cref{subfig:inc-obj-gecode-steelmillslab} again only shows minimal overhead for the \gls{rbmo} compared to replaying the \glspl{neighbourhood}.
\Cref{fig:inc-obj-steelmillslab} again only shows minimal overhead for the \gls{rbmo} compared to replaying the \glspl{neighbourhood}.
For this problem a \gls{sol} with zero wastage is always optimal.
As such the \gls{lns} approaches are sometimes able to prove a \gls{sol} is optimal and finish before the time-out.
This is the case for \gls{chuffed} instances, where almost all \instances{} are solved using the \gls{rbmo} method.
@ -757,7 +757,7 @@ Tasks scheduled in this period can be reshuffled.
\begin{listing}
\mznfile{assets/listing/inc_rcpsp_neighbourhood.mzn}
\caption{\label{lst:inc-free-timeslot}\Gls{rcpsp}/wet: \gls{neighbourhood} freeing all tasks starting in the drawn interval.}
\caption{\label{lst:inc-free-timeslot}\Gls{rcpsp}/wet \gls{neighbourhood} freeing all tasks starting in the drawn interval.}
\end{listing}
\begin{figure}
@ -769,7 +769,7 @@ Tasks scheduled in this period can be reshuffled.
\includegraphics[width=\columnwidth]{assets/img/inc_obj_chuffed_rcpspw.pdf}
\caption{\label{subfig:inc-obj-chuffed-rcpspw}\gls{chuffed}}
\end{subfigure}
\caption{\label{fig:inc-obj-rcpspw}\gls{rcpsp}/wet: integral of cumulative objective value of solving 5 \instances{}.}
\caption{\label{fig:inc-obj-rcpspw}\gls{rcpsp}/wet integral of cumulative objective value of solving 5 \instances{}.}
\end{figure}
\Cref{fig:inc-obj-rcpspw} shows once more that \gls{rbmo} has little overhead over the replaying approach.
@ -811,7 +811,7 @@ The problem therefore has a lexicographic objective: a \gls{sol} is better if it
The results appear in \cref{subfig:inc-cmp-lex}.
They show that both incremental methods have a clear advantage over our naive baseline approach.
Although some additional time is spent \gls{rewriting} the \gls{rbmo} models compared to the incremental, it is minimal.
Although some additional time is spent \gls{rewriting} the \gls{rbmo} models compared to \gls{incremental-rewriting}, it is minimal.
The \gls{rewriting} of the \gls{rbmo} \instances{} would likely take less time when using the new prototype architecture.
Between all the methods, solving time is very similar, but \gls{rbmo} seems to have a slight advantage.
We do not notice any benefit from the use of the incremental solver \glsxtrshort{api}.
@ -823,7 +823,7 @@ Instead of setting a time limit, we limit the number of \glspl{restart} that the
As such, we limit the number of \glspl{neighbourhood} that are computed and applied to the \instance{}.
It should be noted that the \gls{rbmo} method is not guaranteed to apply the exact same \glspl{neighbourhood}, due to the difference caused by random number generation.
\Cref{subfig:inc-cmp-lex} shows the results of applying 1000 \glspl{neighbourhood}.
\Cref{subfig:inc-cmp-lns} shows the results of applying 1000 \glspl{neighbourhood}.
In this case there is an even more pronounced difference between the incremental methods and the naive method.
It is surprising to see that the application of 1000 \glspl{neighbourhood} using \gls{incremental-rewriting} still performs very similar to \gls{rewriting} the \gls{rbmo} method.
The solving times are similar between all methods and once again, we do not see any real advantage of the use of the incremental \solver{} \glsxtrshort{api}.

10
chapters/6_conclusions.tex
View File

@ -51,7 +51,7 @@ Two prototype programs were developed to evaluate this architecture:
\item a \microzinc{} \gls{byte-code} \interpreter{} that produces a \nanozinc{} \gls{slv-mod}.
\end{itemize}
The implementation of these prototypes lacks the maturity of the existing \minizinc{} \compiler{}.
The implementation of these prototypes lacks the maturity of the existing \minizinc{} implementation.
However, the performance of these prototypes already surpasses the existing implementation, averaging a more than ten times speed-up.
This architecture enables many avenues of further research.
@ -69,7 +69,7 @@ Similar to how we can remove the defining \constraint{} during \gls{rewriting},
Determining whether a \constraint{} is \gls{reified} is a crucial decision that has to be made during \gls{rewriting}.
Making the wrong decision can significantly impact \gls{solver} performance.
In \cref{ch:half-reif}, we extend our architecture with our second contribution: \textbf{a formal analysis to reason about the \gls{reif} of \constraints{}}.
Not only does this analysis reduce the number of required \glspl{reif}, it is the first implementation that also automatically introduces \glspl{half-reif} when possible.
Not only does this analysis reduce the number of required \glspl{reif}, it is the first implementation that also introduces \glspl{half-reif} when possible.
Our method introduces a new analysis step after the compilation from \minizinc{} to \microzinc{}.
To determine whether a \constraint{} has to be \gls{reified}, this analysis determines the context of each \constraint{}.
@ -86,13 +86,13 @@ We described how we can communicate this change through the \glspl{cvar} of (hal
Lastly, \glspl{half-reif} can introduce \glspl{implication-chain} that can degrade the performance of the \solver{}.
We described a new simplification technique called \gls{chain-compression} that efficiently eliminates these \glspl{implication-chain} where possible.
The techniques to automatically introduce \glspl{half-reif} and the simplification techniques have been implemented in both our prototype \gls{rewriting} architecture and the existing \minizinc{} \compiler{}.
The techniques to introduce \glspl{half-reif} and the simplification techniques have been implemented in both our prototype \gls{rewriting} architecture and the existing \minizinc{} implementation.
These techniques were included in the official release of \minizinc{} in version 2.3.0.
In support of this, we have modified the \gls{rewriting} libraries of existing \minizinc{} \solvers{} to use \gls{half-reif}.
Notably, we have implemented explicit \glspl{decomp} of \gls{half-reified} \constraints{} for \gls{mip} and \gls{sat} \solvers{}.
The usage of these \glspl{decomp} significantly reduces the number of \constraints{} in the \gls{slv-mod}.
Additionally, we implemented two \glspl{propagator} of \gls{half-reif} \constraints{}, \mzninline{all_different} and \mzninline{element}, in a state-of-the-art \gls{cp} \solver{}, \gls{chuffed}, to re-evaluate the claims of the original \gls{half-reif} paper \autocite{feydy-2011-half-reif}.
In our experiments, we reaffirmed the effectiveness of the \glspl{propagator}, but we showed mixed results for the use of automatic \gls{half-reif} on a larger scale.
In our experiments, we reaffirmed the effectiveness of the \glspl{propagator}, but we showed mixed results for the use of \gls{half-reif} on a larger scale.
While it was clearly beneficial for \gls{sat}, other \solvers{} did not seem to enjoy the same benefit and in some cases were even negatively impacted.
Although \gls{half-reif} is not a new technique, there are still numerous open questions.
@ -104,7 +104,7 @@ As a compromise, we could consider a form in between \gls{half-reif} and full \g
In this form the \gls{propagator} would set the \gls{cvar} to \true{} if the \constraint{} holds, but does not propagate the negation of the \constraint{} when it is set to \false{}.
The downside of this form is that it is not equivalent to a logical implication, which means that measures such as \gls{chain-compression} would not be applicable.
However, \glspl{propagator} for this form are still easy to design/implement, and they ensure that the \gls{cvar} is \gls{fixed} through \gls{propagation}.
Finally, automated \gls{half-reif} in \minizinc{} allows for new solving performance improvements by allowing \solver{} implementers to experiment with \glspl{decomp} or \glspl{propagator} for \gls{half-reified} \constraints{}.
Finally, the use of \gls{half-reif} in \minizinc{} allows for new solving performance improvements by allowing \solver{} implementers to experiment with \glspl{decomp} or \glspl{propagator} for \gls{half-reified} \constraints{}.
\section*{Incremental Solving}
Using a \cml{} as the interface for a \gls{meta-optimization} toolchain can be very intuitive and opens up new opportunities.

36
chapters/A2_benchmark.tex
View File

@ -4,7 +4,7 @@
%************************************************
\noindent{}All experiments included in this thesis were conducted on a dedicated node in a computational cluster.
The machine operates using an \textbf{Intel Xeon 8260} \glsxtrshort{cpu}, which has 24 non-hyperthreaded cores, and has access to \textbf{268.55 GB} of \gls{ram}.
The machine operates using an \textbf{Intel Xeon 8260} \glsxtrshort{cpu}, which has 24 non-hyperthreaded cores, and has access to \textbf{268.55 GB} of \glsxtrshort{ram}.
Each experimental test was given exclusive access to a single \glsxtrshort{cpu} core and access to sufficient \glsxtrshort{ram}.
\section{Experimental Design}%
@ -17,7 +17,7 @@ They are accompanied by instructions to perform the experiments.
The experiments are split into three bundles, each testing a different system.
Each part is published as a Git repository on GitHub.
\paragraph{MiniZinc Prototype} The design for the experiments of the \minizinc{} prototype implementation can be found in:
\paragraph{MiniZinc Prototype} The design for the experiments of the \minizinc{} prototype implementation can be found on the following webpage.
\begin{center}
\url{https://github.com/Dekker1/bytecode-benchmarks}
@ -25,7 +25,7 @@ Each part is published as a Git repository on GitHub.
This repository contains the \gls{rewriting} and recursive function benchmarks.
\paragraph{Half-Reification} The design for all the \gls{half-reif} experiments is located in:
\paragraph{Half-Reification} The design for all the \gls{half-reif} experiments is located on the following webpage.
\begin{center}
\url{https://github.com/Dekker1/half-reif-benchmarks}
@ -33,7 +33,7 @@ This repository contains the \gls{rewriting} and recursive function benchmarks.
This repository contains both the benchmark for the \gls{chuffed} \glspl{propagator} of \gls{half-reif} \constraints{} and the \minizinc{} Challenge 2019 \& 2020 benchmark.
\paragraph{Restarting Meta-Search} Finally, the design of the experiments for restart based \gls{meta-optimization} can be found in:
\paragraph{Restarting Meta-Search} Finally, the design of the experiments for restart based \gls{meta-optimization} can be found on the following webpage.
\begin{center}
\url{https://github.com/Dekker1/on-restart-benchmarks}
@ -45,29 +45,29 @@ This repository contains the benchmarks for both \gls{gecode} and \gls{chuffed}.
\section{Software}%
\label{sec:bench-soft}
Central to the experiments in this thesis are two kinds of programs: programs that rewrite a \constraint{} model into a \solver{} specification and the \solvers{} that given a specification search for \glspl{sol}.
Central to the experiments in this thesis are two kinds of programs: programs that rewrite a \constraint{} model into a \gls{slv-mod} and the \solvers{} that search for \glspl{sol}.
We generally test the rewriting programs, in particular to rewrite \minizinc{} \instances{} to \flatzinc{}, but use the \solvers{} to evaluate the effect of changes to these rewriting programs.
\subsection{MiniZinc Rewriting}
In this thesis we use three different programs to rewrite \minizinc{} to \flatzinc{}:
In this thesis we use three different programs to rewrite \minizinc{} to \flatzinc{}.
\begin{itemize}
\item The official release of MiniZinc (version 2.5.5) \autocite{minizinc-2021-minizinc}.
The source code for this version can be found here:
\item The official release of MiniZinc, version 2.5.5 \autocite{minizinc-2021-minizinc}.
The source code for this version can be found on the following webpage.
\begin{center}
\url{https://github.com/MiniZinc/libminizinc/tree/2.5.5}
\end{center}
\item A prototype for the language architecture designed as part of this thesis.
The source code for this version can be found here:
The source code for this version can be found on the following webpage.
\begin{center}
\url{https://github.com/Dekker1/libminizinc/tree/feature/bytecode}
\end{center}
\item The official MiniZinc release (version 2.5.5) \autocite{minizinc-2021-minizinc}, adjusted to support \gls{rbmo}.
The source code for this version can be found here:
\item The official MiniZinc release, version 2.5.5, adjusted to support \gls{rbmo}.
The source code for this version can be found on the following webpage.
\begin{center}
\url{https://github.com/Dekker1/libminizinc/tree/feature/on_restart}
\end{center}
@ -76,10 +76,10 @@ In this thesis we use three different programs to rewrite \minizinc{} to \flatzi
\subsection{MiniZinc Solvers}
In this thesis we use the following \solvers{}:
In this thesis we use the following \solvers{}.
\paragraph{Chuffed} is an open source \gls{lcg} \solver{} \autocite{chuffed-2021-chuffed,chu-2011-chuffed}.
In this thesis we use three different versions of the \gls{chuffed} \solver{}:
In this thesis we use three different versions of the \gls{chuffed} \solver{}.
\begin{itemize}
@ -112,7 +112,7 @@ Its source code is available on the following webpage.
\end{center}
\paragraph{Gecode} is an open source \gls{cp} solver \autocite{schulte-2019-gecode}.
In this thesis we use four different versions of the \gls{gecode} solver:
In this thesis we use four different versions of the \gls{gecode} solver.
\begin{itemize}
\item The official release of \gls{gecode}, version 6.3.0.
@ -170,7 +170,7 @@ A repository of all \minizinc{} models previously used in the challenges and acc
\end{center}
The \gls{rewriting} experiment presented in \cref{sec:rew-experiments} use a selection of seventeen models originating from the \minizinc{} challenge.
These models can identified using the following labels:
These models can identified using the following labels.
\begin{multicols}{3}
\ttfamily
@ -196,7 +196,7 @@ These models can identified using the following labels:
\end{multicols}
The large scale \gls{half-reif} experiment presented in \cref{sec:half-experiments} uses the \minizinc{} instances from 2019 and 2020.
The 2019 \minizinc{} Challenge included the models identified by the following labels:
The 2019 \minizinc{} Challenge included the models identified by the following labels.
\begin{multicols}{3}
\ttfamily
@ -224,7 +224,7 @@ The 2019 \minizinc{} Challenge included the models identified by the following l
\end{itemize}
\end{multicols}
\noindent{}The 2020 \minizinc{} Challenge included the models identified by the following labels:
\noindent{}The 2020 \minizinc{} Challenge included the models identified by the following labels.
\begin{multicols}{3}
\ttfamily
@ -252,7 +252,7 @@ The 2019 \minizinc{} Challenge included the models identified by the following l
\end{itemize}
\end{multicols}
The incremental experiments presented in \cref{sec:inc-experiments} are based on four models from the \minizinc{} Challenge:
The incremental experiments presented in \cref{sec:inc-experiments} are based on four models from the \minizinc{} Challenge, identified by the following labels.
\begin{multicols}{2}
\ttfamily