diff --git a/assets/glossary.tex b/assets/glossary.tex index b41890b..c99bc8c 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -9,6 +9,10 @@ % program that implements that API}, % } +\newglossaryentry{aggregation}{ + name={aggregation}, + description={}, +} \newglossaryentry{gls-cbls}{ name={constraint-based local search}, diff --git a/chapters/1_introduction.tex b/chapters/1_introduction.tex index f2b6d85..bfa427d 100644 --- a/chapters/1_introduction.tex +++ b/chapters/1_introduction.tex @@ -23,7 +23,7 @@ model can be used with any of these solvers, which is achieved through the use of solver-specific libraries of constraint definitions. In \minizinc, these solver libraries are written in the same language. -\minizinc\ turned out to be much more expressive than expected, so more +As such, \minizinc\ turned out to be much more expressive than expected, so more and more preprocessing and model transformation has been added to both the core \minizinc\ library, and users' models. And in addition to one-shot solving, \minizinc\ is frequently used as the basis of a larger meta-optimisation tool diff --git a/chapters/4_rewriting.tex b/chapters/4_rewriting.tex index a10cc89..4daf0d0 100644 --- a/chapters/4_rewriting.tex +++ b/chapters/4_rewriting.tex @@ -755,7 +755,7 @@ by garbage collection in the interpreter. Since our prototype interpreter uses reference counting, it already accurately tracks the liveness of each identifier. -\subsection{Constraint propagation} +\subsection{Constraint Propagation} Another way that variables can become unused is if a constraint can be detected to be true based on its semantics, and the known domains of the variables. For @@ -767,7 +767,7 @@ model without changing satisfiability. This, in turn, may result in their auxiliary definitions, if any). This is a simple form of \gls{propagation}, the main inference method used in -constraint solvers \autocite{schulte-2008-propagation}. Constraint propagation, +constraint solvers \autocite{schulte-2008-propagation}. \gls{propagation}, in general, can not only detect when constraints are trivially true (or false), but also tighten variable domains. For instance, given the constraint \mzninline{x>y}, with initial domains \mzninline{x in 1..10, y in 1..10}, would @@ -782,7 +782,7 @@ the \mzninline{abs} function. We therefore need to track whether a variable domain has been enforced through external constraints, or is the consequence of its own definition. We omit the details of this mechanism for space reasons. -A further effect of constraint propagation is the replacement of constraints by +A further effect of \gls{propagation} is the replacement of constraints by simpler versions. A constraint \mzninline{x=y+z}, where the domain of \mzninline{z} has been tightened to the singleton \mzninline{0..0}, can be rewritten to \mzninline{x=y}. Propagating the effect of one constraint can thus @@ -792,12 +792,12 @@ run all propagation rules or algorithms until they reach a fix-point. The \nanozinc\ interpreter applies propagation rules for the most important constraints, such as linear and Boolean constraints, which can lead to significant reductions in generated code size. It has been shown previously that -applying full constraint propagation during compilation can be beneficial +applying full \gls{propagation} during compilation can be beneficial \autocite{leo-2015-multipass}, in particular when the target solver requires complicated reformulations (such as linearisation for MIP solvers \autocite{belov-2016-linearisation}). -Returning to the example above, constraint propagation (and other model +Returning to the example above, \gls{propagation} (and other model simplifications) can result in \emph{equality constraints} \mzninline{x=y} being introduced. For certain types of target solvers, in particular those based on constraint programming, equality constraints can lead to exponentially larger @@ -850,8 +850,8 @@ equalities to the target constraint solver. \paragraph{Implementation} Rewriting a function call that has a \microzinc\ definition and rewriting a -constraint due to propagation are very similar. The interpreter therefore simply -interleaves both forms of rewriting. Efficient constraint propagation engines +constraint due to \gls{propagation} are very similar. The interpreter therefore simply +interleaves both forms of rewriting. Efficient \gls{propagation} engines ``wake up'' a constraint only when one of its variables has received an update (\ie\ when its domain has been shrunk). To enable this, the interpreter needs to keep a data structure linking variables to the constraints where they appear @@ -860,7 +860,7 @@ arguments). These links do not take part in the reference counting. \subsection{Delayed Rewriting} -Adding constraint propagation and simplification into the rewriting system means +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. @@ -888,7 +888,7 @@ that the system becomes non-confluent, and some orders of execution may produce For MIP solvers, it is quite important to enforce \emph{tight} bounds in order to improve efficiency and sometimes even numerical stability. It would therefore be useful to rewrite the \mzninline{lq_zero_if_b} predicate only after all the -constraint propagation has been performed, in order to take advantage of the +\gls{propagation} has been performed, in order to take advantage of the tightest possible bounds. On the other hand, evaluating a predicate may also \emph{impose} new bounds on variables, so it is not always clear which order of evaluation is best. @@ -897,18 +897,18 @@ In our \microzinc/\nanozinc\ system, we allow predicates and functions to be \emph{annotated} as potential candidates for \emph{delayed rewriting}. Any annotated constraint is handled by the (CallPrimitive) rule rather than the (Call) rule, which means that it is simply added as a call into the \nanozinc\ -code, without evaluating its body. When propagation reaches a fix-point, all -annotations are removed from the current \nanozinc\ program, and evaluation +code, without evaluating its body. When \gls{propagation} reaches a fix-point, +all annotations are removed from the current \nanozinc\ program, and evaluation resumes with the predicate bodies. This crucial optimisation enables rewriting in multiple \emph{phases}. For example, a model targeted at a MIP solver is rewritten into Boolean and reified constraints, whose definitions are annotated to be delayed. The \nanozinc\ model -can then be fully simplified by constraint propagation, before the Boolean and +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{\titlecap{\glsentrytext{gls-cse}}}\label{sec:4-cse} +\subsection{Common Subexpression 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 @@ -931,10 +931,10 @@ evaluation even begins, and hoisted into a let expression: constraint let { var int: y = abs(x) } in (y*2 >= 20) \/ (y+5 >= 15) \end{mzn} -% + However, some expressions only become syntactically equal during evaluation, as in the following example. -% + \begin{example} Consider the fragment: @@ -971,6 +971,10 @@ 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} + \paragraph{Reification} Many constraint modelling languages, including \minizinc, not only enable @@ -1025,8 +1029,10 @@ 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} -\subsection{Constraint \titlecap{\glsentrytext{aggregation}}}% +\subsection{Constraint Aggregation}% \label{subsec:rew-aggregation} Complex \minizinc\ expression can sometimes result in the creation of many new @@ -1054,7 +1060,7 @@ 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 aggregation of constraints. When we aggregate +This can be resolved using the \gls{aggregation} of constraints. When we aggregate constraints we combine constraints connected through functional definitions into one or multiple constraints eliminating the need for intermediate variables. For example, the arithmetic definitions can be combined into linear constraints, @@ -1066,14 +1072,14 @@ 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 -its arguments, the interpreter will employ dedicated aggregation logic to visit +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 intermediate variables become unused, they will be removed using the normal mechanisms. -\jip{TODO: Add the example of aggregating the previous example from the - \nanozinc\ to the linear expression.} +\jip{TODO: Aggregation is also part of the background. How can we make this more + specific to how it works in \nanozinc} \section{Experiments}\label{sec:4-experiments} @@ -1157,18 +1163,20 @@ 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 variable in constraints that do not help define it. Then, we discuss the use of -constraint propagation during the partial evaluation of the \nanozinc\ program. -This 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 next \nanozinc\ constraint to rewrite, the interpreter can -sometimes delay the rewriting of certain constraints to ensure the most amount -of information is available. The final optimisation technique, \gls{cse}, -ensures that we do not create or evaluate the same constraint or function twice -and reuse variables where possible. - -\jip{todo: Aggregation} +\gls{propagation} during the partial evaluation of the \nanozinc\ program. This +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 +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 +create or evaluate the same constraint or function twice and reuse variables +where possible. Finally, the last optimisation technique we discuss is the use +of constraint \gls{aggregation}. The use of \gls{aggregation} ensures that 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 compare this experimental implementation against the current \minizinc\