Work on half-reification (most intro)

assets/packages.tex

@@ -66,6 +66,7 @@
 
 % Glossary / Acronyms
 \usepackage[acronym,toc]{glossaries}
+\glsdisablehyper % Comment for debugging
 \usepackage[stylemods=bookindex]{glossaries-extra}
 \usepackage{titlecaps}
 \setabbreviationstyle[acronym]{long-short}

chapters/4_half_reif.tex

@@ -2,9 +2,12 @@
 \chapter{Half Reification}\label{ch:half-reif}
 %************************************************
 
+\glsreset{half-reif}
+
 \input{chapters/4_half_reif_preamble}
 
-\section{Introduction to Half Reification}
+\section{An Introduction to Half Reification}
+\label{sec:half-intro}
 
 The complex expressions language used in \cmls{}, such as \minizinc{}, often require the use of \gls{reification} in the flattening process to reach a solver level constraint model.
 If the Boolean expression \mzninline{pred(...)} is seen in a non-root context, then a new Boolean \variable{} \mzninline{b} is introduced to replace the expression, its \emph{control} \variable{}.
@@ -24,16 +27,17 @@ Flattening with \gls{half-reif} is an approach that improves upon all these weak
 
 \begin{enumerate}
 	\item Flattening using \glspl{half-reif} naturally produces relational semantics.
-	\item Propagators for a \glspl{half-reif} can often be constructed by merely altering the implementation the regular \constraint.
+	\item Propagators for a \glspl{half-reif} can often be constructed by merely altering the implementation the regular \constraint{}.
 	\item The control \variables{} can limit the amount of triggered propagators that are known to be unable to prune any variables.
 \end{enumerate}
 
-\jip{Talk about the benefit for propagation}.
+Additionally, for many \solvers{} the decomposition of a \gls{reification} is more complex than a \gls{half-reif}.
+We will show that the usage of \glspl{half-reif} can therefore lead to a reduction in \constraints{} in the solver level constraint model.
 
 \Gls{half-reif} can be used instead of full \gls{reification} when the \gls{reification} can never be forced to be false.
 We see this in, for example, a disjunction \(a \lor b\).
 No matter the value of \(a\), setting the value of \(b\) to be true can never make the overall expression false.
-At any \(b\) is thus never forced to be false.
+\(b\) is thus never forced to be false.
 This requirement follows from the difference between implication and logical equivalences.
 Setting the left hand side of a implication to false, does not influence the value on the right hand side.
 So if we know that this is never required in the overall expression, then using an implication instead of a logical equivalence (\ie{} a \gls{half-reif} instead of a full \gls{reification}) does not change the meaning of the constraint.
@@ -195,8 +199,7 @@ This formula, however, is no longer a direct set of clauses.
 Rewriting this formula into \gls{cnf} would result in:
 \[ \neg b \implies \neg c = \forall_{i,j} b \lor lit_{ij} \]
 This adds a new binary clause for every literal in the original \gls{cnf}.
-This overhead can be avoided when using \gls{half-reif}.
+In general, many more clauses are needed to decompose a \gls{reification} compared to a \gls{half-reif}.
-\jip{TODO: it would be great to conclude here that all these clauses are unnecessary in a positive context, since \(b\) would never be set to false.}
 
 According to the principles above, decomposition libraries for the full \minizinc{} language have been implemented for \gls{mip} and \gls{sat} solvers.
 In \cref{sec:half-experiments} we asses the effects when flattening with \gls{half-reif}.
@@ -204,7 +207,6 @@ In \cref{sec:half-experiments} we asses the effects when flattening with \gls{ha
 \section{Context Analysis}%
 \label{sec:half-context}
 
-
 When taking into account the possible undefinedness of an expression, every expression in a \minizinc{} model has two different contexts: the context in which the expression itself occurs, its \emph{value context}, and the context in which the partiality of the expression is captured, its \emph{partiality context}.
 As described in \cref{subsec:back-mzn-partial}, \minizinc{} uses relational semantics of partial values.
 This means that if a function does not have a result, then its nearest enclosing Boolean expression is set to false.

chapters/4_half_reif_preamble.tex

@@ -1,14 +1,16 @@
-\noindent{}In this chapter we revisit the notion of \gls{half-reif} as introduced by Feydy et al.\ \autocite*{feydy-2011-half-reif}.
+\noindent{}Feydy et al.\ introduced the notion of \gls{half-reif} as an improvement over the use of \gls{reification} \autocite*{feydy-2011-half-reif}.
-\jip{TODO: benefits of half-reification}.
+They show that some of the problems and expenses of the use of \gls{reification} can be mitigated using this technique.
-We show that in modern \gls{cp} \solvers{} still benefit from the use of half-reified propagators.
+In addition, the creation of propagators for \glspl{half-reif} of constraints can often be an easy process.
-\jip{This was already discussed in the half-reif paper} Additionally, we discuss a technique that often allows solver implementer to adapt a propagator for a regular constraint to its \gls{half-reif}.
+It is not always possible, however, to use a \gls{half-reif} instead of a \gls{reification}.
-We also discuss the advantages of the use of \gls{half-reif} when writing decompositions and introduce a new version of the linearisation library that enjoys these advantages.
+The authors identify the conditions required for the usage of \gls{half-reif} and provide an algorithm that flattens a subset of the \minizinc{} language using the technique.
-We introduce methods to automatically detect when a expression in a \minizinc\ model can be half-reified, enabling the modellers to enjoy the advantages of half-reification without having to introduce them manually.
+Crucially, this algorithm does \emph{not} directly generalize to the full \minizinc{} language.
-Finally, we discuss the effect of half-reification on earlier discussed flattening methods.
+The chosen subset omits let-expressions, which can complicate the process.
-
+An identifier for the same expression can suddenly occur in multiple locations.
-The remainder of the chapter is organised as follows.
-\Cref{sec:half-propagation} discusses the propagation of half-reified \constraints{}.
-\Cref{sec:half-decomposition} discusses the decomposition of half-reified constraint.
-\Cref{sec:half-context} introduces the notion of context analysis: a way to determine if \gls{half-reif} can be used for a certain expression.
-Finally, \cref{sec:half-flattening} explains how this information can be used during the flattening process.
 
+This chapter re-evaluates the usage of \gls{half-reif} and provides the first full implementation of a flattener for \minizinc{} with support for \gls{half-reif}.
+In \cref{sec:half-intro,sec:half-propagation} we introduce the core concepts of \gls{half-reif} and propagators for half-reified \constraints{}, as discussed by Feydy et al.
+An additional benefit of \gls{half-reif} is that its decomposition can be significantly smaller than the decomposition of a \gls{reification}.
+\Cref{sec:half-decomposition} shows the benefits of \gls{half-reif} when writing decompositions for \gls{mip} and \gls{sat} \solvers{}.
+In \cref{sec:half-context} we introduce our new context analysis algorithm: a way to determine where \gls{half-reif} can be used in \microzinc{}, and by extend \minizinc{}.
+Then, in \cref{sec:half-flattening}, we elaborate on how the usage of \gls{half-reif} changes the flattening process.
+Finally, the effects of propagators for half-reified constraints and the automatic introduction of half-reified is analysed in \cref{sec:half-experiments}.