Add section on constraint aggregation

chapters/4_rewriting.tex

@@ -1025,6 +1025,56 @@ 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}.
 
+
+\subsection{Constraint \titlecap{\glsentrytext{aggregation}}}%
+\label{subsec:rew-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} will result in the following \nanozinc:
+
+\begin{nzn}
+  var int: x;
+  var int: y;
+  var int: z;
+  var int: i1;
+  └── constraint int_times(y, 2);
+  var int: i2;
+  └── constraint int_plus(x, i1);
+  constraint int_le(i2, z);
+\end{nzn}
+
+These \nanozinc\ definitions are correct, but, at least for \gls{mip} solvers,
+the existence of the intermediate variables is likely to have a negative impact
+on the solvers performance. These solves would likely performed better had they
+received the linear constraint \mzninline{int_lin_le([1,2,-1], [x,y,z], 0)}
+directly. Since many solvers support linear constraints, it is often an
+additional burden to have intermediate values that have to be given a value in
+the solution.
+
+This can be resolved using the 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,
+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
+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
+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.}
+
 \section{Experiments}\label{sec:4-experiments}
 
 We have created a prototype implementation of the architecture presented in the
@@ -1064,7 +1114,7 @@ average, the new system achieves a speed-up of \(2.3\), with very few instances
 not achieving any speedup. In terms of memory performance
 (\cref{sfig:4-comparemem}), version 2.4.3 can sometimes still outperform the new
 prototype. We have identified that the main memory bottlenecks are our currently
-unoptimised implementations of CSE lookup tables and argument vectors.
+unoptimised implementations of \gls{cse} lookup tables and argument vectors.
 
 These are very encouraging results, given that we are comparing a largely
 unoptimised prototype to a mature piece of software.