Attempt at remaining feedback

.vscode/ltex.hiddenFalsePositives.en-GB.txt

@@ -375,3 +375,10 @@
 {"rule":"WANT","sentence":"^\\QI especially want to thank Caitlin for her love and support even when\\E$"}
 {"rule":"WANT","sentence":"^\\QFinally, I would like to thank my friends and family who have kept me sane for the last four years: my mother, Saskia, was always there to support me; my father, Marco, and Natalja always helped me look forward to the future; my siblings, Bram, Guus, and Layla, my friends abroad, Dries, Johan, Mats, and Manon I especially want to thank Caitlin for her love and support when I needed it most.\\E$"}
 {"rule":"WANT","sentence":"^\\QI especially want to thank Caitlin for her love and support when I needed it most.\\E$"}
+{"rule":"WANT","sentence":"^\\QAbove all, I want to thank Caitlin for her love and support when I needed it most.\\E$"}
+{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QAs an input to the inference process, an “argCtx” function is used to give the context of the arguments of a function, given the function itself and the context of the call.\\E$"}
+{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QNote that the translation introduces a special root_ctx decision variable to abide by the MicroZinc syntax.\\E$"}
+{"rule":"THREE_NN","sentence":"^\\QAlthough pure \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q behaves the same under any call evaluation strategy, in implementation a call by value strategy can provide more predictable behaviour with debugging functions in the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q language.\\E$"}
+{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe function [fontsize=]minizinc set2bool is used to transform the set decision variable into an array of Boolean variables that represent whether an element is present in the set.\\E$"}
+{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q graph \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where chained implications have been removed.\\E$"}
+{"rule":"EN_A_VS_AN","sentence":"^\\QAn expression \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q can be \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q when every to the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is also a if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is replaced by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}

.vscode/settings.json

@@ -8,7 +8,7 @@
         "\\solvers{}": "pluralDummy",
         "\\prbpars{}": "pluralDummy",
         "\\prbpar{}": "dummy",
-        "\\instance{}": "dummy",
+        "\\instance{}": "vowelDummy",
         "\\instances{}": "pluralDummy",
         "\\constraints{}": "pluralDummy",
         "\\constraint{}": "dummy",
@@ -75,7 +75,9 @@
         "\\plainfile{}": "ignore",
         "\\amplfile{}": "ignore",
         "\\true{}": "dummy",
-        "\\false{}": "dummy"
+        "\\false{}": "dummy",
+        "\\solutions{}": "pluralDummy",
+        "\\solution{}": "dummy"
     },
     "ltex.latex.environments": {
         "mzn": "ignore",

assets/bibliography/references.bib

@@ -427,6 +427,22 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org},
 }
 
+@article{ford-2004-column,
+  author    = {Ford, Jr., Lester Randolph and
+               Fulkerson, Delbert Ray},
+  title     = {A Suggested Computation for Maximal Multi-Commodity Network Flows},
+  journal   = {Manag. Sci.},
+  volume    = {50},
+  number    = {12-Supplement},
+  pages     = {1778--1780},
+  year      = {2004},
+  url       = {https://doi.org/10.1287/mnsc.1040.0269},
+  doi       = {10.1287/mnsc.1040.0269},
+  timestamp = {Tue, 30 Jun 2020 11:40:56 +0200},
+  biburl    = {https://dblp.org/rec/journals/mansci/FordF04.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{fourer-2002-amplcp,
 	author = {Robert Fourer and David M. Gay},
 	title = {Extending an Algebraic Modeling Language to Support Constraint
@@ -498,6 +514,18 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org},
 }
 
+@article{fruhwirth-1998-chr,
+	author = {Thom W. Fr{\"{u}}hwirth},
+	title = {Theory and Practice of Constraint Handling Rules},
+	journal = {The Journal of Logic Programming},
+	volume = 37,
+	number = {1-3},
+	pages = {95--138},
+	year = 1998,
+	url = {https://doi.org/10.1016/S0743-1066(98)10005-5},
+	doi = {10.1016/S0743-1066(98)10005-5},
+}
+
 @techreport{gamrath-2020-scip,
 	author = {Gerald Gamrath and Daniel Anderson and Ksenia Bestuzheva and Wei-Kun
 	          Chen and Leon Eifler and Maxime Gasse and Patrick Gemander and Ambros
@@ -517,18 +545,6 @@
 	url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-78023},
 }
 
-@article{fruhwirth-1998-chr,
-	author = {Thom W. Fr{\"{u}}hwirth},
-	title = {Theory and Practice of Constraint Handling Rules},
-	journal = {The Journal of Logic Programming},
-	volume = 37,
-	number = {1-3},
-	pages = {95--138},
-	year = 1998,
-	url = {https://doi.org/10.1016/S0743-1066(98)10005-5},
-	doi = {10.1016/S0743-1066(98)10005-5},
-}
-
 @article{gebser-2012-clasp,
 	author = {Martin Gebser and Benjamin Kaufmann and Torsten Schaub},
 	title = {Conflict-driven answer set solving: From theory to practice},
@@ -574,6 +590,19 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org},
 }
 
+@article{hooker-2003-lbbd,
+	title={Logic-based Benders decomposition},
+	author={Hooker, John N and Ottosson, Greger},
+	journal={Mathematical Programming},
+	volume={96},
+	number={1},
+	pages={33--60},
+	year={2003},
+	publisher={Springer},
+	url = {https://doi.org/10.1007/s10107-003-0375-9},
+	doi = {10.1007/s10107-003-0375-9},
+}
+
 @manual{ibm-2017-opl,
 	title = {OPL Language User’s Manual},
 	author = {CPLEX, IBM ILOG},
@@ -875,15 +904,6 @@
 	version = {2.5.5},
 }
 
-@book{michel-2005-comet,
-	author = {Van Hentenryck, Pascal and Michel, Laurent},
-	title = {Constraint-Based Local Search},
-	year = {2005},
-	isbn = {0262220776},
-	publisher = {The MIT Press},
-	url = {https://mitpress.mit.edu/books/constraint-based-local-search},
-}
-
 @article{nightingale-2017-ess-prime,
 	author = {Peter Nightingale and {\"{O}}zg{\"{u}}r Akg{\"{u}}n and Ian P. Gent
 	          and Christopher Jefferson and Ian Miguel and Patrick Spracklen},
@@ -1257,6 +1277,28 @@
 	publisher = {MIT Press},
 }
 
+@inproceedings{van-hentenryck-1999-oplscript,
+  author    = {Pascal Van Hentenryck and
+               Laurent Michel},
+  editor    = {Krzysztof R. Apt and
+               Antonis C. Kakas and
+               {\'{E}}ric Monfroy and
+               Francesca Rossi},
+  title     = {{OPL} Script: Composing and Controlling Models},
+  booktitle = {New Trends in Contraints, Joint ERCIM/Compulog Net Workshop, Paphos,
+               Cyprus, October 25-27, 1999, Selected Papers},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {1865},
+  pages     = {75--90},
+  publisher = {Springer},
+  year      = {1999},
+  url       = {https://doi.org/10.1007/3-540-44654-0_4},
+  doi       = {10.1007/3-540-44654-0_4},
+  timestamp = {Tue, 23 Feb 2021 09:09:50 +0100},
+  biburl    = {https://dblp.org/rec/conf/compulog/HentenryckM99.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{van-hentenryck-2000-opl-search,
 	author = {Van Hentenryck, Pascal and Perron, Laurent and Puget, Jean-Fran\c{c}
 	          ois},
@@ -1278,6 +1320,15 @@
 	            optimization},
 }
 
+@book{van-hentenryck-2005-comet,
+	author = {Van Hentenryck, Pascal and Michel, Laurent},
+	title = {Constraint-Based Local Search},
+	year = {2005},
+	isbn = {0262220776},
+	publisher = {The MIT Press},
+	url = {https://mitpress.mit.edu/books/constraint-based-local-search},
+}
+
 @inproceedings{hentenryck-2013-objcp,
 	author = {Van Hentenryck, Pascal and Michel, Laurent},
 	title = {The Objective-CP Optimization System},

assets/glossary.tex

@@ -197,7 +197,7 @@
 
 \newglossaryentry{comet}{
   name={COMET},
-  description={A \cml{} with advanced \gls{meta-optimization} functionality \autocite{michel-2005-comet}.}
+  description={A \cml{} with advanced \gls{meta-optimization} functionality \autocite{van-hentenryck-2005-comet}.}
 }
 
 \newglossaryentry{compiler}{

assets/listing/rew_pigeon_uzn.mzn

@@ -8,9 +8,8 @@ function var bool: all_different(array[int] of var int: x) =
 			where int_lt(i,j)
 	]);
 
-function var bool: main(int: n) =
+function bool: main(int: n) =
 	let {
-		var bool: root_ctx;
 		array[1..n] of var 1..n-1: pigeon;
 		constraint all_different(pigeon);
-	} in root_ctx;
+	} in true;

assets/shorthands.tex

@@ -61,3 +61,6 @@
 \newcommand*{\ctxeval}[2]{\ensuremath{\mathbb{M}\left(#2\right)\left\|~#1~\right\|}}
 \newcommand*{\ctxfunc}[2]{\ensuremath{\mathbb{F}\left(#2\right)\left\|~#1~\right\|}}
 \newcommand*{\ctxitem}[1]{\ensuremath{\mathbb{m}\left\|~#1~\right\|}}
+
+% Spacing issues
+\newcommand*{\codeendsexample}{\vspace{-2.3em}}

chapters/2_background.tex

@@ -288,8 +288,9 @@ Note that using this \gls{global} as follows would have simplified the \minizinc
 
 \begin{mzn}
 	var 0..total_space: space_used;
-	constraint knapsack(toy_space, toy_joy, set2bool(selection), space_used, total_joy);
+	constraint knapsack(toy_space, toy_joy, set2bool(selection)@\footnotemark{}@, space_used, total_joy);
 \end{mzn}
+\footnotetext{The function \mintinline[fontsize=\scriptsize]{minizinc}{set2bool} is used to transform the set \variable{} into an array of Boolean variables that represent whether an element is present in the set.}
 
 \noindent{}This has the additional benefit that the knapsack structure of the problem is then known.
 The \constraint{} can be rewritten using a specialized \gls{decomp} provided by the \solver{}, or it can be marked as a \gls{native} \constraint{}.

chapters/3_rewriting.tex

@@ -72,7 +72,7 @@ The core of the syntax of \microzinc{} is defined in \cref{fig:rew-uzn-syntax}.
 Function declarations without an expression body are used to mark functions that are \gls{native} to the target \solver{}.
 We have omitted the definitions of \syntax{<mzn-type-inst>} and \syntax{<ident>}, which can be assumed to be the same as the definition of \syntax{<type-inst>} and \syntax{<ident>} in the \minizinc{} grammar, see \cref{ch:minizinc-grammar}.
 While we omit the typing rules here for space reasons, we will assume that in well-typed \microzinc{} programs conditions of expressions are \parameters{}.
-This means that the where conditions \syntax{<exp>} in \glspl{comprehension}, the conditions \syntax{<exp>} in \gls{conditional} expressions, and the \syntax{<literal>} index in \gls{array} accesses must have \mzninline{par} type.
+This means that the where conditions \syntax{<exp>} in \glspl{comprehension}, the conditions \syntax{<exp>} in \gls{conditional} expressions, and the \syntax{<literal>} index in \gls{array} accesses must have parametric type.
 In \minizinc{} the use of \variables{} in these positions is allowed, and these expressions are rewritten to function calls.
 We will discuss how the same transformation takes place when translating \minizinc{} to \microzinc{}.
 
@@ -136,21 +136,11 @@ The translation from \minizinc{} to \microzinc{} involves the following steps.
 		This includes simple cases such as replacing \gls{operator} expressions, like \mzninline{x+y}, by function calls, \mzninline{int_plus(x,y)}, and replacing generators in calls, like \mzninline{sum(x in A)(x)}, by \glspl{comprehension}, \mzninline{sum([x|x in A])}.
 		As mentioned above, \gls{conditional} expressions where the decision is made by a \variable{} are also not directly supported in \microzinc{}.
 		These expressions are therefore also replaced by function calls that are possibly decomposed.
-		An expression \mzninline{if x then A else B endif}, where \mzninline{x} is a \variable{}, is replaced the following call.
+		An expression \mzninline{if x then A else B endif}, where \mzninline{x} is a \variable{}, is replaced the call \mzninline{if_then_else([x, true], [A, B])}. 
-		
+		A recent study by \textcite{stuckey-2019-conditionals} describes how \mzninline{if_then_else} can be decomposed for different types of \solvers{}.
-		\begin{mzn}
+		An expression \mzninline{A[x]}, where \mzninline{x} is a \variable{}, is replaced by the call \mzninline{element(A, x)}.
-			if_then_else([x, true], [A, B])
-		\end{mzn}
-
-		An expression \mzninline{A[x]}, where \mzninline{x} is a \variable{}, is replaced by the following call.
-
-		\begin{mzn}
-			element(A, x)
-		\end{mzn}
-
 		\mzninline{element} is a well-known \gls{global}.
 		For many \gls{cp} \solvers{} it is a \gls{native} \constraint{} and for other \solvers{} there have long been accepted \glspl{decomp}.
-		A recent study by \textcite{stuckey-2019-conditionals} describes how \mzninline{if_then_else} can be decomposed for different types of \solvers{}.
 
 	\item Replace optional \variables{} into non-optional forms.
 		As shown by \textcite{mears-2014-option}, optional type \variables{} can be represented using a \variable{} of the same non-optional type and a Boolean \variable{}.
@@ -190,11 +180,11 @@ The translation from \minizinc{} to \microzinc{} involves the following steps.
 
 		\begin{mzn}
 			let {
-				(var int: res, var bool: total) = element(e, v);
+				(var int: res, var bool: total) = element_safe(e, v);
 			} in (total /\ res = 5) \/ b;
 		\end{mzn}
 
-	\item Resolve sub-type based overloading statically.
+	\item Resolve subtype based overloading statically.
 		To prevent the runtime overhead of the dynamic lookup of overloaded function definitions for every call, the function dispatch in \microzinc{} is determined statically.
 
 		It is important, however, that the correct version of a function is chosen when it allows for either \variable{} and \parameter{} arguments.
@@ -226,27 +216,29 @@ The translation from \minizinc{} to \microzinc{} involves the following steps.
 	Consider the \minizinc{} model in \cref{lst:rew-pigeon-mzn}.
 	It describes a simple \gls{unsat} ``pigeonhole problem'': trying to assign \(n\) pigeons to \(n-1\) holes.
 
-		\begin{listing}
-			\mznfile{assets/listing/rew_pigeon_mzn.mzn}
-			\caption{\label{lst:rew-pigeon-mzn} A \minizinc{} model of the pigeonhole problem.}
-		\end{listing}
-
 	The translation to \microzinc{} turns all expressions into function calls, replaces the special generator syntax in the \mzninline{forall} with an \gls{array} \gls{comprehension}, and creates the \mzninline{main} function.
 	The result of this translation is shown in \cref{lst:rew-pigeon-uzn}.
 
-	\begin{listing}
-		\mznfile{assets/listing/rew_pigeon_uzn.mzn}
-		\caption{\label{lst:rew-pigeon-uzn} The \microzinc{} translation of the pigeonhole problem in \cref{lst:rew-pigeon-mzn}.}
-	\end{listing}
-
 	For an \instance{} of the \cmodel{}, we can then create a simple \nanozinc{} program that calls \mzninline{main}.
 	For example for \(n=10\), we would create the following \nanozinc{} program.
 
 	\begin{nzn}
 		constraint main(10);
 	\end{nzn}
+	\codeendsexample{}
 \end{example}
 
+\begin{listing}[ht]
+	\mznfile{assets/listing/rew_pigeon_mzn.mzn}
+	\caption{\label{lst:rew-pigeon-mzn} A \minizinc{} model of the pigeonhole problem.}
+\end{listing}
+
+
+\begin{listing}[ht]
+	\mznfile{assets/listing/rew_pigeon_uzn.mzn}
+	\caption{\label{lst:rew-pigeon-uzn} The \microzinc{} translation of the pigeonhole problem in \cref{lst:rew-pigeon-mzn}.}
+\end{listing}
+
 \subsection{Partial Evaluation of \glsentrytext{nanozinc}}\label{sub:rew-partial}
 
 Each call in a \nanozinc{} program is either a call to a \gls{native} \constraint{}, or it has a corresponding \microzinc{} function definition.
@@ -284,6 +276,7 @@ A \nanozinc{} program (\cref{fig:rew-nzn-syntax}) consists of a topologically-or
 \Constraints{} can also occur at the top-level of the \nanozinc{} program.
 These are said to be the \rootc{}-context \constraints{} of the \cmodel{}, i.e., those that have to hold globally and are not just used to define an \gls{avar}.
 Only root-context \constraints{} can effectively constrain the overall problem.
+In \microzinc{} these \constraints{} must originate from \constraint{} items in the generated \mzninline{main} function.
 \Constraints{} attached to \variables{} originate from function calls, and since all functions are guaranteed to be total, attached \constraints{} can only define the function result.
 
 \begin{example}\label{ex:rew-absnzn}
@@ -317,7 +310,8 @@ The full set of rules appears in \cref{fig:rew-rewrite-to-nzn-calls,fig:rew-rewr
 To simplify presentation, we assume that all rules that introduce new identifiers into the \nanozinc{} program do so in a way that ensures those identifiers are fresh (i.e., not used in the rest of the \nanozinc{} program), by suitable alpha renaming.
 We also present our rules using a \emph{call by name} evaluation strategy, i.e., the arguments to function calls are substituted into function body.
 As such, they are only evaluated when required for the result of the function.
-Although pure \microzinc{} behaves the same under any call evaluation strategy, in implementation a \emph{call by value} strategy can provide more predictable behaviour with debugging functions in the \minizinc{} language, such as \mzninline{trace} and \mzninline{assert}.
+Although pure \microzinc{} behaves the same under any call evaluation strategy, in implementation a \emph{call by value} strategy can provide more predictable behaviour with debugging functions in the \minizinc{} language.
+It would likely be unexpected that functions such as \mzninline{trace} and \mzninline{assert} are only evaluated if and when their values are required (call by name), instead of when the function call is encountered.
 
 \begin{figure*}[p]
 	\centering
@@ -545,7 +539,7 @@ The \constraints{} directly succeeding the declaration prepended by \texttt{↳}
 
 	We assume here that \mzninline{c}, \mzninline{x} and \mzninline{y} are used in other parts of the model not shown here and therefore not removed.
 	Note how it is crucial to exclude the attached \constraints{} when counting the usage of \variables{}.
-	\mzninline{int_abs(x, z)}, the \constraint{}  which merely defines \mzninline{z}, would otherwise force us to keep \mzninline{z} in the \nanozinc{} program, if it were included in the count.
+	\mzninline{int_abs(x, z)}, the \constraint{}  which merely defines \mzninline{z}, would otherwise require us to keep \mzninline{z} in the \nanozinc{} program, if it were included in the count.
 \end{example}
 
 It is important to notice the difference between \constraints{} that appear at the top level and \constraints{} that appear as part of the attached \constraints{} of a \variable{}.
@@ -573,7 +567,7 @@ In this thesis we will follow the same naming standard as \minizinc{}, where a \
 	All other \variables{} can thus be removed, and the model will stay \gls{eqsat}.
 
 	In the \nanozinc{} version of this model, each of the multiplications \constraints{} will be added to the list of attached \constraints{} of its corresponding \mzninline{y} \variable{}.
-	When, after evaluating the \gls{array} access, all of those \variables{} except the last are detected to be unused, their removal triggers the removal of the subtraction \constraints{}.
+	When, after evaluating the \gls{array} access, all of those \variables{} except the last are detected to be unused, their removal triggers the removal of the multiplication \constraints{}.
 
 	For this example the current \minizinc{} compiler, version 2.5.5, will produce a \gls{slv-mod} that contains:
 
@@ -583,7 +577,7 @@ In this thesis we will follow the same naming standard as \minizinc{}, where a \
 		\item \mzninline{n-1} multiplication \constraints{}.
 	\end{itemize}
 	
-	\noindent{}This is despite the fact that the \domain{} of the \variable{} \mzninline{x} has already been \gls{fixed} to 10\@.
+	\noindent{}It creates the definitions for \mzninline{y} despite the fact that the \domain{} of the \variable{} \mzninline{x} has already been \gls{fixed} to 1\@.
 	The \nanozinc{} system can correctly detect that the \mzninline{y} \variables{} and multiplication \constraints{} are not required.
 \end{example}
 
@@ -679,6 +673,42 @@ This crucial optimization enables rewriting in multiple phases.
 For example, a \cmodel{} targeted at a \gls{mip} \solver{} is rewritten into Boolean and reified \constraints{}, whose definitions are annotated to be delayed.
 The \nanozinc{} program can then be fully simplified by \gls{propagation}, before the Boolean and reified \constraints{} are rewritten into \gls{native} linear \constraints{} suitable for \gls{mip}.
 
+\begin{example}
+
+	Let us revisit the example from \cref{subsec:back-delayed-rew}.
+	The following \minizinc{} fragment calls a predicate that uses the ``Big M method''.
+	
+	\begin{mzn}
+		function var int: lq_zero_if_b(var int: x, var bool: b) ::delayed =
+			x <= ub(x)*(1-b); % b -> x<=0
+
+		var 0..1000: x;
+		var bool: b;
+		constraint lq_zero_if_b(x, b);
+		constraint x <= 10;
+	\end{mzn}
+
+	If this fragment is processed without the \gls{del-rew}, then it will result in the following \nanozinc{}.
+
+	\begin{nzn}
+		var 0..100: x;
+		var bool: b;
+		constraint int_lin_le([1, 1000], [x,b], 1000);
+	\end{nzn}
+
+	Note, however, that if \mzninline{ub(x)} was known to be 100, then a stronger constraint could have been used.
+	When using \gls{del-rew}, the interpreter will instead first produce the following \nanozinc{}.
+
+	\begin{nzn}
+		var 0..100: x;
+		var bool: b;
+		constraint lq_zero_if_b(x, b);
+	\end{nzn}
+
+	Because the evaluation of \mzninline{lq_zero_if_b} is delayed until after the domain changes of \mzninline{x} it can instead produce \mzninline{int_lin_le([1, 100], [x,b], 100)}.
+
+\end{example}
+
 \subsection{Common Sub-expression Elimination}%
 \label{sec:rew-cse}
 
@@ -706,6 +736,7 @@ Earlier in the process, however, the \minizinc{} to \microzinc{} \compiler{} can
 		constraint let { var int: y = abs(x) } in
 			(y*2 >= 20) \/ (y+5 >= 15)
 	\end{mzn}
+	\codeendsexample{}
 \end{example}
 
 As such, the \compiler{} can enforce sharing of common sub-expressions before evaluation begins.
@@ -775,6 +806,7 @@ When the \gls{avar} become unused, they will be removed using the normal mechani
 	\begin{mzn}
 		constraint int_lin_le([1,2,-1], [x,y,z], 0)
 	\end{mzn}
+	\codeendsexample{}
 \end{example}
 
 \section{Experiments}\label{sec:rew-experiments}

chapters/4_half_reif.tex

@@ -25,7 +25,7 @@ The \gls{rewriting} process then enforces a \constraint{} \mzninline{pred_reif(.
 \end{itemize}
 
 As an alternative, the authors introduce \gls{half-reif}.
-It follows from the idea that in many cases it is sufficient to use the logical implication of an expression, \mzninline{b -> pred(...)}, instead of the logical equivalence, \mzninline{b <-> pred(...)}.
+It follows from the idea that in many cases it is \gls{eqsat} to use the logical implication of an expression, \mzninline{b -> pred(...)}, instead of the logical equivalence, \mzninline{b <-> pred(...)}.
 \Gls{rewriting} with \gls{half-reif} is an approach that improves upon these weaknesses of \gls{rewriting} with ``full'' \gls{reif}.
 
 \begin{itemize}
@@ -36,21 +36,23 @@ It follows from the idea that in many cases it is sufficient to use the logical
 Additionally, for many \solvers{} the \gls{decomp} of a \gls{reif} is more complex than the \gls{decomp} of a \gls{half-reif}.
 We will show that using \glspl{half-reif} can therefore lead to a reduction in \gls{native} \constraints{} in the \gls{slv-mod}.
 
-\Gls{half-reif} can be used instead of full \gls{reif} when the resulting \gls{cvar} can never be forced to be \false{}.
+A Boolean expression \(e\) can be \gls{half-reified} when every \gls{sol} to the \instance{} in which it is located is also a \gls{sol} for the \instance{} in which \(e\) is replaced by \true{}.
 This requirement follows from the difference between implication and logical equivalence.
-Setting the left-hand side of an implication to \false{} does not influence the value on the right-hand side.
+When the left-hand side of an implication \(b \implies{} e\) is \false{}, it does not influence the value on the right-hand side.
-This is why the \gls{cvar} should never be forced to be \false{}, since this would not enforce the negation of the \constraint{}.
+Therefore, it can be used in these cases as it is guaranteed that if \(e\) represented by a new Boolean \variable{} \(b\), then it is never implied that \(b = \false\). 
-Setting the right-hand side of an implication to \true{} also does not influence the left-hand side.
+Note that when the right-hand side of an implication \(b \implies{} e\) is \true{}, it also does not influence the left-hand side.
-This is, however, not an issue since in this case the value can just be assigned by the \gls{propagation} of other \constraints{} or a \gls{search-decision}.
+A possible downside of \gls{half-reif} is thus that its \gls{cvar} might need to be assigned by a \gls{search-decision}.
 
 \begin{example}
+\label{ex:hr-disjunction}
+
 	For example, \gls{half-reif} can be used in the following disjunction.
 
 	\begin{mzn}
 		constraint (x = 5) \/ (y = 5);
 	\end{mzn}
 
-	This \constraint{} forces that, between \mzninline{x} and \mzninline{y}, at least one \variable{} takes the value five.
+	This \constraint{} states that, between \mzninline{x} and \mzninline{y}, at least one \variable{} takes the value five.
 	The usual \gls{rewriting} would result in the following (intermediate) model, using \glspl{reif} for the equalities.
 
 	\begin{mzn}
@@ -61,8 +63,8 @@ This is, however, not an issue since in this case the value can just be assigned
 		constraint b1 \/ b2;
 	\end{mzn}
 
-	However, independent of the value of \mzninline{b1}, if \mzninline{b2} takes the value \true{}, then it can never make the disjunction \false{}.
+	However, independent of the value of \mzninline{x = 5}, if \mzninline{y = 5} takes the value \true{}, then it can never make the disjunction \false{}.
-	Therefore, \gls{propagation} of the disjunction can never force \mzninline{b1} to take the value \false{}.
+	Therefore, all \glspl{sol} is still a \gls{sol} when \mzninline{y = 5} (or \mzninline{x = 5}) is replaced by \true{}.
 	Consequently, this means using \gls{half-reif} is \gls{eqsat}.
 	\Gls{rewriting} using \gls{half-reif} will result in the following model.
 
@@ -73,6 +75,7 @@ This is, however, not an issue since in this case the value can just be assigned
 		constraint b2 -> (y = 5);
 		constraint b1 \/ b2;
 	\end{mzn}
+	\codeendsexample{}
 \end{example}
 
 This property can be extended to include non-Boolean expressions.
@@ -86,8 +89,8 @@ Since Boolean expressions in \minizinc{} can be used in, for example, integer ex
 	\end{mzn}
 
 	Making the left-hand side of the \constraint{} larger will only ever help satisfy the \constraint{}.
-	This means \gls{propagation} of the expressions \mzninline{x = 5} can never force them to take the value \false{}.
+	This means that all \glspl{sol}  will still be \glspl{sol} if any expression \mzninline{x = 5} is replaced by \true{}.
-	The \gls{rewriting} process can thus use \glspl{half-reif} instead of \glspl{reif} for these expressions.
+	Similar to \cref{ex:hr-disjunction}, the \gls{rewriting} process can thus use \glspl{half-reif} instead of \glspl{reif} for the \mzninline{x = 5} expressions.
 \end{example}
 
 To systematically analyse whether Boolean expressions can be \gls{half-reified}, we study the monotonicity of \constraints{} w.r.t.\@ an expression.
@@ -115,7 +118,7 @@ Therefore, for our analysis, we approximate these definitions.
 We say an expression is in \mixc{} context when it cannot be determined syntactically whether the enclosing \constraint{} is monotone or antitone w.r.t.\@ the expression.
 
 Expressions in \posc{} context are the ones we discussed before.
-A Boolean expression in \posc{} context cannot be forced to be \false{}.
+Any solution to an \instance{} is still a \gls{sol} when a Boolean expression in a \posc{} is replaced by \true{}.
 As such, \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 an expression in a \negc{} context can be \gls{half-reified}.
 
@@ -148,9 +151,9 @@ Only full \gls{reif} can be used for expressions that are in this context.
 		constraint (x = 5) xor (y = 5);
 	\end{mzn}
 	
-	This \constraint{} forces either \mzninline{x} or \mzninline{y}, but not both, to take the value five.
+	This \constraint{} states either \mzninline{x} or \mzninline{y}, but not both, must take the value five.
 	The equalities in this constraint are in \mixc{} context, because whether \mzninline{y} can and must take the value 5 now directly depends on whether \mzninline{x} has already taken the value five, and vice versa.
-	As such, when \mzninline{x} takes the value five it forces \mzninline{y} to not take the value five.
+	Neither when \mzninline{x = 5} nor \mzninline{y = 5} is replaced by \true{} will all \glspl{sol} to the \instance{} remain \glspl{sol}.
 	This means we cannot use a \gls{half-reif}, since it does not enforce the negated \constraint{}.
 \end{example}
 
@@ -173,9 +176,8 @@ Given \(check\), \(prune\), \(entailed\), and \(b\) \cref{alg:half-prop} shows p
 
 \begin{algorithm}[t]
 	
-	\KwIn{The functions \(check\), \(prune\), and \(entailed\) that form the for non-\gls{reified} \gls{propagator} of \constraint{} \(c\) and a Boolean \gls{cvar} \(b\).
+	\KwIn{The functions \(check\), \(prune\), and \(entailed\) that form the for non-\gls{reified} \gls{propagator} of \constraint{} \(c\) and a Boolean \gls{cvar} \(b\).}
-	}
+	\KwResult{This pseudocode propagates the \gls{half-reif} of \(c\) (i.e., \(b \implies\ c\)) and returns to the \solver{} whether the \gls{half-reif} of \(c\) is \gls{violated}, and whether it is entailed.}
-	\KwResult{This pseudocode propagates the \gls{half-reif} of \(c\) (i.e., \(b \implies\ c\)) and returns to the \solver{} whether the \constraint{} is \gls{violated}, and whether it is entailed.}
 
 	\BlankLine{}
 	\If{\(b \text{ is unassigned}\)}{
@@ -196,20 +198,20 @@ Logically, the creation of \glspl{propagator} for \glspl{half-reif} can always f
 In practice, however, this is not always possible.
 In some cases, \glspl{propagator} do not explicitly define \(check\), or \(entailed\) as separate steps, but perform them as part of the pruning process.
 When a \gls{domain} is found to be empty, then the \gls{propagator} declares the current state \gls{unsat}.
-It is not possible to construct the \gls{half-reified} \gls{propagator} from such an implicit \(check\) or \(entailed\) operation.
+It is infeasible to construct the \gls{half-reified} \gls{propagator} from such an implicit \(check\) or \(entailed\) operation.
 Instead, new explicit methods have to be devised to implement the \gls{propagator} of the \gls{half-reif} \constraint{}.
 
 In comparison, a \gls{propagator} for the \gls{reif} of \(c\) cannot be created from these three logical tasks.
 In addition, we require the \(prune\) task from a \gls{propagator} of \(\neg{} c\).
 Using this additional function, we can define an algorithm for the \gls{propagator}, shown in \cref{alg:reif-prop}. Although this seems reasonable for small \constraints{}, such as integer equality, for many \glspl{global} their negation is hard to define.
-For example, the negation of the \mzninline{all_different} \constraint{} is a \constraint{} that forces that at least two values are equal.
+For example, the negation of the \mzninline{all_different} \constraint{} is a \constraint{} that requires that at least two values are equal.
 This is far from a common \constraint{}, and we are not aware of any \solver{} that implements a \gls{propagator} for it.
 
 \begin{algorithm}[t]
 	
 	\KwIn{The functions \(check\), \(prune\), and \(entailed\) that form the for non-\gls{reified} \gls{propagator} of \(c\), the function \(pruneNeg\) that prunes the values of the \constraint{} \(\neg{} c\), and a Boolean \gls{cvar} \(b\).
 	}
-	\KwResult{This pseudocode propagates the \gls{reif} of \(c\) (i.e., \(b \leftrightarrow{} c\)) and returns to the \solver{} whether the \constraint{} is \gls{violated}, and whether it is entailed.}
+	\KwResult{This pseudocode propagates the \gls{reif} of \(c\) (i.e., \(b \leftrightarrow{} c\)) and returns to the \solver{} whether the \gls{reif} of \(c\) is \gls{violated}, and whether it is entailed.}
 
 	\BlankLine{}
 	\If{\(b \text{ is unassigned}\)}{
@@ -244,7 +246,7 @@ For Booleans appearing in \posc{} context we can make the \gls{propagator} of th
 Similarly, in \negc{} context we can make the \gls{propagator} \mzninline{b -> pred(...)} run at the lowest priority.
 This means that the \glspl{cvar} are still \gls{fixed} at the same time, but there is less overhead.
 
-In \cref{sec:half-experiments} we assess the implementation of \glspl{propagator} for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element} based on these principles.
+In \cref{sec:half-experiments} we assess \glspl{propagator} implementations for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element} based on these principles.
 
 \section{Decomposition and Half-Reification}%
 \label{sec:half-decomposition}
@@ -338,7 +340,7 @@ The partiality context is the context in which this condition is placed.
 
 	In this fragment, we study the context of the division expression \mzninline{y div x}.
 	The expression itself return an integer \variable{}, and it is used on the left-hand side of a less than \constraint{}.
-	This result is therefore in a \negc{} context: it is only forced to take a smaller value.
+	This result is therefore in a \negc{} context.
 	This is its value context.
 
 	However, since the \domain{} of \mzninline{x} includes zero, \gls{rewriting} \mzninline{x div y} will introduce the condition under which its result can be used.
@@ -790,7 +792,7 @@ The goal of the algorithm is now to identify and remove vertices that are not ma
 	\KwIn{An implication \constraint{} graph \(G=\tuple{V, E}\) and a set \(M
 	\subseteq{} V\) of vertices used in other \constraints{}.}
 
-	\KwOut{An equisatisfiable graph \(G'=\tuple{V', E'}\) where chained
+	\KwOut{An \gls{eqsat} graph \(G'=\tuple{V', E'}\) where chained
 	implications have been removed.}
 
 	\(V' \longleftarrow V\)\;
@@ -918,6 +920,7 @@ This ensures that all \variables{} and \constraints{} created for the earlier ve
 		↳ constraint int_lin_le([-1, -5], [i, b2], -5);
 		constraint bool_not(k, b2);
 	\end{nzn}
+	\codeendsexample{}
 \end{example}
 
 Since 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.
@@ -1015,8 +1018,7 @@ In each \instance{} certain values have already been \gls{fixed}.
 It is not always possible for all rows and columns to contain only distinct values.
 
 In \minizinc{} counting the number of rows/columns with all different values can be accomplished using a \gls{reified} \mzninline{all_different} \constraint{}.
-Since the goal of the problem is to maximize the number of \mzninline{all_different} \constraints{} that hold, these \constraints{} are never forced to be \false{}.
+Since the goal of the problem is to maximize the number of \mzninline{all_different} \constraints{} that hold, these \constraints{} are in \posc{} context and can be \gls{half-reified}.
-This means these \constraints{} are in \posc{} context and can be \gls{half-reified}.
 
 \Cref{tab:half-qcp} shows the comparison of two solving configurations in \gls{chuffed} for the QCP-max problem.
 The results are grouped based on their size of the instance.
@@ -1189,7 +1191,7 @@ That the effect is so positive is surprising since its \gls{rewriting} statistic
 \section{Summary}
 \label{sec:half-summary}
 
-The usage of \gls{reified} \constraints{} can be detrimental to \solver{} performance and the \gls{rewriting} process should use non-\gls{reified} or \gls{half-reif} \constraints{} when possible.
+For some models avoiding \gls{reif} or the usage of \gls{half-reif} instead of \gls{reif} can lead to a significant improvement in solver performance. 
 This chapter presented a framework to reason about \gls{reif} during the \gls{rewriting} process.
 It provided a \microzinc{} analysis that associates each expression with a certain context.
 Depending on the context, we then know whether a \constraint{} can remain non-\gls{reified}, can be \gls{half-reified}, or must be \gls{reified}.

chapters/5_incremental.tex

@@ -23,7 +23,7 @@ The following algorithms are examples of \gls{meta-optimization}.
 
 	\item[\gls{lns}] \autocite{shaw-1998-local-search}
 		This \gls{meta-optimization} algorithm was first introduced as a heuristic for vehicle routing problems, but has proven to be a very successful method to quickly improve \gls{sol} quality for many types of problem.
-		After finding a (sub-optimal) \gls{sol} to a problem, \constraints{} are added to restrict the search in the \gls{neighbourhood} of that \gls{sol}.
+		After finding a (suboptimal) \gls{sol} to a problem, \constraints{} are added to restrict the search in the \gls{neighbourhood} of that \gls{sol}.
 		When a new \gls{sol} is found, the \constraints{} are removed, and \constraints{} for a new \gls{neighbourhood} are added.
 
 	\item[Online Optimization]\autocite{jaillet-2021-online}
@@ -41,7 +41,7 @@ The following algorithms are examples of \gls{meta-optimization}.
 \end{description}
 
 The usage of \gls{meta-optimization} algorithms is not new to \cmls{}.
-Languages such as \gls{opl} and \gls{comet} \autocite{michel-2005-comet}, later succeeded by the \gls{obj-cp} library \autocite{hentenryck-2013-objcp}, provide convenient syntax for programmable search for their target \solvers{}.
+Languages such as \gls{opl}, with extended functionality through use of \emph{OPL Script} \autocite{van-hentenryck-1999-oplscript}, and \gls{comet} \autocite{van-hentenryck-2005-comet}, later succeeded by the \gls{obj-cp} library \autocite{hentenryck-2013-objcp}, provide convenient syntax for programmable search for their target \solvers{}.
 Crucially, \gls{comet} was the first system to introduce the notion of applying new \constraints{} on \gls{restart}.
 A \gls{restart} happens when a solver abandons its current search efforts, returns to its initial \gls{search-space}, and begins a new exploration.
 In many (\gls{cp}) \solvers{} it is possible to add new \constraints{} upon restarting that are only valid for the particular \gls{restart}.
@@ -84,7 +84,7 @@ This allows the \gls{neighbourhood} to be defined in terms of the previous \gls{
 In addition, a \gls{neighbourhood} definition will typically make use of the random number generators available in \minizinc{}.
 
 \Cref{lst:inc-lns-minisearch-pred} shows a simple random \gls{neighbourhood}.
-For each decision variable \mzninline{x[i]}, it draws a random number from a uniform distribution. 
+For each \variable{} \mzninline{x[i]}, it draws a random number from a uniform distribution. 
 If it exceeds threshold \mzninline{destr_rate}, then it posts \constraints{} forcing \mzninline{x[i]} to take the same value from previous \gls{sol}.
 For example, \mzninline{uniform_neighbourhood(x, 0.2)} would result in each variable in the \gls{array} \mzninline{x} having a 20\% chance of being unconstrained, and an 80\% chance of being assigned to the value it had in the previous \gls{sol}.
 
@@ -461,7 +461,7 @@ During solving, the \solver{} needs to execute the new constraints as follows.
 		This is straightforward by using a \mzninline{last_val} \gls{propagator}.
 		It wakes up whenever its argument is \gls{fixed}, and updates the last value (a non-\gls{backtrack}able value).
 	\item[Random number functions] Fix their \variable{} argument to a random number in the appropriate probability distribution.
-	\item[\mzninline{complete_reif(c)}] Stop and mark the search as ``complete'' when its \variable{} argument is forced to be \true{}.
+	\item[\mzninline{complete_reif(c)}] Stop and mark the search as ``complete'' when its \variable{} argument is set to be \true{}.
 \end{description}
 
 \noindent{}Importantly, these \constraints{} need to be propagated in a way that their effects can be undone for the next \gls{restart}.

chapters/6_conclusions.tex

@@ -56,7 +56,7 @@ However, the performance of these prototypes already surpasses the existing impl
 
 This architecture enables many avenues of further research.
 For one, the formal rewriting rules presented open up possibilities to more extended formal reasoning about \cmls{}.
-This could potentially lead to the ability to prove certain properties of the \gls{rewriting} process.
+This could potentially lead to the ability to prove the integrity of the \gls{rewriting} process.
 Additionally, the architecture introduces reasoning about the transition from \minizinc{} \instances{} to \gls{slv-mod} as two different levels: the transition from \minizinc{} to \microzinc{} and the evaluation of the \nanozinc{} program to create a \gls{slv-mod}.
 In our prototype we have presented techniques to help improve the quality of the \gls{slv-mod}, but many improvements to these techniques and other techniques may be possible.
 Finally, we use \nanozinc{} to track \constraints{} that are introduced to define a \variable{}.
@@ -142,8 +142,13 @@ The improvements offered by these new methods may spark future research.
 Primarily, they will allow and promote using \gls{meta-optimization} algorithms in \cmls{} for new problems.
 It could even be worthwhile to revisit existing applications of incremental constraint modelling.
 The utilization of the presented methods can offer a significant improvement in performance, allowing the solving of more complex problems.
-Finally, new \gls{meta-optimization} techniques could require extensions of the methods presented.
 
+Other \gls{meta-optimization} techniques, such as \emph{column generation} \autocite{ford-2004-column} and \emph{logic-based Benders decomposition} \autocite{hooker-2003-lbbd}, require extensions of the methods presented.
+To support column generation, the methods would need to be extended to allow not only the addition of new \variables{}, but the usage of these \variables{} in existing \constraints{}, using so-called \emph{open constraints}.
+Logic-based Benders decomposition uses multiple interacting solvers to solve different parts of the problem.
+Since \minizinc{} \solvers{} often reason about the same \instance{} using different \variables{}, special handling will need to be added to \minizinc{} to ensure the \solvers{} can interact with each other.
+
+\pagebreak{}
 \section*{Summary}
 In conclusion, this thesis presented an architecture for the \gls{rewriting} of \cmls{}.
 This architecture has been designed with modern usages of these languages in mind, such as \gls{rewriting} for low-level \solvers{} and \gls{meta-optimization}.