From 1ab2442c8d9acc12fd6d172d6615edfecab2b609 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Mon, 26 Apr 2021 18:06:13 +1000 Subject: [PATCH] Small introduction and spell checking --- assets/acronyms.tex | 1 + assets/glossary.tex | 14 +++ chapters/2_background.tex | 39 ++++++++ chapters/3_rewriting.tex | 180 +++++++++++++++++++------------------ chapters/5_incremental.tex | 113 ++++++++++++----------- 5 files changed, 201 insertions(+), 146 deletions(-) diff --git a/assets/acronyms.tex b/assets/acronyms.tex index a6e6aaa..9ed7442 100644 --- a/assets/acronyms.tex +++ b/assets/acronyms.tex @@ -4,6 +4,7 @@ \newacronym[see={[Glossary:]{gls-cse}}]{cse}{CSE\glsadd{gls-cse}}{Common Subexpression Elimination} \newacronym[see={[Glossary:]{gls-csp}}]{csp}{CSP\glsadd{gls-csp}}{Constraint Satisfaction Problem} \newacronym[see={[Glossary:]{gls-cop}}]{cop}{COP\glsadd{gls-cop}}{Constraint Optimisation Problem} +\newacronym[see={[Glossary:]{gls-lcg}}]{lcg}{LCG\glsadd{gls-lcg}}{Lazy Clause Generation} \newacronym[see={[Glossary:]{gls-lns}}]{lns}{LNS\glsadd{gls-lns}}{Large Neighbourhood Search} \newacronym[see={[Glossary:]{gls-mip}}]{mip}{MIP\glsadd{gls-mip}}{Mixed Integer Programming} \newacronym[see={[Glossary:]{gls-sat}}]{sat}{SAT\glsadd{gls-sat}}{Boolean Satisfiability} diff --git a/assets/glossary.tex b/assets/glossary.tex index 8fa99c4..42a1846 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -24,6 +24,11 @@ description={}, } +\newglossaryentry{chuffed}{ + name={Chuffed}, + description={}, +} + \newglossaryentry{comprehension}{ name={comprehension}, description={}, @@ -79,6 +84,10 @@ description={}, } +\newglossaryentry{gecode}{ + name={Gecode}, + description={}, +} \newglossaryentry{generator}{ name={generator}, description={}, @@ -104,6 +113,11 @@ description={}, } +\newglossaryentry{gls-lcg}{ + name={lazy clause generation}, + description={}, +} + \newglossaryentry{gls-lns}{ name={large neighbourhood search}, description={}, diff --git a/chapters/2_background.tex b/chapters/2_background.tex index c5a4663..861be28 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -555,9 +555,48 @@ expressions in the \gls{solver} model. \section{The Current \glsentrytext{minizinc} Interpreter}% \label{sec:back-mzn-interpreter} +For version 2.5.5 of the \minizinc\ bundle, the \texttt{minizinc} executable is +officially provided tool to solve \minizinc\ instances. A modeller provides the +\texttt{minizinc} executable with a \minizinc\ model, the ground data required +to instantiate the model, and a \gls{solver} definition. Primarily the +\gls{solver} definition defines the \minizinc\ library used to flatten the +\minizinc\ instance and the way in which the \gls{solver} is to be executed. The +process of the \texttt{minizinc} executable can be categorised into the +following stages: + +\begin{description} + \item[Parsing] \texttt{minizinc} parses the input data, the \minizinc\ model, + and the \gls{solver} library. + \item[Type checking] \texttt{minizinc} ensures the type consistency of the + \minizinc\ model, making sure that the types of all expressions match their + declarations and is allowed in the locations where they are used. \\ In the + process of type checking the model, all identifiers and calls are connected to + the declaration that they refer to. + \item[Flattening] \jip{TODO: This should have something} + \item[Optimisation] Given the generated \flatzinc{} model, \texttt{minizinc} + will try optimise this model to try and reduce the number of + \glspl{constraint} and size of the \glspl{domain} of \glspl{variable} in the + \flatzinc\ model. + \item[Solving] The optimised \flatzinc\ model is given to the \gls{solver}. + Any solutions found by the \gls{solver} are communicated back to the user. +\end{description} + +\jip{TODO: Description of the flattening process} + +\jip{TODO: Description of the techniques used during the optimisation phase} + \section{Other Constraint Modelling Languages}% \label{sec:back-other-languages} +\subsection{AMPL}% +\label{sub:back-ampl} + +\subsection{OPL}% +\label{sub:back-} + +\subsection{Essence}% +\label{sub:back-essence} + \section{ACD Term Rewriting}% \label{sec:back-term} diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex index dc7383c..77f48fc 100644 --- a/chapters/3_rewriting.tex +++ b/chapters/3_rewriting.tex @@ -3,7 +3,7 @@ %************************************************ Rewriting a high-level constraint model down into an equivalent solver-level -constraint model might often seems like a simple term rewriting system. In +constraint model might often seem like a simple term rewriting system. In reality, however, simple rewriting of the model will often result in sub-optimal solver-level model and this might result in exponentially more work for the solver. To combat this problem many techniques have been developed to create @@ -35,7 +35,7 @@ tool chain allows us to: \end{itemize} The new architecture is shown in \Cref{sfig:4-newarch}. A constraint model is -first compiled to byte code (called \microzinc), independent of the data. The +first compiled to byte code (called \microzinc{}), independent of the data. The byte code is interpreted with the data to produce \nanozinc\ code, an extension of the existing \flatzinc\ format. The interpreter can even be made incremental: in \cref{ch:incremental} we discuss how in meta optimisation, no recompilation @@ -78,15 +78,15 @@ presents our conclusions. This section introduces the two sub-languages of \minizinc\ at the core of the new abstract machine model we have developed. -\microzinc\ is a simplified subset of \minizinc\ that only contains function +\microzinc{} is a simplified subset of \minizinc\ that only contains function declarations and a restricted expression language, but it extends \minizinc{}'s type system with tuples. Models written in \minizinc\ can be translated into -\microzinc. +\microzinc{}. -\nanozinc\ is similar to \flatzinc\ in that it contains only simple variable +\nanozinc{} is similar to \flatzinc\ in that it contains only simple variable declarations and flat constraints. However, while all function calls in \flatzinc\ need to be solver-level primitives, \nanozinc\ calls can refer to -functions implemented in \microzinc. Furthermore, \nanozinc\ allows for +functions implemented in \microzinc{}. Furthermore, \nanozinc\ allows for constraints to be bound to a specific variable and constraints and variables declarations can be interleaved. @@ -124,7 +124,7 @@ and where expressions have \mzninline{par} type. ::= "in" ["," "in" ]* \end{grammar} - \caption{\label{fig:4-uzn-syntax}Syntax of \microzinc.} + \caption{\label{fig:4-uzn-syntax}Syntax of \microzinc{}.} \end{figure} \newcommand{\sep}{\rhd} @@ -149,17 +149,17 @@ explained in detail in \cref{sec:4-nanozinc}, for now you can ignore them). ::= "└──" \end{grammar} - \caption{\label{fig:4-nzn-syntax}Syntax of \nanozinc.} + \caption{\label{fig:4-nzn-syntax}Syntax of \nanozinc{}.} \end{figure} \subsection{\glsentrytext{minizinc} to \glsentrytext{microzinc}/\glsentrytext{nanozinc}} -The translation from \minizinc\ to \microzinc\ involves the following steps: +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 + \microzinc{}. This includes simple cases such as replacing operator expressions like \mzninline{x+y} by function calls \mzninline{int_plus(x,y)}. As mentioned above, more complex rules for rewriting conditionals with variables, such as \mzninline{if x then A @@ -180,17 +180,17 @@ The translation from \minizinc\ to \microzinc\ involves the following steps: if boolean variable exists. \item Lift the partiality in expressions into the surrounding context to - implement \minizinc{}'s relational semantics. In contrast to \minizinc, - the evaluation of \microzinc\ will implement strict semantics for - partial expressions, whereas \minizinc\ uses relational semantics. - Stuckey and Tack have extensively examined this problems and describe - how to transform any partial function into a total function. + implement \minizinc{}'s relational semantics. In contrast to + \minizinc{}, the evaluation of \microzinc\ will implement strict + semantics for partial expressions, whereas \minizinc\ uses relational + semantics. Stuckey and Tack have extensively examined these problems and + describe how to transform any partial function into a total function. \autocite*{stuckey-2013-functions}. A general approach for describing - the partially in \minizinc\ functions in \microzinc\ functions is to - make the function return both a boolean variable that indicates the - totality of the input variables and the resulting value of the function - that is adjusted that is adjusted to return a predefined value when it - would normally be undefined. For example, The function + the partially in \microzinc\ functions is to make the function return + both a boolean variable that indicates the totality of the input + variables and the resulting value of the function that is adjusted that + is adjusted to return a predefined value when it would normally be + undefined. For example, The function \begin{mzn} function var int: element(array of int: a, var int: x); @@ -230,14 +230,14 @@ The translation from \minizinc\ to \microzinc\ involves the following steps: every call, the function dispatch in \microzinc\ is determined statically. - It is important, however, that the correct version of functions that - allow for both variable and parameter arguments is chosen. And, as we - will later discuss in more detail, is possible for variables to be fixed - to a single value, at which point they can be treated as parameters. The - ensure the correct version of the function is used, functions can be - defined to, at runtime, check if a variable is fixed and, if so, - dispatch to the parameter version of the function. If we for example - have a \minizinc\ function \mzninline{f} that is overloaded on + It is important, however, that the correct version of a function is + chosen when it allows for both variable and parameter parameters. And, + as we will later discuss in more detail, is possible for variables to be + fixed to a single value, at which point they can be treated as + parameters. To ensure the correct version of the function is used, + functions are changed to, at runtime, check if a variable is fixed and, + if so, dispatch to the parameter version of the function. If we for + example have a \minizinc\ function \mzninline{f} that is overloaded on \mzninline{var int} and \mzninline{int}, then the \microzinc\ transformation might look like: @@ -315,8 +315,9 @@ The translation from \minizinc\ to \microzinc\ involves the following steps: Each call in a \nanozinc\ program is either a call to a solver-level predicate, or it has a corresponding \microzinc\ function definition. The goal of partial -evaluation is to transform the \nanozinc\ program into (essentially) \flatzinc, -\ie\ a program where all calls are calls to solver-level predicates. +evaluation is to transform the \nanozinc\ program into (essentially) +\flatzinc{}, \ie\ a program where all calls are calls to solver-level +predicates. To achieve this, we define the semantics of \microzinc\ as a rewriting system that produces \nanozinc\ calls. Each non-primitive call in a \nanozinc\ program @@ -435,7 +436,7 @@ suitable alpha renaming. \tuple{\ensuremath{\texttt{constraint}~\ptinline{F}(a_1, \ldots, a_k), \Env}}} \end{prooftree} \caption{\label{fig:4-rewrite-to-nzn-calls} Rewriting rules for partial evaluation - of \microzinc\ calls to \nanozinc.} + of \microzinc\ calls to \nanozinc{}.} \end{figure*} The rules in \cref{fig:4-rewrite-to-nzn-calls} handle function calls. The first @@ -497,7 +498,7 @@ considered primitives, and as such simply need to be transferred into the \infer2[(ItemC)]{\Sem{\(\mbox{constraint}~C\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow\ \tuple{x, \Env''}} \end{prooftree} \caption{\label{fig:4-rewrite-to-nzn-let} Rewriting rules for partial evaluation - of \microzinc\ let expressions to \nanozinc.} + of \microzinc\ let expressions to \nanozinc{}.} \end{figure*} The rules in \cref{fig:4-rewrite-to-nzn-let} considers let expressions. Starting @@ -561,7 +562,7 @@ notation. \tuple{\mbox{concat} [ A_v~|~v \in{} S ], \Env{} \cup{} \bigcup{}_{v \in{} S} \Env{}_{v}}} \end{prooftree} \caption{\label{fig:4-rewrite-to-nzn-other} Rewriting rules for partial evaluation - of other \microzinc\ expressions to \nanozinc.} + of other \microzinc\ expressions to \nanozinc{}.} \end{figure*} Finally, the rules in \cref{fig:4-rewrite-to-nzn-other} handle the evaluation of @@ -585,23 +586,23 @@ concatenation of the resulting lists with all the additional \nanozinc\ items. Our prototype implementation of the \microzinc/\nanozinc\ framework consists of the following components. -The \textbf{compiler} translates \minizinc\ into a \textbf{bytecode} encoding of -\microzinc. The compiler currently supports a significant subset of the full +The \textbf{compiler} translates \minizinc\ into a \textbf{byte code} encoding of +\microzinc{}. The compiler currently supports a significant subset of the full \minizinc\ language, with the missing features (such as multi-dimensional arrays and complex output statements) requiring additional engineering effort but no new technology. -The \textbf{interpreter} evaluates \microzinc\ bytecode and \nanozinc\ programs +The \textbf{interpreter} evaluates \microzinc\ byte code and \nanozinc\ programs based on the rewrite system introduced in this section. It can read parameter data from a file or via an API\@. The interpreter constructs the call to the -\mzninline{main} function, and then performs the rewriting into flat \nanozinc. +\mzninline{main} function, and then performs the rewriting into flat \nanozinc{}. Memory management is implemented using reference counting, which lends itself well to the optimisations discussed in the next section. The interpreter is written in around 3.5kLOC of C++ to enable easy embedding into applications and other programming languages. The framework includes \textbf{interfaces} to multiple solvers. It can -pretty-print the \nanozinc\ code to standard \flatzinc, so that any solver +pretty-print the \nanozinc\ code to standard \flatzinc{}, so that any solver currently compatible with \minizinc\ can be used. Additionally, a direct C++ API can be used to connect solvers directly, in order to enable incremental solving. This topic is revisited in \cref{ch:incremental}. @@ -667,11 +668,11 @@ prepended by \texttt{└── }). independent of the value of \mzninline{b}. The constraint \mzninline{abs(x) > y} is therefore not required. However, the rewriting has to choose a particular order in which arguments are evaluated, so it is always possible - that it already evaluated the left hand side before ``noticing'' that the + that it already evaluated the left-hand side before ``noticing'' that the disjunction is true. If the system now simplifies the constraint \mzninline{bool_or(b, c)} to - \mzninline{true}, the identifier \mzninline{b} will become unused outside of + \mzninline{true}, the identifier \mzninline{b} will become unused outside its auxiliary definitions, since it was only referenced from the \mzninline{bool_or} call. Removing \mzninline{b} leads will also its defining constraint, \mzninline{int_gt_reif}, being removed. This in turn means that @@ -689,10 +690,10 @@ prepended by \texttt{└── }). other parts of the model not shown here and therefore not removed. \end{example} -Note how how counting usage of variables outside its auxiliary definitions -allows us to remove the \mzninline{z} variable --- we could not simply have -counted the usage of \mzninline{z} in all constraints since the constraint used -to define it, \mzninline{int_abs(x, z)}, would have kept it alive. +Note how counting usage of variables outside its auxiliary definitions allows us +to remove the \mzninline{z} variable --- we could not simply have counted the +usage of \mzninline{z} in all constraints since the constraint used to define +it, \mzninline{int_abs(x, z)}, would have kept it alive. It is important to notice the difference between constraints that appear at the top level and constraints that appear as part of the auxiliary definitions of a @@ -855,7 +856,7 @@ arguments). These links do not take part in the reference counting. Adding \gls{propagation} and simplification into the rewriting system means that the system becomes non-confluent, and some orders of execution may produce -``better'', \ie\ more compact or more efficient, \nanozinc. +``better'', \ie\ more compact or more efficient, \nanozinc{}. \begin{example} The following example is similar to code found in the \minizinc\ libraries of @@ -901,7 +902,7 @@ can then be fully simplified by \gls{propagation}, before the Boolean and reified constraints are rewritten into lower-level linear primitives suitable for MIP\@. -\subsection{Common Subexpression Elimination}\label{sec:4-cse} +\subsection{Common Sub-expression Elimination}\label{sec:4-cse} The simplifications introduced above remove definitions from the model when we can detect that they are no longer needed. In some cases, it is even possible to @@ -946,9 +947,9 @@ in the following example. straightforward approach to ensure that the same instantiation of a function is only evaluated once is through memorisation. After the evaluation of a \microzinc\ call, the instantiated call and its result are stored in a lookup - table, the \gls{cse} table. Before a call is evaluated the \gls{cse} table is - consulted. If the call is found, then the accompanying result is used; - otherwise, the evaluation proceeds as normal. + table, the \gls{cse} table. Then before any consequent call is evaluated the + \gls{cse} table is consulted. If the call is found, then the accompanying + result is used; otherwise, the evaluation proceeds as normal. In our example, the evaluation of \mzninline{pythagoras(i, i)} would proceed as normal to evaluate \mzninline{x = pow(i, 2)}. However, the expression @@ -958,19 +959,19 @@ in the following example. It is worth noting that the \gls{cse} approach based on memorisation also covers the static example above, where the compiler can enforce sharing of common -subexpressions before evaluation begins. However, since the static analysis is -cheap and can potentially avoid many dynamic table lookups, it is valuable to +sub-expressions before evaluation begins. However, since the static analysis is +cheap and can potentially avoid many dynamic table look-ups, it is valuable to combine both approaches. The static approach can be further improved by \emph{inlining} function calls, since that may expose more calls as being syntactically equal. \jip{TODO: \gls{cse} will be discussed in the background. How can we make this - more specific to how it works in \nanozinc} + more specific to how it works in \nanozinc{}.} \paragraph{Reification} -Many constraint modelling languages, including \minizinc, not only enable +Many constraint modelling languages, including \minizinc{}, not only enable constraints to be globally enforced, but typically also support constraints to be \emph{reified} into a Boolean variable. Reification means that a variable \mzninline{b} is constrained to be true if and only if a corresponding @@ -978,7 +979,7 @@ constraint \mzninline{c(...)} holds. We have already seen reification in \cref{ex:4-absreif}: the truth of constraint \mzninline{abs(x) > y} was bound to a Boolean variable \mzninline{b1}, which was then used in a disjunction. We say that the same constraint can be used in \emph{root context} as well as in a -\emph{reified context}. In \minizinc, almost all constraints can be used in both +\emph{reified context}. In \minizinc{}, almost all constraints can be used in both contexts. However, reified constraints are often defined in the library in terms of complicated decompositions into simpler constraints, or require specialised algorithms in the target solvers. In either case, it can be very beneficial for @@ -992,13 +993,14 @@ reification (or in fact any evaluation). We can harness \gls{cse} to store the evaluation context when a constraint is added, and detect when the same constraint is used in both contexts. Whenever a lookup in the \gls{cse} table is successful, action can be taken depending on both the current and stored -evaluation context. If the stored expression was in root context, the constant -\mzninline{true} can be used, independent of the current context. If the stored -expression was in reified context and the current context is reified, the stored -result variable can be used. If the stored expression was in reified context and -the current context is root context, then the previous result can be replaced by -the constant \mzninline{true} (and all its dependencies removed) and the -evaluation will proceed as normal with the root context constraint. +evaluation context. If the stored expression was in root context, then the +constant \mzninline{true} can be used, independent of the current context. +Otherwise, if the stored expression was in reified context and the current +context is reified, then the stored result variable can be used. Finally, if the +stored expression was in reified context and the current context is root +context, then the previous result can be replaced by the constant +\mzninline{true} (and all its dependencies removed) and the evaluation will +proceed as normal with the root context constraint. \begin{example} Consider the fragment: @@ -1011,19 +1013,19 @@ evaluation will proceed as normal with the root context constraint. If we process the top-level constraints in order we create a reified call to \mzninline{q(x)} for the original call. Suppose processing the second - constraint we discover \mzninline{t(x,y)} is \mzninline{true}, setting - \mzninline{b1}. When we process \mzninline{q(x)} in the call - \mzninline{t(x,y)} we find it is the root context. So \gls{cse} needs to set - \mzninline{b0} to \mzninline{true}. + constraint we discover \mzninline{t(x,y)} is \mzninline{true}, fixing + \mzninline{b1}. When we then process \mzninline{q(x)} in instantiation of the + call \mzninline{p(x,y)}, we find it is the root context. So \gls{cse} needs to + set \mzninline{b0} to \mzninline{true}. \end{example} -\minizinc\ distinguishes not only between root and reified contexts, but in +\minizinc{} distinguishes not only between root and reified contexts, but in addition recognises constraints in \emph{positive} contexts, also known as \emph{half-reified} \autocite{feydy-2011-half-reif}. A full explanation and discussion of half-reification can be found in \cref{ch:half_reif}. \jip{TODO: Reification should also be discussed in the background. How can we - make this more specific to how it works in \nanozinc} + make this more specific to how it works in \nanozinc{}.} \subsection{Constraint Aggregation}% \label{subsec:rew-aggregation} @@ -1047,11 +1049,11 @@ operators. For example the evaluation of the linear constraint \mzninline{x + These \nanozinc\ definitions are correct, but, at least for \gls{mip} solvers, the existence of the intermediate variables is likely to have a negative impact -on the solvers performance. These solves would likely performed better had they -received the linear constraint \mzninline{int_lin_le([1,2,-1], [x,y,z], 0)} -directly. Since many solvers support linear constraints, it is often an -additional burden to have intermediate values that have to be given a value in -the solution. +on the \gls{solver}'s performance. These \glspl{solver} would likely perform +better had they received the linear constraint \mzninline{int_lin_le([1,2,-1], +[x,y,z], 0)} directly. Since many solvers support linear constraints, it is +often an additional burden to have intermediate values that have to be given a +value in the solution. This can be resolved using the \gls{aggregation} of constraints. When we aggregate constraints we combine constraints connected through functional @@ -1060,25 +1062,25 @@ intermediate variables. For example, the arithmetic definitions can be combined into linear constraints, Boolean logic can be combined into clauses, and counting constraints can be combined into global cardinality constraints. -In \nanozinc, we are able to aggregate constraints during partial evaluation. To +In \nanozinc{}, we are able to aggregate constraints during partial evaluation. To aggregate a certain kind of constraint, the solver must the constraint as a solver-level primitive. These constraints will now be kept as temporary functional definitions in the \nanozinc\ program. Once a top-level (relational) -constraint is posted that uses the temporary functional definitions as one of +\gls{constraint} is posted that uses the temporary functional definitions as one of its arguments, the interpreter will employ dedicated \gls{aggregation} logic to visit the functional definitions and combine their constraints. The top-level -constraint constraint is then replaced by the combined constraint. When the +\gls{constraint} is then replaced by the combined \gls{constraint}. When the intermediate variables become unused, they will be removed using the normal mechanisms. \jip{TODO: Aggregation is also part of the background. How can we make this more - specific to how it works in \nanozinc} + specific to how it works in \nanozinc{}.} \section{Experiments}\label{sec:4-experiments} We have created a prototype implementation of the architecture presented in the -preceding sections. It consists of a compiler from \minizinc\ to \microzinc, and -an incremental \microzinc\ interpreter producing \nanozinc. The system supports +preceding sections. It consists of a compiler from \minizinc\ to \microzinc{}, and +an incremental \microzinc\ interpreter producing \nanozinc{}. The system supports a significant subset of the full \minizinc\ language; notable features that are missing are support for set and float variables, option types, and compilation of model output expressions and annotations. We will release our implementation @@ -1093,11 +1095,11 @@ well as incremental flattening and solving that demonstrate the efficiency gains that are possible thanks to the new architecture. We selected 20 models from the annual \minizinc\ challenge and compiled 5 -instances of each model to \flatzinc, using the current \minizinc\ release +instances of each model to \flatzinc{}, using the current \minizinc\ release version 2.4.3 and the new prototype system. In both cases we use the standard \minizinc\ library of global constraints (\ie\ we decompose those constraints rather than using solver built-ins, in order to stress-test the flattening). We -measured pure flattening time, \ie\ without time required to parse and typecheck +measured pure flattening time, \ie\ without time required to parse and type check in version 2.4.3, and without time required for compilation to \microzinc\ in the new system (compilation is usually very fast). Times are averages of 10 runs.\footnote{All models obtained from @@ -1123,13 +1125,13 @@ unoptimised prototype to a mature piece of software. \begin{subfigure}[b]{.48\columnwidth} \centering \includegraphics[width=\columnwidth]{assets/img/4_compare_runtime} - \caption{\label{sfig:4-compareruntime}flattening run time (ms)} + \caption{\label{sfig:4-compareruntime}Flattening run time (ms)} \end{subfigure}% \hspace{0.04\columnwidth}% \begin{subfigure}[b]{.48\columnwidth} \centering \includegraphics[width=\columnwidth]{assets/img/4_compare_memory} - \caption{\label{sfig:4-comparemem}flattening memory (MB)} + \caption{\label{sfig:4-comparemem}Flattening memory (MB)} \end{subfigure} \caption{\label{fig:4-runtime}Performance on flattening 100 MiniZinc Challenge instances. \minizinc\ 2.4.3 (x-axis) vs new architecture (y-axis), log-log @@ -1139,10 +1141,10 @@ unoptimised prototype to a mature piece of software. \section{Summary}% \label{sec:rew-summary} -In this chapter, we introduced a systematic view of the execution of \minizinc, -revisiting the rewriting from high-level \minizinc\ to solver-level \flatzinc. -We first introduced introduced the intermediate languages \microzinc\ and -\nanozinc\ and explained how \minizinc\ can be transformed into a set of +In this chapter, we introduced a systematic view of the execution of \minizinc{}, +revisiting the rewriting from high-level \minizinc\ to solver-level \flatzinc{}. +We first introduced the intermediate languages \microzinc{} and +\nanozinc{} and explained how \minizinc\ can be transformed into a set of \microzinc\ definitions and a \nanozinc\ program. We then, crucially, discussed how to partially evaluate a \nanozinc\ program using \microzinc\ definitions and present formal definitions of the rewriting rules applied during partial @@ -1151,7 +1153,7 @@ evaluation. Continuously applying these rules would result in a correct solver-level model, but it is unlikely to be the best model for the solver. We, therefore, discuss multiple techniques to improve the solver-level constraint model during the -partial evaluation of \nanozinc. First, we introduce a novel technique to +partial evaluation of \nanozinc{}. First, we introduce a novel technique to eliminate all unused variables and constraints: we track all constraints that are introduced only to define a variable. This means we can keep an accurate count of when a variable becomes unused by counting only the references to a @@ -1160,7 +1162,7 @@ variable in constraints that do not help define it. Then, we discuss the use of technique can help shrink the domains of the decision variable or even combine variables known to be equal. When a redefinition of a constraint requires the introspection into the current domain of a variable, it is often important to -have the tightest possible domain. Hence, we discuss how in choosing the the +have the tightest possible domain. Hence, we discuss how in choosing the next \nanozinc\ constraint to rewrite, the interpreter can sometimes delay the rewriting of certain constraints to ensure the most amount of information is available. \Gls{cse}, our next optimisation technique, ensures that we do not @@ -1171,7 +1173,7 @@ individual functional constraints can be collected and combined into an aggregated form. This allows us to avoid the existence of intermediate variables in some cases. This optimisation is very important for \gls{mip} solvers. -Finally, we test the described system using a experimental implementation. We +Finally, we test the described system using an experimental implementation. We compare this experimental implementation against the current \minizinc\ interpreter, version 2.5.3, and look at both runtime and its memory usage. Although the experimental implementation there are instances where the diff --git a/chapters/5_incremental.tex b/chapters/5_incremental.tex index e9267ba..1dbeb35 100644 --- a/chapters/5_incremental.tex +++ b/chapters/5_incremental.tex @@ -9,7 +9,7 @@ modifications, thousands of times. Examples of these methods are: \begin{itemize} \item Multi-objective search \autocite{jones-2002-multi-objective}. Optimising - multiple objectives is often not supported directly in solvers. Instead + multiple objectives is often not supported directly in solvers. Instead, it can be solved using a \gls{meta-search} approach: find a solution to a (single-objective) problem, then add more constraints to the original problem and repeat. @@ -41,17 +41,17 @@ All of these examples have in common that a problem instance is solved, new constraints are added, the resulting instance is solved again, and constraints may be removed again. -The usage of these methods is not new to \gls{constraint-modelling} and they +The usage of these methods is not new to \gls{constraint-modelling}, and they have proven to be very useful \autocite{schrijvers-2013-combinators, - rendl-2015-minisearch, schiendorfer-2018-minibrass, ek-2020-online, - ingmar-2020-diverse}. In its most basic form, a simple scripting language is +rendl-2015-minisearch, schiendorfer-2018-minibrass, ek-2020-online, +ingmar-2020-diverse}. In its most basic form, a simple scripting language is sufficient to implement these methods, by repeatedly calling on the \gls{constraint-modelling} infrastructure to compile and solve the adjusted constraint models. While improvements of the compilation of constraint models, such as the ones discussed in previous chapters, can increase the performance of these approaches, the overhead of re-compiling an almost identical model may still prove prohibitive, warranting direct support from the -\gls{constraint-modelling} infrastructure. In this chapter we introduces two +\gls{constraint-modelling} infrastructure. In this chapter we introduce two methods to provide this support: \begin{itemize} @@ -61,7 +61,7 @@ methods to provide this support: algorithms into efficient solver-level specifications based on solver restarts, avoiding re-compilation all-together. \item Alternatively, we can add an incremental interface for adding and - removing constraints to the infrastructure of the \cml. Although this + removing constraints to the infrastructure of the \cml{}. Although this does not avoid the need for re-compilation, it can reduce the work to only the part of the constraint model that has changed. This approach can be used when an algorithm cannot be described using restart-based @@ -70,7 +70,7 @@ methods to provide this support: The rest of the chapter is organised as follows. \Cref{sec:6-modelling} discusses the declarative modelling of restart-based \gls{meta-search} -algorithms that can be modelled directly in a \cml. +algorithms that can be modelled directly in a \cml{}. \Cref{sec:6-solver-extension} introduces the method to compile these \gls{meta-search} specifications into efficient solver-level specifications that only require a small extension of existing \glspl{solver}. @@ -83,8 +83,8 @@ Finally, \Cref{sec:6-conclusion} presents the conclusions. \section{Modelling of Restart-Based Meta-Search}\label{sec:6-modelling} -This section introduces a \minizinc\ extension that enables modellers to define -\gls{meta-search} algorithms in \cmls. This extension is based on the construct +This section introduces a \minizinc{} extension that enables modellers to define +\gls{meta-search} algorithms in \cmls{}. This extension is based on the construct introduced in \minisearch\ \autocite{rendl-2015-minisearch}, as summarised below. @@ -96,7 +96,7 @@ below. % variables that need to be applied to the base model, \eg\ forcing variables to % take the same value as in the previous solution. -\minisearch\ introduced a \minizinc\ extension that enables modellers to express +\minisearch{} introduced a \minizinc{} extension that enables modellers to express meta-searches inside a \minizinc\ model. A meta-search in \minisearch\ typically solves a given \minizinc\ model, performs some calculations on the solution, adds new constraints and then solves again. @@ -157,9 +157,9 @@ To address these two issues, we propose to keep modelling neighbourhoods as predicates, but define \gls{meta-search} algorithms from an imperative perspective. -define a small number of additional \minizinc\ built-in annotations and -functions that (a) allow us to express important aspects of the meta-search in a -more convenient way, and (b) enable a simple compilation scheme that requires no +We define a few additional \minizinc\ built-in annotations and functions that +(a) allow us to express important aspects of the meta-search in a more +convenient way, and (b) enable a simple compilation scheme that requires no additional communication with and only small, simple extensions of the backend solver. @@ -200,7 +200,7 @@ The second component of our \gls{lns} definition is the \emph{restarting strategy}, defining how much effort the solver should put into each neighbourhood (\ie\ restart), and when to stop the overall search. -We propose adding new search annotations to \minizinc\ to control this behaviour +We propose adding new search annotations to the \minizinc\ language to control this behaviour (see \cref{lst:6-restart-ann}). The \mzninline{restart_on_solution} annotation tells the solver to restart immediately for each solution, rather than looking for the best one in each restart, while \mzninline{restart_without_objective} @@ -220,7 +220,7 @@ search after a fixed number of restarts. Although using just a restart annotations by themselves allows us to run the basic \gls{lns} algorithm, more advanced \gls{meta-search} algorithms will -require more then reapplying the same \gls{neighbourhood} time after time. It +require more than reapplying the same \gls{neighbourhood} time after time. It is, for example, often beneficial to use several \gls{neighbourhood} definitions for a problem. Different \glspl{neighbourhood} may be able to improve different aspects of a solution, at different phases of the search. Adaptive \gls{lns} @@ -273,8 +273,7 @@ status is not \mzninline{START}: \mznfile{assets/mzn/6_basic_lns.mzn} In order to use this predicate with the \mzninline{on_restart} annotation, we -cannot simply pass \mzninline{basic_lns(uniform_neighbourhood(x, 0.2))}. First -of all, calling \mzninline{uniform_neighbourhood} like that would result in a +cannot simply pass \mzninline{basic_lns(uniform_neighbourhood(x, 0.2))}. Calling \mzninline{uniform_neighbourhood} like that would result in a \emph{single} evaluation of the predicate, since \minizinc\ employs a call-by-value evaluation strategy. Furthermore, the \mzninline{on_restart} annotation only accepts the name of a nullary predicate. Therefore, users have @@ -299,7 +298,7 @@ activate a different neighbourhood for each restart \begin{listing} \mznfile{assets/mzn/6_round_robin.mzn} - \caption{\label{lst:6-round-robin} A predicate providing the round robin + \caption{\label{lst:6-round-robin} A predicate providing the round-robin meta-heuristic} \end{listing} @@ -330,7 +329,7 @@ We can use the constructs introduced above to implement alternative meta-heuristics such as simulated annealing. In particular, we use \mzninline{restart_without_objective} to tell the solver not to add the branch-and-bound constraint on restart. It will still use the declared objective -to decide whether a new solution is the globally best one seen so far, and only +to decide whether a new solution is globally the best one seen so far, and only output those (to maintain the convention of \minizinc\ solvers that the last solution printed at any point in time is the currently best known one). @@ -345,9 +344,9 @@ through the built-in variable \mzninline{_objective}. A more interesting example is a simulated annealing strategy. When using this strategy, the solutions that the solver finds are no longer required to steadily improve in quality. Instead, we ask the solver to find a solution that is a significant improvement over the -previous solution. Over time we decrease the amount by which we require the +previous solution. Over time, we decrease the amount by which we require the solution needs to improve until we are just looking for any improvements. This -\gls{meta-search} can help improving the qualities of solutions quickly and +\gls{meta-search} can help improve the qualities of solutions quickly and thereby reaching the optimal solution quicker. This strategy is also easy to express using our restart-based modelling: @@ -365,29 +364,29 @@ on. We can model this strategy restarts as such: \mznfile{assets/mzn/6_lex_minimize.mzn} The lexicographic objective changes the objective at each stage in the -evaluation. Initially the stage is 1. Otherwise is we have an UNSAT result, then -the last stage has been completed (proved optimal). We increase the stage by one -if we have stages to go otherwise we finish. Otherwise if the last all was SAT -we maintain the same stage, and store the objective value (for this stage) in -the \mzninline{best} array. For normal computation we fix all the earlier stage -variables to their best value. If we are not in the first run for a stage we add -the branch and bound cut to try to find better solutions. Finally we set the -objective to be the objective for the current stage. +evaluation. Initially the stage is 1. Otherwise, is we have an unsatisfiable +result, then the last stage has been completed (proved optimal). We increase the +stage by one if we have stages to go otherwise we finish. Otherwise, if the last +all was SAT we maintain the same stage, and store the objective value (for this +stage) in the \mzninline{best} array. For normal computation we fix all the +earlier stage variables to their best value. If we are not in the first run for +a stage we add the branch and bound cut to try to find better solutions. +Finally, we set the objective to be the objective for the current stage. There is not always a clear order of importance for different objectives in a problem. In these cases we might instead look for a number of diverse solutions and allow the user to pick the most acceptable options. The following fragment -shows a \gls{meta-search} for the pareto optimality of a pair of objectives: +shows a \gls{meta-search} for the Pareto optimality of a pair of objectives: \mznfile{assets/mzn/6_pareto_optimal.mzn} In this implementation we keep track of the number of solutions found so far using \mzninline{nsol}. There is a maximum number we can handle (\mzninline{ms}). At the start the number of solutions is 0. If we find no -solutions we finish the entire search. Otherwise we record that we have one more -solution. We store the solution values in \mzninline{s1} and \mzninline{s2} -arrays. Before each restart we add constraints removing pareto dominated -solutions, based on each previous solution. +solutions, then we finish the entire search. Otherwise, we record that we have +one more solution. We store the solution values in \mzninline{s1} and +\mzninline{s2} arrays. Before each restart we add constraints removing Pareto +dominated solutions, based on each previous solution. \section{Compilation of Meta-Search Specifications}\label{sec:6-solver-extension} @@ -410,10 +409,10 @@ executed by standard \gls{cp} solvers with a small set of simple extensions. The neighbourhood definitions from the previous section have an important property that makes them easy to compile to standard \flatzinc: they are defined -in terms of standard \minizinc\ expressions, with the exception of a few new -built-in functions. When the neighbourhood predicates are evaluated in the -\minisearch\ way, the \minisearch\ runtime implements those built-in functions, -computing the correct value whenever a predicate is evaluated. +in terms of standard \minizinc\ expressions, except for a few new built-in +functions. When the neighbourhood predicates are evaluated in the \minisearch\ +way, the \minisearch\ runtime implements those built-in functions, computing the +correct value whenever a predicate is evaluated. Instead, the compilation scheme presented below uses a limited form of \emph{partial evaluation}: parameters known at compile time will be fully @@ -426,8 +425,8 @@ evaluation is performed by hijacking the solver's own capabilities: It will automatically perform the evaluation of the new functions by propagating the new constraints. -To compile an \gls{lns} specification to standard \flatzinc, the \minizinc\ compiler -performs four simple steps: +To compile a \gls{lns} specification to standard \flatzinc{}, the \minizinc\ +compiler performs four simple steps: \begin{enumerate} \item Replace the annotation \mzninline{::on_restart("X")} with a call to @@ -506,13 +505,12 @@ Calls to the random number functions have been renamed by appending The definition of these new functions follows the same pattern as for \mzninline{sol}, \mzninline{status}, and \mzninline{last_val}. The MiniZinc definition of the \mzninline{uniform_nbh} function is shown in -\Cref{lst:6-int-rnd}.% -\footnote{Random number functions need to be marked as \mzninline{::impure} for - the compiler not to apply \gls{cse} \autocite{stuckey-2013-functions} if they - are called multiple times with the same arguments.}% -Note that the function accepts variable arguments \mzninline{l} and -\mzninline{u}, so that it can be used in combination with other functions, such -as \mzninline{sol}. +\Cref{lst:6-int-rnd}. \footnote{Random number functions need to be marked as +\mzninline{::impure} for the compiler not to apply \gls{cse} +\autocite{stuckey-2013-functions} if they are called multiple times with the +same arguments.} Note that the function accepts variable arguments \mzninline{l} +and \mzninline{u}, so that it can be used in combination with other functions, +such as \mzninline{sol}. \begin{listing} \mznfile{assets/mzn/6_uniform_slv.mzn} @@ -524,7 +522,7 @@ as \mzninline{sol}. We will now show the minimal extensions required from a solver to interpret the new \flatzinc\ constraints and, consequently, to execute \gls{lns} definitions -expressed in \minizinc. +expressed in \minizinc{}. First, the solver needs to parse and support the restart annotations of~\cref{lst:6-restart-ann}. Many solvers already support all this @@ -541,13 +539,13 @@ new constraints the solver needs to: \item \mzninline{last_val(x, lx)} (variants): constrain \mzninline{lx} to take the last value assigned to \mzninline{x} during search. If no value was ever assigned, it has no effect. Note that many solvers (in particular - SAT and LCG solvers) already track \mzninline{last_val} for their + \gls{sat} and \gls{lcg} solvers) already track \mzninline{last_val} for their variables for use in search. To support \gls{lns} a solver must at least track the \emph{last value} of each of the variables involved in such a constraint. This is straightforward by using the \mzninline{last_val} propagator itself. It wakes up whenever the first argument is fixed, and updates the last value (a non-backtrackable value). - \item random number functions: fix their variable argument to a random number + \item Random number functions: fix their variable argument to a random number in the appropriate probability distribution. \end{itemize} @@ -557,8 +555,8 @@ propagate these constraints in the root node of the search. Modifying a solver to support this functionality is straightforward if it already has a mechanism for posting constraints during restarts. We have -implemented these extensions for both Gecode (110 new lines of code) and Chuffed -(126 new lines of code). +implemented these extensions for both \gls{gecode} (110 new lines of code) and +\gls{chuffed} (126 new lines of code). For example, consider the model from \cref{lst:6-basic-complete} again. \Cref{lst:6-flat-pred} shows a part of the \flatzinc\ that arises from compiling @@ -590,7 +588,7 @@ presentation. \begin{listing} \mznfile{assets/mzn/6_basic_complete_transformed.mzn} - \caption{\label{lst:6-flat-pred} \flatzinc\ that results from compiling \\ + \caption{\label{lst:6-flat-pred} \flatzinc{} that results from compiling \\ \mzninline{basic_lns(uniformNeighbourhood(x,0.2))}.} \end{listing} @@ -600,7 +598,7 @@ and \mzninline{b3} to \mzninline{false}. Therefore, the implication in \lref{line:6:x1:end} is not activated, leaving \mzninline{x[1]} unconstrained. The neighbourhood constraints are effectively switched off. -When the solver restarts, all of the special propagators are re-executed. Now +When the solver restarts, all the special propagators are re-executed. Now \mzninline{s} is not 1, and \mzninline{b1} will be set to \mzninline{true}. The \mzninline{float_random} propagator assigns \mzninline{rnd1} a new random value and, depending on whether it is greater than \mzninline{0.2}, the Boolean @@ -614,9 +612,10 @@ against being invoked before the first solution is found, since the solution has been recorded yet, but we use this simple example to illustrate how these Boolean conditions are compiled and evaluated. -\section{An Incremental Interface for Constraint Modelling Languages}\label{sec:6-incremental-compilation} +\section{An Incremental Interface for Constraint Modelling Languages}% +\label{sec:6-incremental-compilation} -As an alternative approach to run \gls{meta-search} algorithm we propose the +As an alternative approach to run \gls{meta-search} algorithm, we propose the possibility of incremental flattening. The execution of any In order to support incremental flattening, the \nanozinc\ interpreter must be @@ -649,7 +648,7 @@ structure~\autocite{warren-1983-wam}. The trail records all changes to the \nanozinc\ program: \begin{itemize} - \item the addition or removal of new variables or constraints, + \item The addition or removal of new variables or constraints, \item changes made to the domains of variables, \item additions to the \gls{cse} table, and \item substitutions made due to equality propagation.