diff --git a/assets/bibliography/references.bib b/assets/bibliography/references.bib index 7955c51..0f112b1 100644 --- a/assets/bibliography/references.bib +++ b/assets/bibliography/references.bib @@ -706,6 +706,18 @@ 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 diff --git a/assets/listing/half_alldiff.mzn b/assets/listing/half_alldiff.mzn new file mode 100644 index 0000000..db2561e --- /dev/null +++ b/assets/listing/half_alldiff.mzn @@ -0,0 +1,4 @@ +predicate all_different(array[int] of var int: x) = + forall(i,j in index_set(x) where i < j)( + x[i] != x[j] + ); diff --git a/assets/listing/half_impli.mzn b/assets/listing/half_impli.mzn new file mode 100644 index 0000000..e99ff69 --- /dev/null +++ b/assets/listing/half_impli.mzn @@ -0,0 +1,5 @@ +predicate impli( + var bool: x ::promise_ctx_antitone, + var bool: y ::promise_ctx_monotone +) = + not x \/ y; diff --git a/assets/listing/half_reif_check.mzn b/assets/listing/half_reif_check.mzn new file mode 100644 index 0000000..d676391 --- /dev/null +++ b/assets/listing/half_reif_check.mzn @@ -0,0 +1,15 @@ +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; diff --git a/chapters/2_background.tex b/chapters/2_background.tex index 3189c52..b7b8829 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -155,7 +155,7 @@ The structure of a \minizinc{} model can be described directly in terms of a \cm \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}. @@ -180,7 +180,7 @@ The type of a \variable{} is preceded by the \mzninline{var} keyword. 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} diff --git a/chapters/4_half_reif.tex b/chapters/4_half_reif.tex index 59fdc36..7c3cb1e 100644 --- a/chapters/4_half_reif.tex +++ b/chapters/4_half_reif.tex @@ -30,7 +30,7 @@ As an alternative, the authors introduce \gls{half-reif}. \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} @@ -76,7 +76,7 @@ Now, we will categorise the latter into: \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{}. @@ -98,7 +98,7 @@ Although expressions in a \negc{} context cannot be directly \gls{half-reified}, \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. @@ -122,7 +122,7 @@ Given \texttt{b}, \(check\), and \(prune\), \cref{alg:half-prop} shows pseudo co \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\)).} @@ -191,7 +191,7 @@ Ultimately, \minizinc{}'s \gls{linearisation} library rewrites most \glspl{reif} 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} \] @@ -340,17 +340,14 @@ If a function argument is not annotated, then the argument is evaluated in \mixc \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} @@ -373,7 +370,7 @@ If a function argument is not annotated, then the argument is evaluated in \mixc \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{ /\ }}{ @@ -409,7 +406,7 @@ Otherwise, the \compiler{} follows the following steps to try to introduce the m 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. @@ -505,7 +502,7 @@ The (Item0) rule is triggered when there are no more inner items in the let-expr \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} @@ -514,14 +511,16 @@ It is, however, not always safe to do so. 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. @@ -536,16 +535,16 @@ It is, however, not always safe to do so. } 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}. @@ -580,7 +579,7 @@ Otherwise, it will act as a normal \rootc{} context. \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}. @@ -590,7 +589,7 @@ We will, however, discuss the dynamically adjusting of contexts during \gls{rewr \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} @@ -626,7 +625,7 @@ During the \gls{rewriting} process the contexts assigned to the different expres 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{}. @@ -634,9 +633,9 @@ During the \gls{rewriting} process the contexts assigned to the different expres 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} @@ -650,7 +649,7 @@ It can be used to eliminate these \glspl{implication-chain}. 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} @@ -660,13 +659,13 @@ In this case the conjunction can be replaced by \mzninline{b1 -> c} and \texttt{ 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. @@ -708,21 +707,21 @@ The algorithm can be further improved by considering implied conjunctions. 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} @@ -759,7 +758,7 @@ All usages of the previously recorded result is replaced by the new result. 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. @@ -771,7 +770,7 @@ The expression is \gls{reified} and replaces the existing \gls{half-reified} exp 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} @@ -799,7 +798,7 @@ The same situation can be caused by \gls{propagation}. 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} @@ -811,14 +810,14 @@ The same situation can be caused by \gls{propagation}. \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. @@ -826,27 +825,14 @@ 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} @@ -889,18 +875,16 @@ Therefore, the transformation described in \cref{sec:half-propagation} can be di 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} \input{assets/table/half_qcp} @@ -1039,7 +1023,7 @@ In general, we would expect the reduction of \constraints{} in a \gls{mip} insta 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. diff --git a/chapters/4_half_reif_preamble.tex b/chapters/4_half_reif_preamble.tex index 4d13308..8a42b46 100644 --- a/chapters/4_half_reif_preamble.tex +++ b/chapters/4_half_reif_preamble.tex @@ -1,14 +1,14 @@ \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.