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

Reorganise background sections

Browse Source
This commit is contained in:
Jip J. Dekker 2021-05-15 11:04:44 +10:00
parent e662ff1510
commit 5f09ec6d02
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
2 changed files with 359 additions and 345 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
assets/glossary.tex
View File

@ -221,7 +221,7 @@
}
\newglossaryentry{operator}{
name={operators},
name={operator},
description={},
}

702
chapters/2_background.tex
View File

@ -76,14 +76,16 @@ the model.
\end{example}
In the remainder of this chapter we will first, in \cref{sec:back-minizinc}
introduce \minizinc\ as the leading \cml\ used within this thesis.
\cref{sec:back-mzn-interpreter} explains the process that the current \minizinc\
interpreter uses to translate a \minizinc\ model into a solver-level constraint
model. Then, \cref{sec:back-other-languages} introduces alternative \cmls\ and
compares their functionality to \minizinc{}. Finally, \cref{sec:back-term} and
\cref{sec:back-clp} survey the closely related fields of \gls{trs} and
\gls{clp}.
In the remainder of this chapter we will first, in \cref{sec:back-minizinc} we
introduce \minizinc\ as the leading \cml\ used within this thesis. In
\cref{sec:back-solving} we discuss how \gls{cp} can be used to solve a
constraint model. We also briefly discuss other solving techniques and the
problem format these techniques expect. \Cref{sec:back-other-languages}
introduces alternative \cmls\ and compares their functionality to \minizinc{}.
Then,\cref{sec:back-term} survey the some closely related technologies in the
field of \glspl{trs}. Finally, \cref{sec:back-mzn-interpreter} explores the
process that the current \minizinc\ interpreter uses to translate a \minizinc\
instance into a solver-level constraint model.
\section{\glsentrytext{minizinc}}%
\label{sec:back-minizinc}
@ -109,9 +111,9 @@ library of constraints allow users to easily model complex problems.
The model starts with the declaration of the \glspl{parameter}.
\Lref{line:back:knap:toys} declares an enumerated type that represents all
possible toys, \(T\) in the mathematical model in the example.
\Lref{line:back:knap:joy,line:back:knap:space} declare arrays mapping from
toys to integer values, these represent the functional mappings \(joy\) and
\(space\). Finally, \lref{line:back:knap:left} declares an integer
\Lrefrange{line:back:knap:joy}{line:back:knap:space} declare arrays mapping
from toys to integer values, these represent the functional mappings \(joy\)
and \(space\). Finally, \lref{line:back:knap:left} declares an integer
\gls{parameter} to represent the car capacity as an equivalent to \(C\).
The model then declares its \glspl{variable}. \Lref{line:back:knap:sel}
@ -330,6 +332,7 @@ The choice between different expressions can often be expressed using a
\gls{conditional} expression, sometimes better known as an ``if-then-else''
expressions. You could, for example, force that the absolute value of
\mzninline{a} is bigger than \mzninline{b} using the constraint
\begin{mzn}
constraint if b >= 0 then a > b else b < a endif;
\end{mzn}
@ -489,17 +492,29 @@ Some expressions in the \cmls\ do not always have a well-defined result.
Examples of such expressions in \minizinc\ are:
\begin{itemize}
\item Division (or modulus) when the divisor is zero: \\ \mzninline{x div 0 =
@??@}
\item Division (or modulus) when the divisor is zero:
\item Array access when the index is outside the given index set: \\
\mzninline{array1d(1..3, [1,2,3])[0] = @??@}
\begin{mzn}
x div 0 = @??@
\end{mzn}
\item Finding the minimum or maximum or an empty set: \\ \mzninline{min({})
=@??@}
\item Array access when the index is outside the given index set:
\item Computing the square root of a negative value: \\ \mzninline{sqrt(-1) =
@??@}
\begin{mzn}
array1d(1..3, [1,2,3])[0] = @??@
\end{mzn}
\item Finding the minimum or maximum or an empty set:
\begin{mzn}
min({}) = @??@
\end{mzn}
\item Computing the square root of a negative value:
\begin{mzn}
sqrt(-1) = @??@
\end{mzn}
\end{itemize}
@ -589,331 +604,6 @@ input types and the basic method of solving the given problem.
\subsection{Hybrid Technologies}%
\label{subsec:back-hybrid}
\section{Compiling \glsentrytext{minizinc}}%
\label{sec:back-mzn-interpreter}
\jip{This section is the only one here that is not really literature review.
Maybe this should just be a separate chapter. It is ``new'' in the sense that
is the first real description of some parts of the compiler, but it is
relatively short.}
Traditionally the compilation process is split into three sequential parts: the
\emph{frontend}, the \emph{middle-end}, and the \emph{backend}. It is the job of
the frontend to parse the user input, report on any errors or inconsistencies in
the input, and transform it into an internal representation. The middle-end
performs the main translation in a target-independent fashion. It converts the
internal representation at the level of the compiler frontend to another
internal representation as close to the level required by the compilation
targets. The final transformation to the format required by the compilation
target are performed by the backend. When a compiler is separated into these few
steps, then adding support for new language or compilation target only require
the addition of a frontend or backend respectively.
The \minizinc\ compilation process categorised in the same three categories, as
shown in \cref{fig:back-mzn-comp}. In the frontend, a \minizinc\ model is first
parsed together with its data into an \gls{ast}. The process will then analyse
the \gls{ast} to discover the types of all expressions used in the instance. If
an inconsistency is discovered, then an error is reported to the user. Finally,
the frontend will also preprocess the \gls{ast}. This process is used to rewrite
expressions into a common form for the middle-end, \eg\ remove the ``syntactic''
sugar. For instance, replacing the usage of enumerated types by normal integers.
\begin{figure}
\centering
\includegraphics[width=\linewidth]{assets/img/back_compilation_structure}
\caption{\label{fig:back-mzn-comp} The compilation structure of the \minizinc\
compiler.}
\end{figure}
The middle-end contains the most important two processes: the flattening and the
optimisation. During the flattening process the high-level (\minizinc{})
constraint model is rewritten into a solver level (\flatzinc{}) constraint
model. It could be noted that the flattening step depends on the compilation
target to define its solver level constraints. Even though the information
required for this step is target dependent, we consider it part of the
middle-end as the mechanism is the same for all compilation targets. A full
description of this process will follow in \cref{subsec:back-flattening}. Once a
solver level constraint model is constructed, the \minizinc\ compiler will try
to optimise this model: shrink domains of variables, remove constraints that are
proven to hold, and remove variables that have become unused. These optimisation
techniques are discussed in \cref{subsec:back-fzn-optimisation}.
The backend will convert the internal solver level constraint model into a
format that can be used by the targeted \gls{solver}. Given the formatted
artefact, a solver process, controlled by the backend, can then be started.
Whenever the solver process produces a solution, the backend will reconstruct
the solution to the specification of the original \minizinc{} model.
In this section we will discuss the flattening and optimisation process as
employed by the 2.5.5 version of \minizinc{} \autocite{minizinc-2021-minizinc}.
\subsection{Flattening}%
\label{subsec:back-flattening}
The goal of the flattening process is to arrive at a ``flat'' constraint model:
it only contains constraints that consist of a singular call instruction, all
arguments to calls are \gls{parameter} literals or \gls{variable} identifiers,
and the call itself is a constraint primitive for the target \gls{solver}.
To arrive at a flat model, the flattening process will transverse the
declarations, \glspl{constraint}, and the solver goal and flatten any expression
contained in these items. The flattening of an expression is a recursive
process. \Gls{parameter} literals and \gls{variable} identifiers are already
flat. For any other kind of expression, its arguments are first flattened. If
the expression itself is a constraint primitive, then it is ready
\jip{This should say something about introducing relational reified constraints.}
\paragraph{Common Sub-expression Elimination}
Because the evaluation of a \minizinc\ expression cannot have any side-effects,
In some cases, it is even possible to not generate definitions in the first
place through the use of \gls{cse}. This simplification is a well understood
technique that originates from compiler optimisation \autocite{cocke-1970-cse}
and has proven to be very effective in discrete optimisation
\autocite{marinov-2005-sat-optimisations, araya-2008-cse-numcsp}, including
during the evaluation of \cmls\ \autocite{rendl-2009-enhanced-tailoring}.
For instance, in the constraint\\
\begin{mzn}
constraint (abs(x)*2 >= 20) \/ (abs(x)+5 >= 15);
\end{mzn}
the expression \mzninline{abs(x)} is occurs twice. There is however no need to
create two separate \glspl{variable} (and defining \glspl{constraint}) to
represent the absolute value of \mzninline{x}. The same \gls{variable} can be
used to represent the \mzninline{abs(x)} in both sides of the disjunction.
Seeing that the same expression occurs multiple times is not always easy. Some
expressions only become syntactically equal during evaluation, as in the
following example.
\begin{example}
Consider the fragment:
\begin{mzn}
function var float: pythagoras(var float: a, var float: b) =
let {
var float: x = pow(a, 2);
var float: y = pow(b, 2);
} in sqrt(x + y);
constraint pythagoras(i, i) >= 5;
\end{mzn}
Although the expressions \mzninline{pow(a, 2)} and \mzninline{pow(b, 2)} are
not syntactically equal, the function call \mzninline{pythagoras(i,i)} using
the same variable for \mzninline{a} and \mzninline{b} makes them equivalent.
\end{example}
A straightforward approach to ensure that the same instantiation of a function
To ensure that syntactically equal expressions are only evaluated once the
\minizinc\ compiler through the use of memorisation. After the flattening of an
expression, the instantiated expression and its result are stored in a lookup
table, the \gls{cse} table. Then before any consequent expression is flattened
the \gls{cse} table is consulted. If an equivalent expression 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 defining
\mzninline{y}, \mzninline{pow(i, 2)}, will be found in the \gls{cse} table and
replaced by the earlier stored result: \mzninline{y = x}.
\gls{cse} also has an important interaction with the occurence of reified
constraints. \Glspl{reification} of a \gls{constraint} 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 the efficiency solving process if we can detect that a
reified constraint is in fact not required.
If a constraint is present in the root context, it means that it must hold
globally. If the same constraint is used in a reified context, it can therefore
be replaced with the constant \mzninline{true}, avoiding the need for
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, 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 the evaluation will proceed as normal with the root context
constraint.
\begin{example}
Consider the fragment:
\begin{mzn}
function var bool: p(var int: x, var int: y) = q(x) /\ r(y);
constraint b0 <-> q(x);
constraint b1 <-> t(x,y);
constraint b1 <-> p(x,y);
\end{mzn}
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}, 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}
\paragraph{Adjusting domains}
As discussed in \cref{subsec:back-cp}, the \glspl{domain} of \glspl{variable}
can sometimes be directly changed because of the addition of a \gls{constraint}.
Similarly, depending on the \glspl{domain} of \glspl{variable} some constraints
can be proven \mzninline{true} or \mzninline{false}.
This principle also applies during the flattening of a \minizinc\ model. It is
generally a good idea to detect cases where we can directly change the
\gls{domain} of a \gls{variable}. Sometimes this might mean that the constraint
does not need to be added at all and that constricting the domain is enough.
Tight domains can also allow us to avoid the creation of reified constraints
when the truth-value of a reified constraints can be determined from the
\glspl{domain} of variables.
\begin{example}%
\label{ex:back-adj-dom}
Consider the following \minizinc\ model:
\begin{mzn}
var 1..10: a;
var 1..5: b;
constraint a < b;
constraint (a > 5) -> (a + b > 12);
\end{mzn}
Given the \glspl{domain} specified in the model, the second constraint is
flattened using to reified \glspl{constraint} for each side of the
implication.
If we however consider the first \gls{constraint}, then we deduce that
\mzninline{a} must always take a value that is 4 or lower. When the compiler
adjust the domain of \mzninline{a} while flattening the first
\gls{constraint}, then the second \gls{constraint} can be simplified. The
expression \mzninline{a > 5} is known to be \mzninline{false}, which means
that the constraint can be simplified to \mzninline{true}.
\end{example}
During flattening, the \minizinc\ compiler will actively remove values from the
\gls{domain} when it encounters constraints that trivially reduces it. For
example, constraints with a single comparison expression between a
\gls{variable} and a \gls{parameter} (\eg\ \mzninline{x != 5}), constraint with
a single comparison between two \glspl{variable} (\eg\ \mzninline{x >= y}),
constraints that directly change the domain (\eg\ \mzninline{x in 3..5}). It,
however, will not perform more complex \gls{propagation}, like the
\gls{propagation} of \glspl{global}.
\paragraph{Constraint Aggregation}
Complex \minizinc\ expression can sometimes result in the creation of many new
variables that represent intermediate results. This is in particular true for
linear and boolean equations that are generally written using \minizinc\
operators. For example the evaluation of the linear constraint \mzninline{x +
2*y <= z} could result in the following \flatzinc:
\begin{nzn}
var int: x;
var int: y;
var int: z;
var int: i1;
var int: i2;
constraint int_times(y, 2, i1);
constraint int_plus(x, i1, i2);
constraint int_le(i2, z);
\end{nzn}
This \flatzinc\ model is correct, but, at least for pure \gls{cp} solvers, the
existence of the intermediate variables is likely to have a negative impact on
the \gls{solver}'s performance. These \glspl{solver} would likely perform better
had they received the equivalent linear constraint
\begin{mzn}
constraint int_lin_le([1,2,-1], [x,y,z], 0)
\end{mzn}
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 collect multiple \minizinc\ expressions, that would
each have been separately translated, and combine them into a singular structure
that eliminates the need for intermediate \glspl{variable}. 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.
The \minizinc\ compiler aggregates expressions whenever possible. When the
\minizinc\ compiler reaches an expression that could potentially be part of an
aggregated constraint, the compiler will not flatten the expression. The
compiler will instead perform a search of its sub-expression to collect all other
expressions to form an aggregated constraint. The flattening process continues
by flattening this aggregated constraint, which might still contain unflattened
arguments.
\paragraph{Delayed Rewriting}
Adjusting the \glspl{domain} of variables during flattening means that the
system becomes non-confluent, and some orders of execution may produce
``better'', \ie\ more compact or more efficient, \flatzinc{}.
\begin{example}
The following example is similar to code found in the \minizinc\ libraries of
\gls{mip} solvers.
\begin{mzn}
function var int: lq_zero_if_b(var int: x, var bool: b) =
x <= ub(x)*(1-b);
\end{mzn}
This predicate expresses the constraint \mzninline{b -> x<=0}, using a
well-known method called ``big-M transformation''. The expression
\mzninline{ub(x)} returns a valid upper bound for \mzninline{x}, \ie\ a fixed
value known to be greater than or equal to \mzninline{x}. This could be the
initial upper bound \mzninline{x} was declared with, or the current value in
the corresponding \nanozinc\ \mzninline{mkvar} call. If \mzninline{b} takes
the value 0, the expression \mzninline{ub(x)*(1-b)} is equal to
\mzninline{ub(x)}, and the constraint \mzninline{x <= ub(x)} holds trivially.
If \mzninline{b} takes the value 1, \mzninline{ub(x)*(1-b)} is equal to 0,
enforcing the constraint \mzninline{x <= 0}.
\end{example}
For \gls{mip} solvers, it is quite important to enforce 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 the
\glspl{domain} of the involved variables has been reduced as much as possible,
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.
The same problem occurs with \glspl{reification} that are produced during
flattening. Other constraints could fix the domain of the reified \gls{variable}
and make the \gls{reification} unnecessary. Instead the constraint (or its
negation) can be flattened in root context. This could avoid the use of a big
decomposition or an expensive propagator.
To tackle this problem, the \minizinc\ compiler employs \gls{del-rew}. When a
linear \gls{constraint} is aggregated or a relational \gls{reification}
\gls{constraint} is introduced it is not directly flattened. Instead these
constraints are appended to the end of the current \gls{ast}. All other
constraints currently still unflattened, that could change the relevant
\glspl{domain}, will be flattened first.
Note that this heuristic does not guarantee that \glspl{variable} have their
tightest possible \gls{domain}. One delayed \gls{constraint} can still influence
the \glspl{domain} of \glspl{variable} used by other delayed \glspl{constraint}.
\subsection{Optimisation}%
\label{subsec:back-fzn-optimisation}
The optimisation process of the \minizinc\ compiler
\section{Other Constraint Modelling Languages}%
\label{sec:back-other-languages}
@ -1251,3 +941,327 @@ constraint store to its state before the last decision was made).
\subsection{ACD Term Rewriting}%
\label{subsec:back-acd}
\section{Compiling \glsentrytext{minizinc}}%
\label{sec:back-mzn-interpreter}
\jip{This section is the only one here that is not really literature review.
Maybe this should just be a separate chapter. It is ``new'' in the sense that
is the first real description of some parts of the compiler, but it is
relatively short.}
Traditionally the compilation process is split into three sequential parts: the
\emph{frontend}, the \emph{middle-end}, and the \emph{backend}. It is the job of
the frontend to parse the user input, report on any errors or inconsistencies in
the input, and transform it into an internal representation. The middle-end
performs the main translation in a target-independent fashion. It converts the
internal representation at the level of the compiler frontend to another
internal representation as close to the level required by the compilation
targets. The final transformation to the format required by the compilation
target are performed by the backend. When a compiler is separated into these few
steps, then adding support for new language or compilation target only require
the addition of a frontend or backend respectively.
The \minizinc\ compilation process categorised in the same three categories, as
shown in \cref{fig:back-mzn-comp}. In the frontend, a \minizinc\ model is first
parsed together with its data into an \gls{ast}. The process will then analyse
the \gls{ast} to discover the types of all expressions used in the instance. If
an inconsistency is discovered, then an error is reported to the user. Finally,
the frontend will also preprocess the \gls{ast}. This process is used to rewrite
expressions into a common form for the middle-end, \eg\ remove the ``syntactic''
sugar. For instance, replacing the usage of enumerated types by normal integers.
\begin{figure}
\centering
\includegraphics[width=\linewidth]{assets/img/back_compilation_structure}
\caption{\label{fig:back-mzn-comp} The compilation structure of the \minizinc\
compiler.}
\end{figure}
The middle-end contains the most important two processes: the flattening and the
optimisation. During the flattening process the high-level (\minizinc{})
constraint model is rewritten into a solver level (\flatzinc{}) constraint
model. It could be noted that the flattening step depends on the compilation
target to define its solver level constraints. Even though the information
required for this step is target dependent, we consider it part of the
middle-end as the mechanism is the same for all compilation targets. A full
description of this process will follow in \cref{subsec:back-flattening}. Once a
solver level constraint model is constructed, the \minizinc\ compiler will try
to optimise this model: shrink domains of variables, remove constraints that are
proven to hold, and remove variables that have become unused. These optimisation
techniques are discussed in \cref{subsec:back-fzn-optimisation}.
The backend will convert the internal solver level constraint model into a
format that can be used by the targeted \gls{solver}. Given the formatted
artefact, a solver process, controlled by the backend, can then be started.
Whenever the solver process produces a solution, the backend will reconstruct
the solution to the specification of the original \minizinc{} model.
In this section we will discuss the flattening and optimisation process as
employed by the 2.5.5 version of \minizinc{} \autocite{minizinc-2021-minizinc}.
\subsection{Flattening}%
\label{subsec:back-flattening}
The goal of the flattening process is to arrive at a ``flat'' constraint model:
it only contains constraints that consist of a singular call instruction, all
arguments to calls are \gls{parameter} literals or \gls{variable} identifiers,
and the call itself is a constraint primitive for the target \gls{solver}.
To arrive at a flat model, the flattening process will transverse the
declarations, \glspl{constraint}, and the solver goal and flatten any expression
contained in these items. The flattening of an expression is a recursive
process. \Gls{parameter} literals and \gls{variable} identifiers are already
flat. For any other kind of expression, its arguments are first flattened. If
the expression itself is a constraint primitive, then it is ready
\jip{This should say something about introducing relational reified constraints.}
\paragraph{Common Sub-expression Elimination}
Because the evaluation of a \minizinc\ expression cannot have any side-effects,
In some cases, it is even possible to not generate definitions in the first
place through the use of \gls{cse}. This simplification is a well understood
technique that originates from compiler optimisation \autocite{cocke-1970-cse}
and has proven to be very effective in discrete optimisation
\autocite{marinov-2005-sat-optimisations, araya-2008-cse-numcsp}, including
during the evaluation of \cmls\ \autocite{rendl-2009-enhanced-tailoring}.
For instance, in the constraint\\
\begin{mzn}
constraint (abs(x)*2 >= 20) \/ (abs(x)+5 >= 15);
\end{mzn}
the expression \mzninline{abs(x)} is occurs twice. There is however no need to
create two separate \glspl{variable} (and defining \glspl{constraint}) to
represent the absolute value of \mzninline{x}. The same \gls{variable} can be
used to represent the \mzninline{abs(x)} in both sides of the disjunction.
Seeing that the same expression occurs multiple times is not always easy. Some
expressions only become syntactically equal during evaluation, as in the
following example.
\begin{example}
Consider the fragment:
\begin{mzn}
function var float: pythagoras(var float: a, var float: b) =
let {
var float: x = pow(a, 2);
var float: y = pow(b, 2);
} in sqrt(x + y);
constraint pythagoras(i, i) >= 5;
\end{mzn}
Although the expressions \mzninline{pow(a, 2)} and \mzninline{pow(b, 2)} are
not syntactically equal, the function call \mzninline{pythagoras(i,i)} using
the same variable for \mzninline{a} and \mzninline{b} makes them equivalent.
\end{example}
A straightforward approach to ensure that the same instantiation of a function
To ensure that syntactically equal expressions are only evaluated once the
\minizinc\ compiler through the use of memorisation. After the flattening of an
expression, the instantiated expression and its result are stored in a lookup
table, the \gls{cse} table. Then before any consequent expression is flattened
the \gls{cse} table is consulted. If an equivalent expression 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 defining
\mzninline{y}, \mzninline{pow(i, 2)}, will be found in the \gls{cse} table and
replaced by the earlier stored result: \mzninline{y = x}.
\gls{cse} also has an important interaction with the occurence of reified
constraints. \Glspl{reification} of a \gls{constraint} 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 the efficiency solving process if we can detect that a
reified constraint is in fact not required.
If a constraint is present in the root context, it means that it must hold
globally. If the same constraint is used in a reified context, it can therefore
be replaced with the constant \mzninline{true}, avoiding the need for
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, 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 the evaluation will proceed as normal with the root context
constraint.
\begin{example}
Consider the fragment:
\begin{mzn}
function var bool: p(var int: x, var int: y) = q(x) /\ r(y);
constraint b0 <-> q(x);
constraint b1 <-> t(x,y);
constraint b1 <-> p(x,y);
\end{mzn}
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}, 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}
\paragraph{Adjusting domains}
As discussed in \cref{subsec:back-cp}, the \glspl{domain} of \glspl{variable}
can sometimes be directly changed because of the addition of a \gls{constraint}.
Similarly, depending on the \glspl{domain} of \glspl{variable} some constraints
can be proven \mzninline{true} or \mzninline{false}.
This principle also applies during the flattening of a \minizinc\ model. It is
generally a good idea to detect cases where we can directly change the
\gls{domain} of a \gls{variable}. Sometimes this might mean that the constraint
does not need to be added at all and that constricting the domain is enough.
Tight domains can also allow us to avoid the creation of reified constraints
when the truth-value of a reified constraints can be determined from the
\glspl{domain} of variables.
\begin{example}%
\label{ex:back-adj-dom}
Consider the following \minizinc\ model:
\begin{mzn}
var 1..10: a;
var 1..5: b;
constraint a < b;
constraint (a > 5) -> (a + b > 12);
\end{mzn}
Given the \glspl{domain} specified in the model, the second constraint is
flattened using to reified \glspl{constraint} for each side of the
implication.
If we however consider the first \gls{constraint}, then we deduce that
\mzninline{a} must always take a value that is 4 or lower. When the compiler
adjust the domain of \mzninline{a} while flattening the first
\gls{constraint}, then the second \gls{constraint} can be simplified. The
expression \mzninline{a > 5} is known to be \mzninline{false}, which means
that the constraint can be simplified to \mzninline{true}.
\end{example}
During flattening, the \minizinc\ compiler will actively remove values from the
\gls{domain} when it encounters constraints that trivially reduces it. For
example, constraints with a single comparison expression between a
\gls{variable} and a \gls{parameter} (\eg\ \mzninline{x != 5}), constraint with
a single comparison between two \glspl{variable} (\eg\ \mzninline{x >= y}),
constraints that directly change the domain (\eg\ \mzninline{x in 3..5}). It,
however, will not perform more complex \gls{propagation}, like the
\gls{propagation} of \glspl{global}.
\paragraph{Constraint Aggregation}
Complex \minizinc\ expression can sometimes result in the creation of many new
variables that represent intermediate results. This is in particular true for
linear and boolean equations that are generally written using \minizinc\
operators. For example the evaluation of the linear constraint \mzninline{x +
2*y <= z} could result in the following \flatzinc:
\begin{nzn}
var int: x;
var int: y;
var int: z;
var int: i1;
var int: i2;
constraint int_times(y, 2, i1);
constraint int_plus(x, i1, i2);
constraint int_le(i2, z);
\end{nzn}
This \flatzinc\ model is correct, but, at least for pure \gls{cp} solvers, the
existence of the intermediate variables is likely to have a negative impact on
the \gls{solver}'s performance. These \glspl{solver} would likely perform better
had they received the equivalent linear constraint
\begin{mzn}
constraint int_lin_le([1,2,-1], [x,y,z], 0)
\end{mzn}
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 collect multiple \minizinc\ expressions, that would
each have been separately translated, and combine them into a singular structure
that eliminates the need for intermediate \glspl{variable}. 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.
The \minizinc\ compiler aggregates expressions whenever possible. When the
\minizinc\ compiler reaches an expression that could potentially be part of an
aggregated constraint, the compiler will not flatten the expression. The
compiler will instead perform a search of its sub-expression to collect all other
expressions to form an aggregated constraint. The flattening process continues
by flattening this aggregated constraint, which might still contain unflattened
arguments.
\paragraph{Delayed Rewriting}
Adjusting the \glspl{domain} of variables during flattening means that the
system becomes non-confluent, and some orders of execution may produce
``better'', \ie\ more compact or more efficient, \flatzinc{}.
\begin{example}
The following example is similar to code found in the \minizinc\ libraries of
\gls{mip} solvers.
\begin{mzn}
function var int: lq_zero_if_b(var int: x, var bool: b) =
x <= ub(x)*(1-b);
\end{mzn}
This predicate expresses the constraint \mzninline{b -> x<=0}, using a
well-known method called ``big-M transformation''. The expression
\mzninline{ub(x)} returns a valid upper bound for \mzninline{x}, \ie\ a fixed
value known to be greater than or equal to \mzninline{x}. This could be the
initial upper bound \mzninline{x} was declared with, or the current value in
the corresponding \nanozinc\ \mzninline{mkvar} call. If \mzninline{b} takes
the value 0, the expression \mzninline{ub(x)*(1-b)} is equal to
\mzninline{ub(x)}, and the constraint \mzninline{x <= ub(x)} holds trivially.
If \mzninline{b} takes the value 1, \mzninline{ub(x)*(1-b)} is equal to 0,
enforcing the constraint \mzninline{x <= 0}.
\end{example}
For \gls{mip} solvers, it is quite important to enforce 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 the
\glspl{domain} of the involved variables has been reduced as much as possible,
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.
The same problem occurs with \glspl{reification} that are produced during
flattening. Other constraints could fix the domain of the reified \gls{variable}
and make the \gls{reification} unnecessary. Instead the constraint (or its
negation) can be flattened in root context. This could avoid the use of a big
decomposition or an expensive propagator.
To tackle this problem, the \minizinc\ compiler employs \gls{del-rew}. When a
linear \gls{constraint} is aggregated or a relational \gls{reification}
\gls{constraint} is introduced it is not directly flattened. Instead these
constraints are appended to the end of the current \gls{ast}. All other
constraints currently still unflattened, that could change the relevant
\glspl{domain}, will be flattened first.
Note that this heuristic does not guarantee that \glspl{variable} have their
tightest possible \gls{domain}. One delayed \gls{constraint} can still influence
the \glspl{domain} of \glspl{variable} used by other delayed \glspl{constraint}.
\subsection{Optimisation}%
\label{subsec:back-fzn-optimisation}
The optimisation process of the \minizinc\ compiler