Work on the reification chapter

- Comments by Peter
- Additional reference
- Listings

assets/bibliography/references.bib

···
 	year = {2020},
 }
 
+@inbook{lodi-2013-variability,
+	author = {Andrea Lodi and Andrea Tramontani},
+	title = {Performance Variability in Mixed-Integer Programming},
+	booktitle = {Theory Driven by Influential Applications},
+	chapter = {Chapter 1},
+	year = 2013,
+	pages = {1-12},
+	doi = {10.1287/educ.2013.0112},
+	URL = {https://pubsonline.informs.org/doi/abs/10.1287/educ.2013.0112},
+	eprint = {https://pubsonline.informs.org/doi/pdf/10.1287/educ.2013.0112},
+}
+
 @article{lougee-heimer-2003-coin,
 	author = {Robin Lougee{-}Heimer},
 	title = {The Common Optimization INterface for Operations Research: Promoting

assets/listing/half_alldiff.mzn

···
+predicate all_different(array[int] of var int: x) =
+	forall(i,j in index_set(x) where i < j)(
+		x[i] != x[j]
+	);

assets/listing/half_impli.mzn

···
+predicate impli(
+	var bool: x ::promise_ctx_antitone,
+	var bool: y ::promise_ctx_monotone
+) =
+	not x \/ y;

assets/listing/half_reif_check.mzn

···
+predicate _int_lin_le_imp(
+	array[int] of int: c,
+	array[int] of var int: x,
+	int: d,
+	var bool: b
+) =
+	if is_fixed(b) then
+		if fix(b) then
+			int_lin_le(c, x, d)
+		else
+			true
+		endif
+	else
+		int_lin_le_imp(c, x, d, b)
+	endif;

chapters/2_background.tex

···
 	\item and the \gls{objective} is included as a solving goal.
 \end{itemize}
 
-More complex models also include definitions for custom types, user defined functions, and a custom output format.
+More complex models also include definitions for custom types, user-defined functions, and a custom output format.
 These items are not constrained to occur in any particular order.
 We briefly discuss the most important model items.
 Note that these items already refer to \minizinc{} expressions, which will be discussed in \cref{subsec:back-mzn-expr}.
···
 The type of a \parameter{} can similarly be marked by the \mzninline{par} keyword, but this is not required. 
 These types are used both as normal \parameters{} and as \variables{}.
 To better structure models, \minizinc{} allows collections of these types to be contained in \glspl{array}.
-Unlike other languages, \glspl{array} have a user defined index set, which can start at any value, but they have to be a continuous range.
+Unlike other languages, \glspl{array} have a user-defined index set, which can start at any value, but they have to be a continuous range.
 For example, the following declaration declares an array going from 5 to 10 of new Boolean \variables{}.
 
 \begin{mzn}

chapters/4_half_reif.tex

···
 
 \begin{enumerate}
 	\item \Gls{rewriting} using \glspl{half-reif} naturally produces \glspl{rel-sem}.
-	\item \Glspl{propagator} for a \glspl{half-reif} can often be constructed by merely altering a \gls{propagator} implementation for its regular \constraint{}.
+	\item \Glspl{propagator} for a \glspl{half-reif} can usually be constructed by merely altering a \gls{propagator} implementation for its regular \constraint{}.
 	\item \Gls{half-reif} does not often interact with its \gls{cvar}, limiting the amount of triggered \glspl{propagator} that are known to be unable to prune any \domains{}.
 \end{enumerate}
 
···
 \end{description}
 
 As previously explained, \gls{half-reif} can be used for expressions in \posc{} context.
-Although expressions in a \negc{} context cannot be directly \gls{half-reified}, the negation of a expression in a \negc{} context can be \gls{half-reified}.
+Although expressions in a \negc{} context cannot be directly \gls{half-reified}, the negation of an expression in a \negc{} context can be \gls{half-reified}.
 
 \begin{example}
 	Consider, for example, the following \constraint{}.
···
 \end{example}
 
 Expressions in a \mixc{} context are in a position where \gls{half-reif} is impossible.
-Only full \gls{reif} can be used for expressions in that are in this context.
+Only full \gls{reif} can be used for expressions that are in this context.
 This occurs, for example, when using an exclusive or expression in a \constraint{}.
 The value that one side must take directly depends on the value that the other side takes.
 Each side can thus be forced to be true or false.
···
 
 \begin{algorithm}
 	
-	\KwIn{A function \(check\), that returns false when the \constraint{} \(c\) cannot be satisfied, a function \(prune\), that eliminates values from \variable{} \glspl{domain} that violate\glsadd{violated} the \constraint{} \(c\), and a Boolean control \variable{} \texttt{b}.
+	\KwIn{A function \(check\), that returns false when the \constraint{} \(c\) cannot be satisfied, a function \(prune\), that eliminates values from \variable{} \glspl{domain} that violate\glsadd{violated} the \constraint{} \(c\), and a Boolean \gls{cvar} \texttt{b}.
 	}
 	\KwResult{This pseudo code propagates the \gls{half-reif} of \(c\) (\ie{} \(\texttt{b} \implies\ c\)).}
 
···
 For all these \glspl{reif}, its replacement by a \gls{half-reif} can remove half of the implications required for the \gls{reif}.
 
 For \gls{sat} solvers, a \gls{decomp} for a \gls{half-reif} can be created from its regular \gls{decomp}.
-Any \constraint{} \(c\) will \gls{decomp} into \gls{cnf}.
+Any \constraint{} \(c\) will \gls{decomp} into \gls{cnf} of the following form.
 \[ c = \forall_{i} \exists_{j} lit_{ij} \]
 The \gls{half-reif}, with \gls{cvar} \texttt{b}, could take the following encoding.
 \[ \texttt{b} \implies c = \forall_{i} \neg \texttt{b} \lor \exists_{j} lit_{ij} \]
···
 
 \begin{example}
 
-	Consider the following user-defined \minizinc{} implementation of a logical implication.
+	Consider the user-defined \minizinc{} implementation of a logical implication in \cref{lst:half-impli}.
 
-	\begin{mzn}
-		predicate impli(
-			var bool: x ::promise_ctx_antitone,
-			var bool: y ::promise_ctx_monotone
-		) =
-			not x \/ y;
-	\end{mzn}
+	\begin{listing}
+		\mznfile{assets/listing/half_impli.mzn}
+		\caption{\label{lst:half-impli} A user-defined predicate of a logical implication using \glspl{annotation} to define the context usage of its arguments.}
+	\end{listing}
 
-	The annotations placed on the argument of the \mzninline{impli} function will apply the same context transformations as the \mzninline{->} operator shown in \cref{alg:arg-ctx}.
+	The \glspl{annotation} placed on the argument of the \mzninline{impli} function will apply the same context transformations as the \mzninline{->} operator shown in \cref{alg:arg-ctx}.
 	In term of context analysis, this function now is equivalent to the \minizinc{} operator.
 
 \end{example}
···
 		\Case{\mzninline{ > }, \mzninline{>= }, \mzninline{- }}{
 			\Return{\tuple{\changepos{}ctx, \changeneg{}ctx}}
 		}
-		\Case{\mzninline{ <-> }, \mzninline{xor }, \mzninline{* }}{
+		\Case{\mzninline{ <-> }, \mzninline{= },  \mzninline{xor }, \mzninline{* }}{
 			\Return{\tuple{\mixc, \mixc}}
 		}
 		\Case{\mzninline{ /\ }}{
···
 		Note that this can only occur when a \gls{native} \constraint{} does not define a \gls{reif}.
 \end{enumerate}
 
-The (Access) and (ITE) rules show the context inference for \gls{array} access and if-then-else expressions respectively.
+The (Access) and (ITE) rules show the context inference for \gls{array} access and \gls{conditional} expressions respectively.
 Their inner expressions are evaluated in \(\changepos{}ctx\).
 The inner expressions cannot be simply be evaluated in \(ctx\), because it is not yet certain which expression will be chosen.
 This is important for when \(ctx\) is \rootc{}, since we, at compile time, cannot say which expression will hold globally.
···
 \label{subsec:half-?root}
 
 In the previous section, we briefly discussed the context transformations for the (Access) and (ITE) rules in \cref{fig:half-analysis-expr}.
-Different from the rules described, when an \gls{array} access or if-then-else expression is found in \rootc{} context, it often makes sense to evaluate its sub-expression in \rootc{} context as well.
+Different from the rules described, when an \gls{array} access or \gls{conditional} expression is found in \rootc{} context, it often makes sense to evaluate its sub-expression in \rootc{} context as well.
 It is, however, not always safe to do so.
 
 \begin{example}
···
 	For example, consider the following \microzinc{} fragment.
 
 	\begin{mzn}
-		\constraint{} if b then
+		constraint if b then
 				F(x, y, z)
 			else
 				G(x, y, z)
 			endif;
 	\end{mzn}
 
-	In this case, since only one side of the if-then-else expression is evaluated, the compiler can output calls to the \rootc{} variant of the functions.
+	Let us assume that \mzninline{b} is a \parameter{}, but that its value is not known during the compilation from \minizinc{} to \microzinc{}.
+	In this case, we know that only one side of the \gls{conditional} expression will evaluated, and that call will then globally constrain the \cmodel{}.
+	As such, the \compiler{} can output calls to the \rootc{} variant of the functions.
 	This will enforce the \constraint{} in the most efficient way.
 
 	Things, however, change when the situation gets more complex.
···
 		} in ret;
 	\end{mzn}
 
-	One side of the if-then-else expression is also used in a disjunction.
+	One side of the \gls{conditional} expression is also used in a disjunction.
 	If \mzninline{b} evaluates to \mzninline{true}, then \mzninline{p} is evaluated in \rootc{} context, and \mzninline{p} can take the value \mzninline{true} in the disjunction.
 	Otherwise, \mzninline{q} is evaluated in \rootc{} context, and \mzninline{p} in the disjunction must be evaluated in \posc{} context.
-	It is, therefore, not safe to assume that all sides of the if-then-else expressions are evaluated in \rootc{} context.
+	In this situation, it is not safe for the \compiler{} to output calls for the \rootc{} variants of these calls.
 \end{example}
 
 Using the \changepos{} transformation for sub-expression contexts is safe, but it places a large burden on the \solver{}.
 The solver performs better when the no \gls{reif} has to be used.
 
-To detect situation where the sub-expression are only used in an \gls{array} access or if-then-else expression we introduce the \mayberootc{} context.
+To detect situation where the sub-expression are only used in an \gls{array} access or \gls{conditional} expression we introduce the \mayberootc{} context.
 This context functions as a ``weak'' \rootc{} context.
 If it is joined with any other context, then it acts as \posc{}.
 The extended join operation is shown in \cref{fig:half-maybe-join}.
···
 	\caption{\label{fig:half-analysis-maybe-root} Updated context inference rules for \mayberootc{}.}
 \end{figure*}
 
-\Cref{fig:half-analysis-maybe-root} shows the additional inference rules for \gls{array} access and if-then-else expressions.
+\Cref{fig:half-analysis-maybe-root} shows the additional inference rules for \gls{array} access and \gls{conditional} expressions.
 Looking back at \cref{ex:half-maybe-root}, these additional rules and updated join operation will ensure that the first case will correctly use \rootc{} context calls.
 For the second case, however, it detects that \mzninline{p} is used in both \posc{} and \mayberootc{} context.
 Therefore, it will output the \posc{} call for the right hand side of \mzninline{p}, even when \mzninline{b} evaluates to \mzninline{true}.
···
 \section{Rewriting and Half Reification}%
 \label{sec:half-rewriting}
 
-During the \gls{rewriting} process the contexts assigned to the different expressions can be used directly to determine if and how a expression has to be \gls{reified}.
+During the \gls{rewriting} process the contexts assigned to the different expressions can be used directly to determine if and how an expression has to be \gls{reified}.
 
 \begin{example}
 \label{ex:half-rewriting}
···
 		constraint bool_clause([b1, b2], []);      % b1 \/ b2
 		constraint bool_clause_imp([b3], [y], b1); % b1 -> (y -> b3)
 		constraint f_imp(x, b3);                   % b3 -> f(x)
-		constraint int_ne_imp(x, 5, b4);           % b4 -> x != 5
+		constraint int_ne_imp(x, 5, b2);           % b2 -> x != 5
 	\end{mzn}
 
 	We are able to replace the two \glspl{reif} and push the negation inwards, transforming the equals \constraint{} into a not equals \constraint{}.
···
 	If the Boolean \mzninline{y} was not further \constraint{} in the problem, then we could further reduce it to the following \constraints{}.
 
 	\begin{mzn}
-		constraint bool_clause([y, b2], []);       % y \/ b2
-		constraint f_imp(x, y);                   % b3 -> f(x)
-		constraint int_ne_imp(x, 5, b4);           % b4 -> x != 5
+		constraint bool_clause([y, b2], []); % y \/ b2
+		constraint f_imp(x, y);              % y -> f(x)
+		constraint int_ne_imp(x, 5, b2);     % b2 -> x != 5
 	\end{mzn}
 
 \end{example}
···
 The \gls{rewriting} with \gls{half-reif} also interacts with some of the optimisation methods used during the \gls{rewriting} process.
 Most importantly, \gls{half-reif} has to be considered when using \gls{cse} and \gls{propagation} can change the context of expression.
 In \cref{subsec:half-cse} we will discuss how \gls{cse} can be adjusted to handle \gls{half-reif}.
-Finally, in \cref{subsec:half-dyn-context} we will discuss how the context in which a expression is executed can be adjusted during the \gls{rewriting} process.
+Finally, in \cref{subsec:half-dyn-context} we will discuss how the context in which an expression is executed can be adjusted during the \gls{rewriting} process.
 
 \subsection{Chain compression}%
 \label{subsec:half-compress}
···
 The case shown in the example can be generalised to
 
 \begin{mzn}
-	b1 -> b2 /\ forall(i in N)(b2 -> c[i])
+	constraint b1 -> b2 /\ forall(i in N)(b2 -> c[i])
 \end{mzn}
 
 \noindent{}which, if \texttt{b2} has no other usage in the instance, can be resolved to
 
 \begin{mzn}
-	forall(i in N)(b1 -> c[i])
+	constraint forall(i in N)(b1 -> c[i])
 \end{mzn}
 
 \noindent{}after which \texttt{b2} can be removed from the model.
···
 These can be split up into multiple implications.
 
 \begin{mzn}
-	b -> forall(x in N)(x)
+	constraint b -> forall(x in N)(x)
 \end{mzn}
 
 The expression above is logically equivalent to the following expression.
 
 \begin{mzn}
-	forall(x in N)(b -> x)
+	constraint forall(x in N)(b -> x)
 \end{mzn}
 
 Adopting this transformation both simplifies a complicated \constraint{} and possibly allows for the further compression of \glspl{implication-chain}.
 It should however be noted that although this transformation can increase the number of \constraints{} in the \gls{slv-mod}, it generally increases the \gls{propagation} efficiency.
 
-To adjust the algorithm to simplify implied conjunctions more introspection from the \minizinc{} \compiler{} is required.
+To adjust the algorithm to simplify implied conjunctions, more introspection from the \minizinc{} \compiler{} is required.
 The \compiler{} must be able to tell if a \variable{} is (only) a \gls{cvar} of a reified conjunction and what the elements of that conjunction are.
-In the case where a \variable{} has one incoming edge, but it is marked as used in other \constraint{}, we can now check if it is only a \gls{cvar} for a \gls{reified} conjunction and perform the transformation in this case.
+In the case where a \variable{} has one incoming edge, but it is marked as used in another \constraint{}, we can now check if it is only a \gls{cvar} for a \gls{reified} conjunction and perform the transformation in this case.
 
 \subsection{Common Sub-expression Elimination}%
 \label{subsec:half-cse}
···
 The dependency tracking through the use of \constraints{} attached to \variables{} ensures no defining \constraints are left in the model.
 This ensures that all \variables{} and \constraints{} created the earlier version are correctly removed.
 
-Because the expression itself is changed when a negation is moved inwards, it may not always be clear when the same expression is used in both \posc{} and negc{} context.
+Because the expression itself is changed when a negation is moved inwards, it may not always be clear when the same expression is used in both \posc{} and \negc{} context.
 This problem is solved by introducing a canonical form for expressions where negations can be pushed inwards.
 In this form the result of \gls{rewriting} an expression and its negation are collected in the same place within the \gls{cse} table.
 If it is found that for an expression that is about to be \gls{half-reified} there already exists an \gls{half-reif} for its negation, then we instead evaluate the expression in \mixc{} context.
···
 	When its expression is negated, pushing the negation inwards will result in a \mzninline{!=} operator, a \mzninline{int_ne} call.
 	The opposite happens when a negation is pushed inwards for an expression using \mzninline{!=} operator.
 	So to ensure that a \negc{} occurrence of \mzninline{int_eq} and a \posc{} occurrence of \mzninline{int_ne} use the same \gls{cvar} they are both mapped to \mzninline{int_eq} in the \gls{cse} table.
-	The mapping ensures that the context is correctly transformed when accessing the \gls{cse} table for a \mzninline{int_ne} call.
+	The mapping ensures that the context is correctly transformed when accessing the \gls{cse} table for an \mzninline{int_ne} call.
 
 \end{example}
 
···
 		constraint b -> (2*x = y);
 	\end{mzn}
 
-	Since the \domain{} of \mzninline{x} is strictly smaller than the \domain{} of \mzninline{y}, \gls{propagation} of \mzninline{b} will set it to the value \mzninline{true}.
+	Since the values in the \domain{} of \mzninline{x} are strictly smaller than the values in the \domain{} of \mzninline{y}, \gls{propagation} of \mzninline{b} will set it to the value \mzninline{true}.
 	This however means that the \constraint{} is equivalent to the following \constraint{}.
 
 	\begin{mzn}
···
 \end{example}
 
 The situation shown in the example is the most common change of context.
-If the control \variable{} of a \gls{reif} is fixed, the context often changes to either \rootc{} or a negated \rootc{} context.
+If the \gls{cvar} of a \gls{reif} is fixed, the context often changes to either \rootc{} or a negated \rootc{} context.
 If, on the other hand, the \gls{cvar} of a \gls{half-reif} is fixed, then either the context becomes \rootc{} or the \constraint{} already holds.
 Since direct \constraints{} are strongly preferred over any form of \gls{reif}, it is important to dynamically pick the correct form during the \gls{rewriting} process.
 
 This problem can be solved by the \compiler{}.
 For each \gls{reif} and \gls{half-reif} the \compiler{} introduces another layer of \gls{decomp}.
 In this layer, it checks its \gls{cvar}.
-If the control \variable{} is already fixed, then it rewrites itself into its form in another context.
+If the \gls{cvar} is already fixed, then it rewrites itself into its form in another context.
 Otherwise, it behaves as it would have done normally.
 The \gls{cvar} is thus used to communicate the change in context.
 
···
 
 	Let's assume the \compiler{} finds a call to \mzninline{int_lin_le} in \posc{} context.
 	Instead of outputting the call to \mzninline{int_lin_le_imp} directly, it will instead output a call to \mzninline{_int_lin_le_imp}.
-	This predicate is then generated as follows:
+	This predicate is then generated as shown in \cref{lst:half-check-reif}.
+	This new predicate (calls) can then be rewritten normally.
 
-	\begin{mzn}
-		predicate _int_lin_le_imp(
-			array[int] of int: c,
-			array[int] of var int: x,
-			int: d,
-			var bool: b
-		) =
-			if is_fixed(b) then
-				if fix(b) then
-					int_lin_le(c, x, d)
-				else
-					true
-				endif
-			else
-				int_lin_le_reif(c, x, d, b)
-			endif;
-	\end{mzn}
+	\begin{listing}
+		\mznfile{assets/listing/half_reif_check.mzn}
+		\caption{\label{lst:half-check-reif}A generated predicate for \mzninline{int_lin_le_imp} that checks its \gls{cvar} to ensure a \gls{half-reif} is still required.}
+	\end{listing}
 
-	This new predicate can then be compiled using the normal methods.
 \end{example}
 
 \section{Experiments}
···
 Since \gls{chuffed} is a \gls{lcg} \solver{}, the explanations created by the \gls{propagator} have to be adjusted as well.
 These adjustments happen in a similar fashion to the adjustments of the general algorithm: explanations used for the violation of the \constraint{} can now be used to set the \gls{cvar} to \mzninline{false} and the explanations given to prune a variable are appended by requirement that the \gls{cvar} is \mzninline{true}.
 
-In our second configuration the \mzninline{all_different} \constraint{} is enforced using the following \gls{decomp}.
-
-\begin{mzn}
-	predicate all_different(array[int] of var int: x) =
-		forall(i,j in index_set(x) where i < j)(
-			x[i] != x[j]
-		);
-\end{mzn}
-
+In our second configuration the \mzninline{all_different} \constraint{} is enforced using the \gls{decomp} shown in \cref{lst:half-alldiff}.
 The \mzninline{!=} \constraints{} produced by this redefinition are \gls{reified}.
 Their conjunction, then represent the \gls{reif} of the \mzninline{all_different} \constraint{}.
+
+\begin{listing}
+	\mznfile{assets/listing/half_alldiff.mzn}
+	\caption{\label{lst:half-alldiff}The standard \gls{decomp} for \mzninline{all_different} in the \minizinc{} standard library.}
+\end{listing}
+
 
 \begin{table}
 	\begin{center}
···
 However, we can imagine that the removed \constraints{} in some cases help the \gls{mip} solver.
 An important technique used by \gls{mip} solvers is to detect certain pattern, such as cliques, during the pre-processing of the \gls{mip} instance.
 Some patterns can only be detected when using a full \gls{reif}.
-Furthermore, the performance of \gls{mip} solvers is often dependent on the order and form in which the \constraints{} are given \autocite{fischetti-2014-erratiscism}.
+Furthermore, the performance of \gls{mip} solvers is often dependent on the order and form in which the \constraints{} are given \autocite{lodi-2013-variability,fischetti-2014-erratiscism}.
 With the usage of the \gls{aggregation} and \gls{del-rew}, these can be exceedingly different when using \gls{half-reif}.
 
 The solving statistics for \gls{openwbo} might be most positive.

chapters/4_half_reif_preamble.tex

···
 \noindent{}Whether a \constraint{} has to be \gls{reified} is a crucial decision made during \gls{rewriting}.
 \minizinc{} allows us to write complex \constraints{} that in the process of \gls{rewriting} result in multiple \constraints{} that reason about each other.
-However, determining whether a \constraint{} holds, \(\texttt{b} \leftrightarrow{} c\), requires significantly more effort from the \solver{} than merely enforcing the \constraint{} \(c\).
+However, determining whether a \constraint{} holds, \(b \leftrightarrow{} c\), requires significantly more effort from the \solver{} than merely enforcing the \constraint{} \(c\).
 A \gls{reified} \constraint{} results in a larger \gls{decomp} or a more complex \gls{native} \constraint{}.
 It it thus important that \gls{rewriting} avoids the use of \gls{reif}, whenever it is not required.
  
 In this chapter we present an extended \gls{reif} analysis to help minimise the required \solver{} effort.
 Not only does it consider if a \constraint{} must be \gls{reified} or not, but it also considers whether it could instead be \gls{half-reified}.
 
-The notion of \gls{half-reif} \(\texttt{b} \rightarrow{} c\) for a \constraint{} \(c\) was introduced by \textcite{feydy-2011-half-reif}.
-It is shown \gls{half-reif} can relief some of the problems and expenses of the use of \gls{reif}.
+The notion of \gls{half-reif} \(b \rightarrow{} c\) for a \constraint{} \(c\) was introduced by \textcite{feydy-2011-half-reif}.
+It is shown \gls{half-reif} can relieve some of the problems and expenses of the use of \gls{reif}.
 It is not always possible, however, to use a \gls{half-reif} instead of a \gls{reif}.
 The authors identify the conditions required for its usage and provide an algorithm that rewrites a subset of the \minizinc{} language using the technique.
 Crucially, because of the omission of \gls{let} and multiple occurrences of identifiers, this algorithm does not directly generalise to the full \minizinc{} language.