diff --git a/assets/glossary.tex b/assets/glossary.tex index d676a8a..45cb16a 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -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}. } diff --git a/assets/listing/back_tsp.mzn b/assets/listing/back_tsp.mzn index de8b681..c1451e5 100644 --- a/assets/listing/back_tsp.mzn +++ b/assets/listing/back_tsp.mzn @@ -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]]); diff --git a/chapters/1_introduction.tex b/chapters/1_introduction.tex index 5fe8506..311319b 100644 --- a/chapters/1_introduction.tex +++ b/chapters/1_introduction.tex @@ -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: diff --git a/chapters/2_background.tex b/chapters/2_background.tex index cb7c81b..89cc24a 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -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. diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex index 5f7c407..c11ede1 100644 --- a/chapters/3_rewriting.tex +++ b/chapters/3_rewriting.tex @@ -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{} and \syntax{}, which can be assumed to be the same as the definition of \syntax{} and \syntax{} 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{} in \glspl{comprehension}, the conditions \syntax{} in \gls{conditional} expressions, and the \syntax{} 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}. diff --git a/chapters/4_half_reif.tex b/chapters/4_half_reif.tex index 1d00c21..52efc96 100644 --- a/chapters/4_half_reif.tex +++ b/chapters/4_half_reif.tex @@ -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} diff --git a/chapters/4_half_reif_preamble.tex b/chapters/4_half_reif_preamble.tex index b690146..56aaa54 100644 --- a/chapters/4_half_reif_preamble.tex +++ b/chapters/4_half_reif_preamble.tex @@ -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. diff --git a/chapters/5_incremental.tex b/chapters/5_incremental.tex index b53fcc9..ee4c51b 100644 --- a/chapters/5_incremental.tex +++ b/chapters/5_incremental.tex @@ -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}. diff --git a/chapters/5_incremental_preamble.tex b/chapters/5_incremental_preamble.tex index 5e4ac81..93a85e1 100644 --- a/chapters/5_incremental_preamble.tex +++ b/chapters/5_incremental_preamble.tex @@ -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. \ No newline at end of file +Finally, \Cref{sec:inc-experiments} reports on the experimental results of both approaches. diff --git a/chapters/6_conclusions.tex b/chapters/6_conclusions.tex index 2b7f051..e468a87 100644 --- a/chapters/6_conclusions.tex +++ b/chapters/6_conclusions.tex @@ -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}.