Small introduction and spell checking

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}

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={},

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}
 

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.
 
     <gen-exp> ::= <ident> "in" <exp> ["," <ident> "in" <exp> ]*
   \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).
 
   <nzn-bind> ::= "└──" <nzn-con>
   \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,
+        implement \minizinc{}'s relational semantics. In contrast to
-        the evaluation of \microzinc\ will implement strict semantics for
+        \minizinc{}, the evaluation of \microzinc\ will implement strict
-        partial expressions, whereas \minizinc\ uses relational semantics.
+        semantics for partial expressions, whereas \minizinc\ uses relational
-        Stuckey and Tack have extensively examined this problems and describe
+        semantics. Stuckey and Tack have extensively examined these problems and
-        how to transform any partial function into a total function.
+        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
+        the partially in \microzinc\ functions is to make the function return
-        make the function return both a boolean variable that indicates the
+        both a boolean variable that indicates the totality of the input
-        totality of the input variables and the resulting value of the function
+        variables and the resulting value of the function that is adjusted that
-        that is adjusted that is adjusted to return a predefined value when it
+        is adjusted to return a predefined value when it would normally be
-        would normally be undefined. For example, The function
+        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
+        It is important, however, that the correct version of a function is
-        allow for both variable and parameter arguments is chosen. And, as we
+        chosen when it allows for both variable and parameter parameters. And,
-        will later discuss in more detail, is possible for variables to be fixed
+        as we will later discuss in more detail, is possible for variables to be
-        to a single value, at which point they can be treated as parameters. The
+        fixed to a single value, at which point they can be treated as
-        ensure the correct version of the function is used, functions can be
+        parameters. To ensure the correct version of the function is used,
-        defined to, at runtime, check if a variable is fixed and, if so,
+        functions are changed to, at runtime, check if a variable is fixed and,
-        dispatch to the parameter version of the function. If we for example
+        if so, dispatch to the parameter version of the function. If we for
-        have a \minizinc\ function \mzninline{f} that is overloaded on
+        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,
+evaluation is to transform the \nanozinc\ program into (essentially)
-\ie\ a program where all calls are calls to solver-level predicates.
+\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
+The \textbf{compiler} translates \minizinc\ into a \textbf{byte code} encoding of
-\microzinc. The compiler currently supports a significant subset of the full
+\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
+Note how counting usage of variables outside its auxiliary definitions allows us
-allows us to remove the \mzninline{z} variable --- we could not simply have
+to remove the \mzninline{z} variable --- we could not simply have counted the
-counted the usage of \mzninline{z} in all constraints since the constraint used
+usage of \mzninline{z} in all constraints since the constraint used to define
-to define it, \mzninline{int_abs(x, z)}, would have kept it alive.
+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
+  table, the \gls{cse} table. Then before any consequent call is evaluated the
-  consulted. If the call is found, then the accompanying result is used;
+  \gls{cse} table is consulted. If the call is found, then the accompanying
-  otherwise, the evaluation proceeds as normal.
+  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
+sub-expressions before evaluation begins. However, since the static analysis is
-cheap and can potentially avoid many dynamic table lookups, it is valuable to
+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
+evaluation context. If the stored expression was in root context, then the
-\mzninline{true} can be used, independent of the current context. If the stored
+constant \mzninline{true} can be used, independent of the current context.
-expression was in reified context and the current context is reified, the stored
+Otherwise, if the stored expression was in reified context and the current
-result variable can be used. If the stored expression was in reified context and
+context is reified, then the stored result variable can be used. Finally, if the
-the current context is root context, then the previous result can be replaced by
+stored expression was in reified context and the current context is root
-the constant \mzninline{true} (and all its dependencies removed) and the
+context, then the previous result can be replaced by the constant
-evaluation will proceed as normal with the root context constraint.
+\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
+  constraint we discover \mzninline{t(x,y)} is \mzninline{true}, fixing
-  \mzninline{b1}. When we process \mzninline{q(x)} in the call
+  \mzninline{b1}. When we then process \mzninline{q(x)} in instantiation of the
-  \mzninline{t(x,y)} we find it is the root context. So \gls{cse} needs to set
+  call \mzninline{p(x,y)}, we find it is the root context. So \gls{cse} needs to
-  \mzninline{b0} to \mzninline{true}.
+  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
+on the \gls{solver}'s performance. These \glspl{solver} would likely perform
-received the linear constraint \mzninline{int_lin_le([1,2,-1], [x,y,z], 0)}
+better had they received the linear constraint \mzninline{int_lin_le([1,2,-1],
-directly. Since many solvers support linear constraints, it is often an
+[x,y,z], 0)} directly. Since many solvers support linear constraints, it is
-additional burden to have intermediate values that have to be given a value in
+often an additional burden to have intermediate values that have to be given a
-the solution.
+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
+preceding sections. It consists of a compiler from \minizinc\ to \microzinc{}, and
-an incremental \microzinc\ interpreter producing \nanozinc. The system supports
+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,
+In this chapter, we introduced a systematic view of the execution of \minizinc{},
-revisiting the rewriting from high-level \minizinc\ to solver-level \flatzinc.
+revisiting the rewriting from high-level \minizinc\ to solver-level \flatzinc{}.
-We first introduced introduced the intermediate languages \microzinc\ and
+We first introduced the intermediate languages \microzinc{} and
-\nanozinc\ and explained how \minizinc\ can be transformed into a set of
+\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

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,
+rendl-2015-minisearch, schiendorfer-2018-minibrass, ek-2020-online,
-  ingmar-2020-diverse}. In its most basic form, a simple scripting language is
+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
+This section introduces a \minizinc{} extension that enables modellers to define
-\gls{meta-search} algorithms in \cmls. This extension is based on the construct
+\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
+We define a few additional \minizinc\ built-in annotations and functions that
-functions that (a) allow us to express important aspects of the meta-search in a
+(a) allow us to express important aspects of the meta-search in a more
-more convenient way, and (b) enable a simple compilation scheme that requires no
+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
+cannot simply pass \mzninline{basic_lns(uniform_neighbourhood(x, 0.2))}. Calling \mzninline{uniform_neighbourhood} like that would result in a
-of all, 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
+evaluation. Initially the stage is 1. Otherwise, is we have an unsatisfiable
-the last stage has been completed (proved optimal). We increase the stage by one
+result, then the last stage has been completed (proved optimal). We increase the
-if we have stages to go otherwise we finish. Otherwise if the last all was SAT
+stage by one if we have stages to go otherwise we finish. Otherwise, if the last
-we maintain the same stage, and store the objective value (for this stage) in
+all was SAT we maintain the same stage, and store the objective value (for this
-the \mzninline{best} array. For normal computation we fix all the earlier stage
+stage) in the \mzninline{best} array. For normal computation we fix all the
-variables to their best value. If we are not in the first run for a stage we add
+earlier stage variables to their best value. If we are not in the first run for
-the branch and bound cut to try to find better solutions. Finally we set the
+a stage we add the branch and bound cut to try to find better solutions.
-objective to be the objective for the current stage.
+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
+solutions, then we finish the entire search. Otherwise, we record that we have
-solution. We store the solution values in \mzninline{s1} and \mzninline{s2}
+one more solution. We store the solution values in \mzninline{s1} and
-arrays. Before each restart we add constraints removing pareto dominated
+\mzninline{s2} arrays. Before each restart we add constraints removing Pareto
-solutions, based on each previous solution.
+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
+in terms of standard \minizinc\ expressions, except for a few new built-in
-built-in functions. When the neighbourhood predicates are evaluated in the
+functions. When the neighbourhood predicates are evaluated in the \minisearch\
-\minisearch\ way, the \minisearch\ runtime implements those built-in functions,
+way, the \minisearch\ runtime implements those built-in functions, computing the
-computing the correct value whenever a predicate is evaluated.
+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
+To compile a \gls{lns} specification to standard \flatzinc{}, the \minizinc\
-performs four simple steps:
+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}.%
+\Cref{lst:6-int-rnd}. \footnote{Random number functions need to be marked as
-\footnote{Random number functions need to be marked as \mzninline{::impure} for
+\mzninline{::impure} for the compiler not to apply \gls{cse}
-  the compiler not to apply \gls{cse} \autocite{stuckey-2013-functions} if they
+\autocite{stuckey-2013-functions} if they are called multiple times with the
-  are called multiple times with the same arguments.}%
+same arguments.} Note that the function accepts variable arguments \mzninline{l}
-Note that the function accepts variable arguments \mzninline{l} and
+and \mzninline{u}, so that it can be used in combination with other functions,
-\mzninline{u}, so that it can be used in combination with other functions, such
+such as \mzninline{sol}.
-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
+implemented these extensions for both \gls{gecode} (110 new lines of code) and
-(126 new lines of code).
+\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.