Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Work on half-reification rephrasing

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-15 17:13:58 +10:00
parent ee7d13ab53
commit 1771f3e6f9
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
7 changed files with 281 additions and 305 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
assets/glossary.tex
View File

@ -256,8 +256,8 @@
}
\newglossaryentry{half-reif}{
name={half reification},
description={},
name={half-reification},
description={A half-reification is a variation of a \gls{reif} where for a \gls{constraint} \(c\) it enforces that a \gls{cvar} \texttt{b} represents the logical implication of the \gls{constraint}: \(\texttt{b} \rightarrow{} c\)},
}
\newglossaryentry{half-reified}{
@ -491,7 +491,7 @@
\newglossaryentry{reif}{
name={reification},
description={A reification is a special form of a \gls{constraint} where, instead of the \gls{constraint} being enforced in the \glspl{sol}, it enforces that a \gls{cvar} represents whether the \gls{constraint} holds or not},
description={A reification is a special form of a \gls{constraint} where, instead of the \gls{constraint} \(c\) being enforced in the \glspl{sol}, it enforces that a \gls{cvar} \texttt{b} represents whether the \gls{constraint} holds or not: \(\texttt{b} \leftrightarrow{} c\)},
}
\newglossaryentry{reified}{

2
assets/table/half_flat_gecode.tex
View File

@ -6,6 +6,6 @@
Reifications & 1,698,026 & 763,031 & (-55.06\%) \\
Half Reifications & 0 & 934,975 & \\
Implications Removed & 0 & 54,169 & \\
Flattening Time & 575s & 580s & (0.93\%) \\
Rewriting Time & 575s & 580s & (0.93\%) \\
\bottomrule
\end{tabular}

2
assets/table/half_flat_linear.tex
View File

@ -6,6 +6,6 @@
Reifications & 3,786,613 & 2,570,378 & (-32.12\%) \\
Half Reifications & 0 & 1,099,397 & \\
Implications Removed & 0 & 67,833 & \\
Flattening Time & 3,223s & 3,279s & (1.73\%) \\
Rewriting Time & 3,223s & 3,279s & (1.73\%) \\
\bottomrule
\end{tabular}

2
assets/table/half_flat_sat.tex
View File

@ -6,6 +6,6 @@
Reifications & 433,761 & 263,386 & (-39.28\%) \\
Half Reifications & 42,228 & 178,984 & \\
Implications Removed & 0 & 0 & \\
Flattening Time & 614s & 604s & (-1.76\%) \\
Rewriting Time & 614s & 604s & (-1.76\%) \\
\bottomrule
\end{tabular}

18
chapters/2_background.tex
View File

@ -401,7 +401,7 @@ There are three main purposes for \glspl{let}:
\end{enumerate}
An important detail in \gls{rewriting} \glspl{let} is that any \variables{} that are introduced may need to be renamed in the resulting \gls{slv-mod}.
Different \variables{} declared directly in declaration items, the \variables{} declared in \glspl{let} can be flattened multiple times when used in loops, function definitions (that are called multiple times), and \gls{array} \glspl{comprehension}.
Different \variables{} declared directly in declaration items, the \variables{} declared in \glspl{let} can be evaluated multiple times when used in loops, function definitions (that are called multiple times), and \gls{array} \glspl{comprehension}.
The \gls{rewriting} process must assign any \variables{} in the \gls{let} a new name and use this name in any subsequent definitions and in the resulting expression.
\paragraph{Annotations} Although \minizinc{} does not typically prescribe a way to find the \gls{sol} for an \instance{}, it does provide the modeller a way to give ``hints'' to the \solver{}.
@ -643,24 +643,24 @@ They allow modellers to use always use \glspl{global} and depending on the \solv
\begin{subfigure}[b]{.48\columnwidth}
\centering
\includegraphics{assets/img/back_chess1}
\caption{\label{sfig:back-nqueens-1} Assign a queen to d3}
\caption{\label{sfig:back-nqueens-1} Assign a queen to d3.}
\end{subfigure}%
\hspace{0.04\columnwidth}%
\begin{subfigure}[b]{.48\columnwidth}
\centering
\includegraphics{assets/img/back_chess2}
\caption{\label{sfig:back-nqueens-2} Propagate rows}
\caption{\label{sfig:back-nqueens-2} Propagate the rows.}
\end{subfigure}
\begin{subfigure}[b]{.48\columnwidth}
\centering
\includegraphics{assets/img/back_chess3}
\caption{\label{sfig:back-nqueens-3} Propagate upwards diagonal}
\caption{\label{sfig:back-nqueens-3} Propagate the upwards diagonal.}
\end{subfigure}%
\hspace{0.04\columnwidth}%
\begin{subfigure}[b]{.48\columnwidth}
\centering
\includegraphics{assets/img/back_chess4}
\caption{\label{sfig:back-nqueens-4} Propagate downward diagonal}
\caption{\label{sfig:back-nqueens-4} Propagate the downward diagonal.}
\end{subfigure}
\caption{\label{fig:back-nqueens} An example of domain propagation when a queen gets assigned in the N-Queens problem.}
\end{figure}
@ -1236,8 +1236,8 @@ For instance, replacing the usage of enumerated types by normal integers.
compiler.}
\end{figure}
The middle-end contains the most important two processes: the flattening and the optimisation.
During the flattening process the \minizinc{} model is rewritten into a \gls{slv-mod}.
The middle-end contains the most important two processes: the rewriting and the optimisation.
During the \gls{rewriting} process the \minizinc{} model is rewritten into a \gls{slv-mod}.
It could be noted that the rewriting step depends on the compilation target to define its \gls{native} \constraints{}.
Even though the information required for this step is target dependent, we consider it part of the middle-end as the mechanism is the same for all compilation targets.
A full description of this process will follow in \cref{subsec:back-rewriting}.
@ -1368,7 +1368,7 @@ Some expressions only become syntactically equal when instantiated, as in the fo
To ensure that the same instantiation of a function are only evaluated once, the \minizinc{} \compiler{} uses memoisation.
After the \gls{rewriting} of an expression, the instantiated expression and its result are stored in a lookup table: the \gls{cse} table.
Then before any consequent expression is flattened the \gls{cse} table is consulted.
Then before any consequent expression is rewritten the \gls{cse} table is consulted.
If an equivalent expression is found, then the accompanying result is used; otherwise, the evaluation proceeds as normal.
In our example, the evaluation of \mzninline{pythagoras(i, i)} would proceed as normal to evaluate \mzninline{x = pow(i, 2)}.
@ -1507,7 +1507,7 @@ On the other hand, evaluating a predicate may also \emph{impose} new bounds on \
The same problem occurs with \glspl{reif} that are produced during \gls{rewriting}.
Other \constraints{} could fix the \domain{} of the reified \variable{} and make the \gls{reif} unnecessary.
Instead, the \constraint{} (or its negation) can be flattened in \rootc{} context.
Instead, the \constraint{} (or its negation) can be rewritten in \rootc{} context.
This could avoid the use of a big \gls{decomp} or an expensive \gls{propagator}.
To tackle this problem, the \minizinc{} \compiler{} employs \gls{del-rew}.

522
chapters/4_half_reif.tex
View File

@ -3,142 +3,103 @@
%************************************************
\glsreset{half-reif}
\glsreset{half-reified}
\glsreset{reif}
\glsreset{reified}
\input{chapters/4_half_reif_preamble}
\paragraph{Reification - Text from rewriting}
\todo{Adjust with information in the background section. Is there anything specific to the \microzinc{}/\nanozinc{} system?}
Many constraint modelling languages, including \minizinc{}, not only enable \constraints{} to be globally enforced, but typically also support \constraints{} to be \emph{reified} into a Boolean variable.
Reification means that a variable \mzninline{b} is constrained to be true if and only if a corresponding constraint \mzninline{c(...)
} holds.
We have already seen reification in \cref{ex:rew-absreif}: the truth of constraint \mzninline{abs(x) > y} was bound to a Boolean variable \mzninline{b1}, which was then used in a disjunction.
We say that the same constraint can be used in \emph{root context} as well as in a \emph{reified context}.
In \minizinc{}, almost all constraints can be used in both contexts.
However, reified constraints are often defined in the library in terms of complicated decompositions into simpler constraints, or require specialised algorithms in the target solvers.
In either case, it can be very beneficial for the efficiency of the generated \nanozinc\ program if we can detect that a reified constraint is in fact not required.
If a constraint is present in the root context, it means that it must hold globally.
If the same constraint is used in a reified context, it can therefore be replaced with the constant \mzninline{true}, avoiding the need for reification (or in fact any evaluation).
We can harness \gls{cse} to store the evaluation context when a constraint is added, and detect when the same constraint is used in both contexts.
Whenever a lookup in the \gls{cse} table is successful, action can be taken depending on both the current and stored evaluation context.
If the stored expression was in root context, then the constant \mzninline{true} can be used, independent of the current context.
Otherwise, if the stored expression was in reified context and the current context is reified, then the stored result variable can be used.
Finally, if the stored expression was in reified context and the current context is root context, then the previous result can be replaced by the constant \mzninline{true} (and all its dependencies removed) and the evaluation will proceed as normal with the root context constraint.
\begin{example}
Consider the fragment:
\begin{mzn}
function var bool: p(var int: x, var int: y) = q(x) /\ r(y);
constraint b0 <-> q(x);
constraint b1 <-> t(x,y);
constraint b1 <-> p(x,y);
\end{mzn}
If we process the top-level constraints in order we create a reified call to \mzninline{q(x)} for the original call.
Suppose processing the second constraint we discover \mzninline{t(x,y)} is \mzninline{true}, fixing \mzninline{b1}.
When we then process \mzninline{q(x)} in instantiation of the call \mzninline{p(x,y)}, we find it is the root context.
So \gls{cse} needs to set \mzninline{b0} to \mzninline{true}.
\end{example}
\minizinc{} distinguishes not only between root and reified contexts, but in addition recognises constraints in \emph{positive} contexts, also known as \emph{half-reified} \autocite{feydy-2011-half-reif}.
A full explanation and discussion of half-reification can be found in \cref{ch:half-reif}.
\todo{Reification should also be discussed in the background. How can we
make this more specific to how it works in \nanozinc{}.}
\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{reif} 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{}.
The flattener then enforces a \constraint{} \mzninline{pred_reif(...,b)}, which binds the \variable{} to be the \emph{truth-value} of the expression (\ie\ \mzninline{b <-> pred(...)}).
The complex expressions language used in \cmls{}, such as \minizinc{}, often require the use of \gls{reif} in the \gls{rewriting} process to reach a \gls{slv-mod}.
If the Boolean expression \mzninline{pred(...)} is seen in a non-\rootc{} context, then a new Boolean \variable{} \mzninline{b} is introduced to replace the expression, its \gls{cvar}.
The \gls{rewriting} process then enforces a \constraint{} \mzninline{pred_reif(...,b)}, which binds the \variable{} to be the truth-value of the expression (\ie\ \mzninline{b <-> pred(...)}).
\textcite{feydy-2011-half-reif} show that although the usage of \gls{reif} in the flattening process is well-understood, it suffers from certain weaknesses:
\textcite{feydy-2011-half-reif} show that although the usage of \gls{reif} in the \gls{rewriting} process is well-understood, it suffers from certain weaknesses:
\begin{enumerate}
\item Many \glspl{reif} are created in the rewriting of partial expressions to accommodate \minizinc{}'s relational semantics.
\item Propagators for the \glspl{reif} of global constraints are scarce.
\item A \gls{reif} sometimes provides too much information to its surrounding context, triggering propagators that will never be able to prune any values from a \gls{domain}.
\item Many \glspl{reif} are created in the rewriting of partial expressions to accommodate \minizinc{}'s \glspl{rel-sem}.
\item \Glspl{propagator} for the \glspl{reif} of \glspl{global} are scarce.
\item A \gls{reif} sometimes provides too much information to its surrounding context, triggering \glspl{propagator} that will never be able to prune any values from a \gls{domain}.
\end{enumerate}
In contrast, the authors introduce \gls{half-reif}.
As an alternative, the authors introduce \gls{half-reif}.
\gls{half-reif} 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(...)}.
Flattening with \gls{half-reif} is an approach that improves upon all these weaknesses of flattening with \emph{full} reification:
\Gls{rewriting} with \gls{half-reif} is an approach that improves upon all these weaknesses of \gls{rewriting} with \emph{full} \gls{reif}:
\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 The control \variables{} can limit the amount of triggered propagators that are known to be unable to prune any variables.
\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 \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}
Additionally, for many \solvers{} the decomposition of a \gls{reif} 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.
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 the usage of \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 \gls{reif} can never be forced to be false.
\Gls{half-reif} can be used instead of full \gls{reif} when the resulting \gls{cvar} 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.
\(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{reif}) does not change the meaning of the constraint.
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{reif}) does not change the meaning of the \constraint{}.
This property can be extended to include non-Boolean expressions.
Since Boolean expressions in \minizinc{} can be used in, for example, integer expressions, we can apply similar reasoning to these types of expressions.
\begin{example}
For example the left hand side of the constraint
For example the left hand side of the following \constraint{} is an integer expression that contains the Boolean expression \mzninline{x = 5}.
\begin{mzn}
constraint count(x in arr)(x = 5) > 5;
\end{mzn}
\noindent{}is an integer expression that contains the Boolean expression \mzninline{x = 5}.
Since the increasing left hand side of the constraint will only ever help satisfy the constraint, the expression \mzninline{x = 5} will never forced to be false.
This means that we only need to half-reify the expression.
Since the increasing left hand side of the \constraint{} will only ever help satisfy the \constraint{}, the expression \mzninline{x = 5} will never forced to be false.
This means that the expression can be \gls{half-reified}.
\end{example}
To systematically analyse whether Booelean expressions can be half-reified, we introduce extra distinctions in the context of expressions.
Before, we would merely distinguish between \rootc{} context and \emph{non-root} context.
To systematically analyse whether Boolean expressions can be \gls{half-reified}, we introduce extra distinctions in the context of expressions.
Before, we would merely distinguish between \rootc{} context and non-\rootc{} context.
Now, we will categorise the latter into:
\begin{description}
\item[\posc{} context] when an expression must reach \emph{at least} a certain value to satisfy its enclosing constraint.
\item[\posc{} context] when an expression must reach \emph{at least} a certain value to satisfy its enclosing \constraint{}.
The expression is never forced to take a lower value.
\item[\negc{} context] when an expression can reach \emph{at most} a certain value to satisfy its enclosing constraint.
\item[\negc{} context] when an expression can reach \emph{at most} a certain value to satisfy its enclosing \constraint{}.
The expression is never forced to take a higher value.
\item[\mixc{} context] when an expression must take an \emph{exact value}, be within a \emph{specified range} or when during flattening it cannot be determined whether the expression must be increased or decreased to satisfy the enclosing constraint.
\item[\mixc{} context] when an expression must take an \emph{exact value}, be within a \emph{specified range} or when during \gls{rewriting} it cannot be determined whether the expression must be increased or decreased to satisfy the enclosing \constraint{}.
\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 half-reified, the negation of a expression in a \negc{} context can be half-reified.
Consider, for example, the constraint
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}.
\begin{mzn}
constraint b \/ not (x = 5);
\end{mzn}
\begin{example}
Consider, for example, the following \constraint{}.
The expression \mzninline{x = 5} is in a \negc{} context.
Although a \gls{half-reif} cannot be used directly, in some cases the solver can negate the expression which are then placed in a \posc{} context.
Our example can be transformed into:
\begin{mzn}
constraint b \/ not (x = 5);
\end{mzn}
\begin{mzn}
constraint b \/ x != 5;
\end{mzn}
The expression \mzninline{x = 5} is in a \negc{} context.
Although a \gls{half-reif} cannot be used directly, in some cases the \solver{} can negate the expression which are then placed in a \posc{} context.
Our example can be transformed into the following \constraint{}.
The transformed expression, \mzninline{x != 5}, is now in a \posc{} context.
We can also speak of this process as ``pushing the negation inwards''.
\begin{mzn}
constraint b \/ x != 5;
\end{mzn}
The transformed expression, \mzninline{x != 5}, is now in a \posc{} context.
We can also speak of this process as ``pushing the negation inwards''.
\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.
This occurs, for example, when using an exclusive or expression in a constraint.
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.
The \mixc{} context can also be used as a ``fall back'' context.
@ -147,118 +108,119 @@ If it cannot be determined if an expression is in a \posc{} or \negc{} context,
\section{Propagation and Half Reification}%
\label{sec:half-propagation}
The tasks of a propagator for any constraint can logically be split into two tasks:
The tasks of a \gls{propagator} for any constraint can logically be split into two:
\begin{enumerate}
\item To \(check\) if the constraint can still be satisfied (and otherwise \emph{fail} the current state)
\item To \(prune\) values from the \glspl{domain} of \variables{} that would violate the constraint.
\item to \(check\) if the \constraint{} can still be satisfied (and otherwise declare the current state \gls{unsat}),
\item and to \(prune\) values from the \glspl{domain} of \variables{} that would violate the constraint.
\end{enumerate}
When creating a propagator for the \gls{half-reif} of a constraint, it can be constructed from these two tasks.
The half-reified propagator is dependent on an additional argument \(b\), which is a Boolean \variable{}.
When creating a \gls{propagator} for the \gls{half-reif} of a \constraint{}, it can be constructed from these two tasks.
The \gls{half-reified} \gls{propagator} is dependent on an additional argument \texttt{b}, the \gls{cvar}.
The Boolean \variable{} can be in three states, it can currently not have been assigned a value, it can be assigned \mzninline{true}, or it can be assigned \mzninline{false}.
Given \(b\), \(check\), and \(prune\), \cref{alg:half-prop} shows pseudo code for the propagation of the \gls{half-reif} of the constraint.
Given \texttt{b}, \(check\), and \(prune\), \cref{alg:half-prop} shows pseudo code for the \gls{propagation} of the \gls{half-reif} of the constraint.
\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 the constraint \(c\), and a Boolean control \variable{} \(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 the \constraint{} \(c\), and a Boolean control \variable{} \texttt{b}.
}
\KwResult{This pseudo code propagates the \gls{half-reif} of \(c\) (\ie{} \(b \implies\ c\)).}
\KwResult{This pseudo code propagates the \gls{half-reif} of \(c\) (\ie{} \(\texttt{b} \implies\ c\)).}
\BlankLine{}
\If{\(b\) {\normalfont is unassigned} }{
\If{\texttt{b} {\normalfont is unassigned} }{
\If{\(\neg{}check()\)}{
\(b \longleftarrow \) \mzninline{false}\;
\(\texttt{b} \longleftarrow \) \mzninline{false}\;
}
}
\If{\(b = \) \mzninline{true}}{
\If{\(\texttt{b} = \mzninline{true}\)}{
\(prune()\)\;
}
\caption{\label{alg:half-prop} Propagation pseudo code for the \gls{half-reif} of a constraint \(c\), based on the propagator for \(c\).}
\end{algorithm}
Logically, the creation of propagators for \glspl{half-reif} can always follow this simple principle.
Logically, the creation of \glspl{propagator} for \glspl{half-reif} can always follow this simple principle.
In practice, however, this is not always possible.
In some cases, propagators do not explicitly define \(check\) as a separate step.
In some cases, \glspl{propagator} do not explicitly define \(check\) as a separate step.
Instead, this process can be implicit.
The propagator merely prunes the \glspl{domain} of the \variables{}.
When a \gls{domain} is found to be empty, then the propagator fails the current state.
It is not possible possible to construct the half-reified propagator from such an implicit \(check\) operation.
Instead a new explicit \(check\) method has to be devised to implement the propagator of the \gls{half-reif}.
The \gls{propagator} merely prunes the \glspl{domain} of the \variables{}.
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\) operation.
Instead a new explicit \(check\) method has to be devised to implement the \gls{propagator} of the \gls{half-reif} \constraint{}.
A propagation engine gains certain advantages from \gls{half-reif}, but also may suffer certain penalties.
Half reification can cause propagators to wake up less frequently, since variables that are fixed to true by full reification will never be fixed by half reification.
This is advantageous, but a corresponding disadvantage is that variables that are fixed can allow the simplification of the propagator, and hence make its propagation faster.
\Glspl{propagator} gain certain advantages from \gls{half-reif}, but also may suffer certain penalties.
\Gls{half-reif} can cause propagators to wake up less frequently: \glspl{cvar} that are fixed to true by full \gls{reif} will never be fixed by \gls{half-reif}.
This is advantageous, but a corresponding disadvantage is that \glspl{cvar} that are fixed can allow the simplification of the \glspl{propagator} that use them, and hence make \gls{propagation} faster.
When a full \gls{reif} is required and a full reification \mzninline{x <-> pred(...)} by using two half reified propagators, \mzninline{x -> pred(...)} and \mzninline{y -> not pred(...)}, and the constraint \mzninline{x <-> not y}.
This does not lose propagation strength.
For Booleans appearing in a positive context we can make the propagator of the negated \gls{half-reif} run at the lowest priority, since it will never cause failure.
Similarly in negative contexts we can make the propagator \mzninline{b -> pred(...)} run at the lowest priority.
This means that Boolean variables are still fixed at the same time, but there is less overhead.
When a full \gls{reif} is required, its \gls{propagation} might still be performed using \gls{half-reif}.
A full \gls{reif} \mzninline{x <-> pred(...)} can be propagated using two half reified propagators, \mzninline{x -> pred(...)} and \mzninline{y -> not pred(...)}, and the \constraint{} \mzninline{x <-> not y}.
This does not lose \gls{propagation} strength.
For Booleans appearing in \posc{} context we can make the \gls{propagator} of the negated \gls{half-reif} run at the lowest priority, since it will never detect if the state is \gls{unsat}.
Similarly in \negc{} context we can make the propagator \mzninline{b -> pred(...)} run at the lowest priority.
This means that the \glspl{cvar} are still fixed at the same time, but there is less overhead.
In \cref{sec:half-experiments} we assess the implementation of propagators for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element}.
Both propagators are designed and implemented in \gls{chuffed} according to the principle explained above.
In \cref{sec:half-experiments} we assess the implementation of \glspl{propagator} for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element}.
Both \glspl{propagator} are designed and implemented in \gls{chuffed} according to the principles explained above.
\section{Decomposition and Half Reification}%
\label{sec:half-decomposition}
The use of \gls{half-reif} does not only offer a benefit when a propagator for the half-reified constraint is available.
It can also be beneficial in the decomposition of constraints.
Compared to full \gls{reif}, the decomposition of a \gls{half-reif} does not need to keep track of as much information.
In particular, this can be beneficial when the target \solver{} is a \gls{mip} or \gls{sat} solver.
The decompositions for these solver technologies often explicitly encode reified constraints using two implications.
The use of \gls{half-reif} does not only offer a benefit when a \gls{propagator} for the \gls{half-reified} \constraint{} is available.
It can also be beneficial in the \gls{decomp} of \constraints{}.
Compared to full \gls{reif}, the \gls{decomp} of a \gls{half-reif} does not need to keep track of as much information.
In particular, this can be beneficial when the target \solver{} is a \gls{mip} or \gls{sat} \solver{}.
The \glspl{decomp} for these \solver{} technologies often explicitly encode \gls{reified} \constraints{} using two implications.
If, however, a \gls{reif} is replaced by a \gls{half-reif}, then only one of these implication is required.
\begin{example}
Consider the \gls{reif} of the \constraint{} \mzninline{i <= 4} using the control variable \mzninline{b}, where \mzninline{i} can take values in the domain \mzninline{0..10}.
If the target solver is a \gls{mip} solver, then this \gls{reif} would be linearised.
It would take the following form:
Consider the \gls{reif} of the \constraint{} \mzninline{i <= 4} using the \gls{cvar} \mzninline{b}, where \mzninline{i} can take values in the domain \mzninline{0..10}.
If the target \solver{} is a \gls{mip} \solver{}, then this \gls{reif} would be linearised.
It would take the following form.
\begin{mzn}
constraint i <= 10 - 6 * b; % b -> i <= 4
constraint i >= 5 - 5 * b; % not b -> i >= 5
\end{mzn}
Instead, if we could determine that the \constraint{} could be half-reified, then the linearisation could be simplified to only the first constraint.
Instead, if we could determine that the \constraint{} could be \gls{half-reified}, then the \gls{linearisation} could be simplified to only the first \constraint{}.
\end{example}
The same principle can be applied all throughout the linearisation process.
Ultimately, \minizinc{}'s linearisation library rewrites most \glspl{reif} in terms of implied less than or equal to \constraints{}.
The same principle can be applied all throughout the \gls{linearisation} process.
Ultimately, \minizinc{}'s \gls{linearisation} library rewrites most \glspl{reif} in terms of implied less than or equal to \constraints{}.
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 decomposition for a \gls{half-reif} can be created from its regular decomposition.
Any constraint \(c\) will decompose into \gls{cnf}:
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}.
\[ c = \forall_{i} \exists_{j} lit_{ij} \]
The \gls{half-reif}, with control variable \(b\), could then be encoded as:
\[ b \implies c = \forall_{i} \neg b \lor \exists_{j} lit_{ij} \]
The transition from the \gls{cnf} of the regular constraint to its \gls{half-reif} only adds a single literal to each clause.
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} \]
The transition from the \gls{cnf} of the regular constraint \(c\) to its \gls{half-reif} \(\texttt{b} \implies{} c\) only adds a single literal to each clause.
It is, however, not as straightforward to construct its full \gls{reif}.
In addition to the half-reified \gls{cnf}, a generic \gls{reif} would require the reverse implication, \(\neg b \implies \neg c\).
In addition to the \gls{half-reified} \gls{cnf}, a generic \gls{reif} would require the implication \(\neg \texttt{b} \implies \neg c\).
Based on the \gls{cnf} of \(c\), this would result in the following logical formula:
\[ \neg b \implies \neg c = \forall_{i} b \lor \neg \exists_{j} lit_{ij} \]
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}.
It adds a new binary clause for every literal in the original \gls{cnf}.
In general, many more clauses are needed to decompose a \gls{reif} compared to a \gls{half-reif}.
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 assess the effects when flattening with \gls{half-reif}.
According to the principles above, \gls{decomp} libraries for the full \minizinc{} language have been implemented for \gls{mip} and \gls{sat} \solvers{}.
In \cref{sec:half-experiments} we assess the effects when \gls{rewriting} with \gls{half-reif}.
\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.
As described in \cref{subsec:back-mzn-partial}, \minizinc{} uses \glspl{rel-sem} for partial functions.
This means that if a function does not have a result, then its nearest enclosing Boolean expression is set to false.
In practice, this means that a condition that tests if the function will return a value is added to the nearest enclosing Boolean expression.
The \emph{partiality} context is the context in which this condition is placed.
The partiality context is the context in which this condition is placed.
The context of an expression cannot always be determined by merely considering \minizinc\ expressions top-down.
Expressions bound to a variable can be used multiple times in expressions that influence their context.
The context of an expression cannot always be determined by merely considering \minizinc{} expressions top-down.
Expressions bound to an identifier can be used multiple times in expressions that influence their context.
\begin{example}
Consider the following \minizinc{} fragment.
@ -269,24 +231,26 @@ Expressions bound to a variable can be used multiple times in expressions that i
} in y -> x /\ x -> z;
\end{mzn}
The predicate call \mzninline{pred(a, b, c)} is bound to the variable \mzninline{x}.
If the \variable{} \mzninline{x} is only used in a \posc{} context, then the call itself is in a \posc{} context as well.
As such, the call could then be half-reified.
The predicate call \mzninline{pred(a, b, c)} is bound to the identifier \mzninline{x}.
If \mzninline{x} is only used in a \posc{} context, then the call itself is in a \posc{} context as well.
As such, the call could then be \gls{half-reified}.
Although this is the case in the left side of the conjunction, the other side uses \mzninline{x} in a \negc{} context.
This means that \mzninline{pred(a, b, c)} is in a \mixc{} context and must be fully reified.
This means that \mzninline{pred(a, b, c)} is in a \mixc{} context and must be fully \gls{reified}.
\end{example}
Note that an alternative approach for this example would be to replace the identifier with its definition.
It would then be possible to half-reify the call and the negation of the call.
Although this would increase the use of \gls{half-reif}, it should be noted that the propagation of these two \glspl{half-reif} would be equivalent to propagating the full \gls{reif} of the call.
It would then be possible to \gls{half-reified} versions of both the call and the negation of the call.
Although this would increase the use of \gls{half-reif}, it should be noted that the \gls{propagation} of these two \glspl{half-reif} would be equivalent to the \gls{propagation} of the full \gls{reif} of the call.
In this scenario, we prefer to create the full \gls{reif} as it decreases the number of \variables{} and \constraints{} in the model.
\subsection{Automated analysis}%
\label{subsec:half-automated}
In the architecture introduced in \cref{ch:rewriting}, contexts of the expressions can be determined automatically.
The analysis is best performed during the compilation process from \minizinc{} to \microzinc{}, instead of during the \microzinc{} interpretation, since it requires knowledge about all usages of certain \variable{} at the same time.
The analysis is best performed during the compilation process from \minizinc{} to \microzinc{}.
It requires knowledge about all usages of certain \variable{} at the same time.
This information is not available during during the interpretation of \microzinc{}.
Without loss of generality we can define the context analysis process for \microzinc{} models.
This has the advantage that the value and partiality have already been explicitly separated and no longer requires special handling.
@ -357,9 +321,9 @@ The behaviour of these transformations is shown in \cref{fig:half-ctx-trans}.
\caption{\label{fig:half-analysis-expr} Context inference rules for \microzinc\ expressions.}
\end{figure*}
\Cref{fig:half-analysis-expr} shows the inference rules for all \microzinc{} expressions, apart from let expressions.
The first rule, (Ident), is unique in the sense that the context of an identifier does not directly affects any sub-expressions.
Instead every context in which the identifier is found is collected and will be processed when evaluating the corresponding declaration.
\Cref{fig:half-analysis-expr} shows the inference rules for all \microzinc{} expressions, apart from \glspl{let}.
The first rule, (Ident), is unique in the sense that the context of an identifier does not directly affect other expressions.
Instead, every context in which the identifier is found is collected and will be processed when evaluating the corresponding declaration.
Note that the presented inference rules do not have any explicit state object.
Instead, we introduce the functions ``pushCtx'' and ``collectCtx''.
These functions track and combine the contexts in which a value is used in an implicit global state.
@ -367,11 +331,11 @@ These functions track and combine the contexts in which a value is used in an im
Most changes in the context of \microzinc{} expressions stem from the consequent (Call) rule.
A call expression can change the context in which its arguments should be evaluated.
As an input to the inference process, a ``argCtx'' function is used to give the context of the arguments of a function, given the function itself and the context of the call.
A definition for this function for the \minizinc\ operators can be found in \cref{alg:arg-ctx}.\footnote{We use \minizinc\ operator syntax instead of \microzinc{} identifiers for brevity and clarity.}
A definition for this function for the \minizinc{} operators can be found in \cref{alg:arg-ctx}.\footnote{We use \minizinc\ operator syntax instead of \microzinc{} identifiers for brevity and clarity.}
Although a standard definition for the ``argMax'' function may cover the most common cases, it does not cover user-defined functions stemming from \minizinc{}.
To address this issue, we introduce the \minizinc{} annotations \mzninline{promise_ctx_monotone} and \mzninline{promise_ctx_antitone} to represent the operations \changepos{} and \changeneg{} respectively.
When a function argument is annotated with one of these annotations, the context of the argument in a call in context \(ctx\) is transformed with the operation coressponding to the annotation (\eg\ \(\changepos{}ctx\) or \(\changeneg{}ctx\)).
Although a standard definition for the ``argCtx'' function may cover the most common cases, it does not cover user-defined functions.
To address this issue, we introduce the \glspl{annotation} \mzninline{promise_ctx_monotone} and \mzninline{promise_ctx_antitone} to represent the operations \changepos{} and \changeneg{} respectively.
When a function argument is annotated with one of these annotations, the context of the argument in a call in context \(ctx\) is transformed with the operation corresponding to the annotation (\eg\ \(\changepos{}ctx\) or \(\changeneg{}ctx\)).
If a function argument is not annotated, then the argument is evaluated in \mixc{} context.
\begin{example}
@ -386,8 +350,8 @@ If a function argument is not annotated, then the argument is evaluated in \mixc
not x \/ y;
\end{mzn}
The annotations placed on the argument of the \mzninline{impli} function will apply the same context transformations as a direct \minizinc{} implication, as shown in \cref{alg:arg-ctx}.
In term of context analysis, this function now is equivalent to the \minizinc{} implication operator.
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}.
In term of context analysis, this function now is equivalent to the \minizinc{} operator.
\end{example}
@ -424,9 +388,9 @@ If a function argument is not annotated, then the argument is evaluated in \mixc
The context in which the result of a call expression is used must also be considered.
The (Call) rule, therefore, introduces the \ctxfunc{ident}{ctx} syntax.
This syntax is used to declare that the compiler must introduce a \microzinc\ function variant that flattens the function call to \(ident\) in the context \(ctx\).
This means that if \(ctx\) is \rootc{}, the compiler can use the the function as defined.
Otherwise, the compiler follows the following steps to try to introduce the most compatible variant of the function:
This syntax is used to declare that the \compiler{} must introduce a \microzinc{} function variant that rewrites the function call to \(ident\) in the context \(ctx\).
This means that if \(ctx\) is \rootc{}, the \compiler{} can use the function as defined.
Otherwise, the \compiler{} follows the following steps to try to introduce the most compatible variant of the function:
\begin{enumerate}
\item If a direct definition for \(ctx\) definition exists, then use this definition.
@ -442,13 +406,13 @@ Otherwise, the compiler follows the following steps to try to introduce the most
\item If \(ctx\) is \posc{} or \negc{}, then change \(ctx\) to \mixc{} and return to step 1.
\item Finally, if none of the earlier steps were successful, then the compilation fails.
Note that this can only occur when a solver-level predicate does not have a \gls{reif}.
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 array access and if-then-else 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, say which expression will hold globally.
This is important for when \(ctx\) is \rootc{}, since we, at compile time, cannot say which expression will hold globally.
We will revisit this issue in \cref{subsec:half-?root}.
Finally, the (Compr) and (Arr) rules show simple inference rules for array construction expressions.
@ -469,7 +433,7 @@ If such an expression is evaluated in the context \(ctx\), then its members can
\begin{prooftree}
\hypo{\ctxitem{I \texttt{; } T: x \texttt{ = } e }}
\hypo{\text{collectCtx}(x) = [ctx_{1}, \ldots, ctx_{n}]}
\infer2[(Assign)]{\ctxeval{x}{\text{join}([ctx_{1}, \ldots, ctx_{n}])},~\ctxitem{I}}
\infer2[(Assign)]{\ctxeval{e}{\text{join}([ctx_{1}, \ldots, ctx_{n}])},~\ctxitem{I}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
@ -496,15 +460,15 @@ If such an expression is evaluated in the context \(ctx\), then its members can
\caption{\label{fig:half-analysis-it} Context inference rules for \microzinc\ let-expressions.}
\end{figure*}
\Cref{fig:half-analysis-it} shows the inference rules for let expressions and their inner items.
\Cref{fig:half-analysis-it} shows the inference rules for \glspl{let} and their inner items.
The first rule, (Let), propagates the context in which the expression is evaluated, \(ctx\), directly to the \mzninline{in}-expression.
Thereafter, the analysis will continue by iterating over its inner items.
This is described using the newly introduced syntax \ctxitem{I}.
Note that the \(ctx\) of the let-expression itself, is irrelevant for the analysis of its inner items.
This is described using the syntax \ctxitem{I}.
Note that the \(ctx\) of the \gls{let} itself, is irrelevant for the analysis of its inner items.
The inference for \constraint{} items is described by the (Con) rule.
Since \microzinc{} implements strict semantics, the \constraint{} can be assumed to hold globally.
And, unlike \minizinc{}, the \constraint{} is not dependent on the context of the let-expression.
Since all expressions in well-formed \microzinc{} are total, the \constraint{} can be assumed to hold globally.
And, unlike \minizinc{}, the \constraint{} is not dependent on the context of the \gls{let}.
The \constraint{}'s expression is evaluated in \rootc{} context.
The (Assign) rule reasons about declarations that have a right hand side.
@ -550,7 +514,11 @@ It is, however, not always safe to do so.
For example, consider the following \microzinc{} fragment.
\begin{mzn}
constraint if b then F(x, y, z) else G(x, y, z) endif;
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.
@ -575,7 +543,7 @@ It is, however, not always safe to do so.
\end{example}
Using the \changepos{} transformation for sub-expression contexts is safe, but it places a large burden on the \solver{}.
The solver is likely to perform better when the direct constraint predicate is used.
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 array access or if-then-else expression we introduce the \mayberootc{} context.
This context functions as a \emph{weak} \rootc{} context.
@ -617,33 +585,34 @@ Looking back at \cref{ex:half-maybe-root}, these additional rules and updated jo
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}.
At compile time, this is only correct context to use.
We will, however, discuss the dynamically adjusting of contexts during flattening in \cref{subsec:half-dyn-context}.
We will, however, discuss the dynamically adjusting of contexts during \gls{rewriting} in \cref{subsec:half-dyn-context}.
\section{Flattening and Half Reification}%
\label{sec:half-flattening}
\section{Rewriting and Half Reification}%
\label{sec:half-rewriting}
During the flattening process the contexts assigned to the different expressions can be used directly to determine if and how a expression has to be reified.
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}.
\begin{example}
\label{ex:half-flatten}
\label{ex:half-rewriting}
\todo{Replace the previous example. It was too long and complex.}
\end{example}
A consequence of the use of \gls{half-reif}, shown in the example, is that it forms so called \emph{implication chains}.
This happens when the right hand side of an implication is half reifed and a new Boolean variable is created to represent the variable.
Instead, we could have directly posted the half-reified constraint using the left hand side of the implication as its control variable.
In \cref{subsec:half-compress} we present a new post-processing method, \emph{chain compression}, that can be used to eliminate these implication chains.
As shown in the example, the use of \gls{half-reif} can form so called \emph{implication chains}.
This happens when the right hand side of an implication is \gls{half-reified} and a \gls{cvar} is created to represent the expression.
Instead, we could have used the left hand side of the implication as the \gls{cvar} of the \gls{half-reified} \constraint{}.
In \cref{subsec:half-compress} we present a new post-processing method we call \emph{chain compression}.
It can be used to eliminate these implication chains.
The flattening with \gls{half-reif} also interacts with some of the optimisation methods used during the flattening process.
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 flattening process.
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.
\subsection{Chain compression}%
\label{subsec:half-compress}
As shown in \cref{ex:half-flatten}, flattening with half reification will in many cases result in implication chains: \mzninline{b1 -> b2 /\ b2 -> c}, where \texttt{b2} has no other occurrences.
In this case the conjunction can be replaced by \mzninline{b1 -> c} and \texttt{b2} can be removed from the model.
\Gls{rewriting} with \gls{half-reif} will in many cases result in implication chains: \mzninline{b1 -> b2 /\ b2 -> c}, where \texttt{b2} has no other occurrences.
In this case the conjunction can be replaced by \mzninline{b1 -> c} and \texttt{b2} can be removed from the \cmodel{}.
The case shown in the example can be generalised to
\begin{mzn}
@ -658,10 +627,11 @@ The case shown in the example can be generalised to
\noindent{}after which \texttt{b2} can be removed from the model.
An algorithm to remove these chains of implications is best visualised through the use of an implication graph.
An implication graph \(\tuple{V,E}\) is a directed graph where the vertices \(V\) represent the variables in the instance and an edge \((x,y) \in E\) represents the presence of an implication \mzninline{x -> y} in the instance.
Additionally, for the benefit of the algorithm, a vertex is marked when it is used in other constraints in the constraint model.
An implication graph \(\tuple{V,E}\) is a directed graph.
The vertices \(V\) represent the \variables{} in the \instance{}.
An edge \((x,y) \in E\) represents the presence of an implication \mzninline{x -> y} in the instance.
Additionally, for the benefit of the algorithm, is marked when it is used in other constraints in the constraint model.
The goal of the algorithm is now to identify and remove vertices that are not marked and have only one incoming edge.
\Cref{alg:half-compression} provides a formal specification of the chain compression method in pseudo code.
@ -674,86 +644,88 @@ The goal of the algorithm is now to identify and remove vertices that are not ma
\(V' \longleftarrow V\)\;
\(E' \longleftarrow E\)\;
\For{\(x \in V\)} {
\If{\(x \not\in M\) \textbf{ and }\(\left|\left\{(a,x)| (a,x) \in E\right\}\right| = 1\)}{
\(a \longleftarrow \text{how to bind??}\)\;
\For{\((x, b) \in E\)}{
\(E' \longleftarrow E' \cup \{ (a,b) \} \)\;
\(E' \longleftarrow E' \backslash \{ (x,b) \} \)\;
\For{\( x \in V \backslash{} M \)} {
\Switch{\( \left\{ a~|~(a,x) \in E \right\} \)}{
\Case{\( \left\{ a \right \} \)}{
\For{\((x, b) \in E\)}{
\(E' \longleftarrow E' \cup \{ (a,b) \} \)\;
\(E' \longleftarrow E' \backslash \{ (x,b) \} \)\;
}
\(E' \longleftarrow E' \backslash \{ (a,x) \} \)\;
\(V' \longleftarrow V' \backslash \{ x \} \)\;
}
\(E' \longleftarrow E' \backslash \{ (a,x) \} \)\;
\(V' \longleftarrow V' \backslash \{ x \} \)\;
}
}
\(G' \longleftarrow \tuple{V', E'}\)\;
\caption{\label{alg:half-compression} Implication chain compression algorithm}
\end{algorithm}
\todo{Correctly bind a}
The algorithm can be further improved by considering implied conjunctions.
These can be split up into multiple implications:
These can be split up into multiple implications.
\begin{mzn}
b -> forall(x in N)(x)
\end{mzn}
\noindent{}is equivalent to
The expression above is logically equivalent to the following expression.
\begin{mzn}
forall(x in N)(b -> x)
\end{mzn}
Adopting this transformation both simplifies a complicated constraint and possibly allows for the further compression of implication chains.
It should however be noted that although this transformation can result in an increase in the number of constraints, it generally increases the propagation efficiency.
Adopting this transformation both simplifies a complicated \constraint{} and possibly allows for the further compression of implication chains.
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.
The compiler must be able to tell if a variable is (only) a control variable 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 control variable for a reified conjunction and perform the transformation in this case.
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.
\subsection{Common Sub-expression Elimination}%
\label{subsec:half-cse}
When using full \gls{reif}, all \glspl{reif} are stored in the \gls{cse} table.
This ensure that if we see the same expression is reified twice, then the resulting \variable{} would be reusing.
This ensure that if the same expression is \gls{reified} twice, then the resulting \gls{reif} will be reused.
This avoids that the solver has to enforce the same functional relationship twice.
If the flattener uses \gls{half-reif}, in addition to full \gls{reif}, then \gls{cse} needs to ensure not just that the expressions are equivalent, but also that the context of the two expressions are compatible.
If the \gls{rewriting} uses \gls{half-reif}, in addition to full \gls{reif}, then \gls{cse} needs to ensure not just that the expressions are equivalent, but also that the context of the two expressions are compatible.
For example, if an expression was first found in a \posc{} context and later found in a \mixc{} context, then the resulting \gls{half-reif} from the first cannot be used for the second expression.
In general:
In general the following rules apply.
\begin{itemize}
\item The flattening result of a \posc{} context, a \gls{half-reif}, can only be reused if the same expression is again found in \posc{} context.
\item The result of \gls{rewriting} an expression in \posc{} context, a \gls{half-reif}, can only be reused if the same expression is again found in \posc{} context.
\item The flattening result of a \negc{} context, a \gls{half-reif} with its negation pushed inwards, can only be reused if the same expression is again found in \negc{} context.
\item The result of \gls{rewriting} an expression in \negc{} context, a \gls{half-reif} with its negation pushed inwards, can only be reused if the same expression is again found in \negc{} context.
\item The flattening result of a \mixc{} context, a \gls{reif}, can be reused in \posc{}, \negc{}, and \mixc{} context.
Since we assume that the result of a flattening an expression in \negc{} context pushes the negation inwards, the \gls{reif} does, however, need to be negated.
\item The result of \gls{rewriting} an expression in \mixc{} context, a \gls{reif}, can be reused in \posc{}, \negc{}, and \mixc{} context.
Since we assume that the result of a \gls{rewriting} an expression in \negc{} context pushes the negation inwards, the \gls{reif} does, however, need to be negated.
\item If the expression was already flattened in \rootc{} context, then any repeated usage of the expression can be assumed to take the value \mzninline{true} (or \mzninline{false} in \negc{} context).
\item If the expression was already seen in \rootc{} context, then any repeated usage of the expression can be assumed to take the value \mzninline{true} (or \mzninline{false} in \negc{} context).
\end{itemize}
When considering these compatibility rules, the result of flattening would be highly dependent on the order in which expressions are seen by the flattener.
When considering these compatibility rules, the result of \gls{rewriting} is highly dependent on the order in which expressions are seen.
It would always be better to encounter the expression in a context that results in a reusable expression, \eg{} \mixc{}, before seeing the same expression in another context, \eg{} \posc{}.
This avoids creating both a full \gls{reif} and a \gls{half-reif} of the same expression.
In the \microzinc{} interpreter, this problem is resolved by only keeping the result of their \emph{joint} context.
In the \microzinc{} \interpreter{}, this problem is resolved by only keeping the result of their \emph{joint} context.
The context recorded in the \gls{cse} table and the found context are joint using the join operator, as described in \cref{fig:half-join}.
If this context is different from the recorded context, then the expression is re-evaluated in the joint context and its result kept in the \gls{cse} table.
All usages of the previously recorded result is replaced by the new result.
Because of dependency tracking of the constraints that define variables, we can be sure that all \variables{} and \constraints{} created in defining the earlier version are correctly removed.
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.
This problem is solved by introducing a canonical form for expressions where negations can be pushed inwards.
In this form the result of flattening 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 half reified there already exists an \gls{half-reif} for its negation, then we instead evaluate the expression in mixed context, reifying the expression and replacing the existing half reified expression.
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.
The expression is \gls{reified} and replaces the existing \gls{half-reified} expression.
This canonical form for expressions and their negations can also be used for the expressions in other contexts.
Using the canonical form we can now also be sure that we never create a full \gls{reif} for both an expression and its negation.
Instead, when one is created, the negation of the resulting \variable{} can directly be used as the result of reifying its negation.
Instead, when one is created, the negation of the resulting \variable{} can directly be used as the \gls{reif} of its negation.
Moreover, this mechanism also allows us to detect when an expression and its negation occur in \rootc{} context.
This is simple way to detect conflicts between \constraints{} and, by extend, prove that the constraint model is unsatisfiable.
This is simple way to detect conflicts between \constraints{} and, by extend, prove that the \cmodel{} is \gls{unsat}.
Clearly, a \constraint{} and its negation cannot both hold at the same time.
\todo{This needs an example!!! To complex}
@ -761,8 +733,8 @@ Clearly, a \constraint{} and its negation cannot both hold at the same time.
\subsection{Dynamic Context Switching}%
\label{subsec:half-dyn-context}
In \cref{subsec:half-?root} we discussed the fact that the correct context of an expression is not always known when analysing a \microzinc{} model.
Its context depends on data that is only known at an instance level.
In \cref{subsec:half-?root} we discussed the fact that the correct context of an expression is not always known when analysing \microzinc{}.
Its context depends on data that is only known at an \instance{} level.
The same situation can be caused by \gls{propagation}.
\begin{example}
@ -775,8 +747,8 @@ 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}, propagation of \mzninline{b} will set it to the value \mzninline{true}.
This however means that the constraint is equivalent to
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}.
This however means that the \constraint{} is equivalent to the following \constraint{}.
\begin{mzn}
constraint 2*x = y;
@ -788,15 +760,15 @@ The same situation can be caused by \gls{propagation}.
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, on the other hand, the control \variable{} of a \gls{half-reif} is fixed, then either the context becomes \rootc{} or the constraint already holds.
Since regular \constraints{} are strongly preferred over any form of \gls{reif}, it is important to dynamically pick the correct form during the flattening process.
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 should introduce another layer of decomposition.
In this layer, it checks its control \variable{}.
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.
Otherwise, it behaves as it would have done normally.
The control \variable{} is thus used to communicate any change in context.
The \gls{cvar} is thus used to communicate the change in context.
\begin{example}
@ -822,24 +794,22 @@ The control \variable{} is thus used to communicate any change in context.
endif;
\end{mzn}
This new predicate can then compiled using the normal methods.
This new predicate can then be compiled using the normal methods.
\end{example}
\todo{Should we talk about \mixc{} that could have been \posc{}? I'm not sure we correctly do that one at the moment.}
\section{Experiments}
\label{sec:half-experiments}
We now present experimental evaluation of the presented \gls{half-reif} techniques.
First, to show the benefit of implementing propagators for half-reified constraint, we compare their performance against their decompositions.
We now present experimental evaluation of the presented techniques.
First, to show the benefit of implementing propagators for \gls{half-reified} \constraint{}, we compare their performance against their \glspl{decomp}.
To do this, we recreate two experiments presented by \textcite{feydy-2011-half-reif} in the original \gls{half-reif} paper in a modern \gls{cp} solver, \gls{chuffed}.
In the experiment, we use propagators implemented according to the principles described in this paper.
No new algorithm has been devised to perform the propagation.
The propagator of the original constraint is merely adjusted to influence and watch a control \variable{}.
In the experiment, we use \glspl{propagator} implemented according to the principles described in this paper.
No new algorithm has been devised to perform the \gls{propagation}.
The \gls{propagator} of the direct \constraint{} is merely adjusted to influence and watch a \gls{cvar}.
Additionally, we assess the effects of automatically detecting and introducing \glspl{half-reif} during the flattening process in general.
We flatten and solve 200 \minizinc{} instances for several \solvers{} with and without the use of \gls{half-reif}.
We then analyse the trends in the generated \flatzinc{} models and performance in solving the instances.
Additionally, we assess the effects of automatically detecting and introducing \glspl{half-reif} during the \gls{rewriting} process.
We rewrite and solve 200 \minizinc{} instances for several \solvers{} with and without the use of \gls{half-reif}.
We then analyse the trends in the generated \glspl{slv-mod} and their solving performance.
A description of the used computational environment, \minizinc{} instances, and versioned software has been included in \cref{ch:benchmarks}.
@ -847,27 +817,27 @@ A description of the used computational environment, \minizinc{} instances, and
\label{sec:half-exp-prop}
Our first experiment considers the \gls{qcp-max} quasi-group completion problem.
In this problem, we need to decide the value of an \((n \times n)\) matrix of integer \variables, with domains \mzninline{1..n}.
In this problem, we need to decide the value of an \((n \times n)\) matrix of integer \variables{}, with \domains{} \mzninline{1..n}.
The aim of the problem is to create as many rows and columns where all \variables{} take a unique value.
In each instance certain values have already been fixed.
It is, thus, not always possible for all rows and columns to contain only distinct values.
In each \instance{} certain values have already been 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 by reifying the \mzninline{all_different} constraint.
Since the goal of the problem is to maximise the number of \mzninline{all_different} \constraints{} that hold, these constraints are never forced to be \mzninline{false}.
This means these constraints in a \posc{} context and can be half-reified.
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 maximise the number of \mzninline{all_different} \constraints{} that hold, these \constraints{} are never forced to be \mzninline{false}.
This means these \constraints{} in a \posc{} context and can be \gls{half-reified}.
\Cref{tab:half-qcp} shows the comparison of two solving configurations in \gls{chuffed} for the \gls{qcp-max} problem.
The results are grouped based on their size of the instance.
For each group we show the number of instances solved by the configuration and the average time used for this process.
In our first configuration the half-reified \mzninline{all_different} \constraint{} is enforced using a newly created propagator.
This propagator is an adjusted version from the existing bounds consistent \mzninline{all_different} propagator in \gls{chuffed}.
The implementation of the propagator was already split into parts that \emph{check} the violation of the constraint and parts that \emph{prune} the \glspl{domain} of \variables{}.
In our first configuration the half-reified \mzninline{all_different} \constraint{} is enforced using a \gls{propagator}.
This \gls{propagator} is an adjusted version from the existing bounds consistent \mzninline{all_different} \gls{propagator} in \gls{chuffed}.
The implementation of the \gls{propagator} was already split into parts that check the violation of the constraint and parts that prune the \glspl{domain} of \variables{}.
Therefore, the transformation described in \cref{sec:half-propagation} can be directly applied.
Since \gls{chuffed} is a \gls{lcg} \solver{}, the explanations created by the 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 control variable to \mzninline{false} and the explanations given to prune a variable are appended by requirement that the control variable is \mzninline{true}.
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 decomposition:
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) =
@ -876,22 +846,22 @@ In our second configuration the \mzninline{all_different} constraint is enforced
);
\end{mzn}
The \mzninline{!=} constraints produced by this redefinition are reified.
Their conjunction, then represent the reification of the \mzninline{all_different} constraint.
The \mzninline{!=} \constraints{} produced by this redefinition are \gls{reified}.
Their conjunction, then represent the \gls{reif} of the \mzninline{all_different} \constraint{}.
\begin{table}
\begin{center}
\input{assets/table/half_qcp}
\caption{\label{tab:half-qcp} \gls{qcp-max} problems: number of solved instances and average time (in seconds) with a 300s timeout.}
\caption{\label{tab:half-qcp} \gls{qcp-max} problems: number of solved \instances{} and average time (in seconds) with a 300s timeout.}
\end{center}
\end{table}
The results in \cref{tab:half-qcp} show that the usage of the specialised propagator has a significant advantage over the use of the decomposition.
Although it only allows us to solve a single extra instance, there is a significant reduction in solving time for most instances.
Note that the qcp-15 instances are the only exception.
It appears that none of the instances in this group proved to be a real challenge to either method and we see similar solve times between the two methods.
The results in \cref{tab:half-qcp} show that the usage of the specialised \gls{propagator} has a significant advantage over the use of the \gls{decomp}.
Although it only allows us to solve a one extra instance, there is a significant reduction in solving time for most \instances{}.
Note that the qcp-15 \instances{} are the only exception.
It appears that none of the \instances{} in this group proved to be a real challenge to either method and we see similar solve times between the two methods.
For our second experiment we consider a variation on the prize collecting travelling salesman problem \autocite{balas-1989-pctsp} referred to as \emph{prize collecting path}.
In the problem we are given a graph with weighted edges, both positive and negative.
@ -899,35 +869,35 @@ The aim of the problem is to find the optimal acyclic path from a given start no
It is not required to visit every node.
In this experiment we can show how \gls{half-reif} can reduce the overhead of handling partial functions correctly.
The \minizinc{} model for this problem contains a unsafe array lookup \mzninline{pos[next[i]]}, where the domain of \mzninline{next[i]} is larger than the index set of \mzninline{pos}.
We compare safe decomposition of this \mzninline{element} constraint against a propagator of its \gls{half-reif}.
The decomposition creates a new variable that takes the value of the index only when it is within the index set of the array.
The \minizinc{} model for this problem contains a unsafe array lookup \mzninline{pos[next[i]]}, where the \domain{} of \mzninline{next[i]} is larger than the index set of \mzninline{pos}.
We compare safe \gls{decomp} of this \mzninline{element} \constraint{} against a \gls{propagator} of its \gls{half-reif}.
The \gls{decomp} creates a new \variable{} that takes the value of the index only when it is within the index set of the array.
Otherwise, it will set its surrounding context to \mzninline{false}.
The \gls{half-reif} implicitly performs the same task by setting its control \variable{} to \mzninline{false} whenever the result of the \mzninline{element} constraint does not match the value of the index variable.
Again, for the implementation of the propagator of the \gls{half-reif} constraint we adjust the regular propagator as described above.
The \gls{half-reif} implicitly performs the same task by setting its \gls{cvar} to \mzninline{false} whenever the result of the \mzninline{element} constraint does not match the value of the index variable.
Again, for the implementation of the \gls{propagator} of the \gls{half-reif} constraint we adjust the direct \gls{propagator} as described above.
\begin{table}
\begin{center}
\input{assets/table/half_prize}
\caption{\label{tab:half-prize} Prize collecting paths: number of solved instances and average time (in seconds) and with a 300s timeout.}
\caption{\label{tab:half-prize} Prize collecting paths: number of solved \instances{} and average time (in seconds) and with a 300s timeout.}
\end{center}
\end{table}
The results of the experiment are shown in \cref{tab:half-prize}.
Although the performance on smaller instances is similar, the dedicated propagator consistently outperforms the usage of the decomposition.
The difference in performance becomes more pronounced in the bigger instances.
In the 32-4-8 group, we even see that usage of the propagator allows us to solve an additional three instances.
Although the performance on smaller \instances{} is similar, the dedicated \gls{propagator} consistently outperforms the usage of the \gls{decomp}.
The difference in performance becomes more pronounced in the bigger \instances{}.
In the 32-4-8 group, we even see that usage of the \gls{propagator} allows us to solve an additional three \instances{}.
\subsection{Flattening with Half Reification}
\label{sec:half-exp-flatten}
\subsection{Rewriting with Half Reification}
\label{sec:half-exp-rewriting}
The introduction of automated context analysis and introduction of \glspl{half-reif} allows us to evaluate the usage of \gls{half-reif} on a larger scale.
In our second experiment we assess its effects on the flattening and solving of the instances of the 2019 and 2020 \minizinc{} challenge \autocite{stuckey-2010-challenge,stuckey-2014-challenge}.
These experiments are conducted using the \gls{gecode} \solver{}, which has propagators for \glspl{half-reif} of many basic \constraints{}, and \minizinc{}'s linearisation library, which has been adapted to use \gls{half-reif} as earlier described.
The \minizinc{} instances are flattened using the \minizinc{} 2.5.5 flattener, which can enable and disable the usage of \gls{half-reif}.
The solving of the linearised models is tested using the \gls{cbc} and \gls{cplex} \gls{mip} \solvers{}.
The usage of context analysis and introduction of \glspl{half-reif} allows us to evaluate the usage of \gls{half-reif} on a larger scale.
In our second experiment we assess its effects on the \gls{rewriting} and solving of the \instances{} of the 2019 and 2020 \minizinc{} challenge \autocite{stuckey-2010-challenge,stuckey-2014-challenge}.
These experiments are conducted using the \gls{gecode} \solver{}, which has propagators for \glspl{half-reif} of many basic \constraints{}, and \minizinc{}'s \gls{linearisation} library, which has been adapted to use \gls{half-reif} as earlier described.
The \minizinc{} instances are rewritten using the \minizinc{} 2.5.5 \compiler{}, which can enable and disable the usage of \gls{half-reif}.
The solving of the linearised \instances{} is tested using the \gls{cbc} and \gls{cplex} \gls{mip} \solvers{}.
\todo{TODO:\ Extend this section with the \gls{sat} results once they are run.}
@ -944,46 +914,46 @@ The solving of the linearised models is tested using the \gls{cbc} and \gls{cple
\input{assets/table/half_flat_sat}
\caption{\label{subtab:half-flat-bool}Booleanisation library}
\end{subtable}
\caption{\label{tab:half-flattening} Cumulative statistics of flattening all \minizinc{} instances from \minizinc{} Challenge 2019 \& 2020 (200 instances).}
\caption{\label{tab:half-rewrite} Cumulative statistics of \gls{rewriting} all \minizinc{} \instances{} from \minizinc{} challenge 2019 \& 2020 (200 \instances{}).}
\end{table}
Grouped by \solver{} library and whether \gls{half-reif} is used, \cref{tab:half-flattening} shows several cumulative figures from the flattening process of the \minizinc{} challenge.
Grouped by \solver{} library and whether \gls{half-reif} is used, \cref{tab:half-rewrite} shows several cumulative figures from the \gls{rewriting} process of the \minizinc{} challenge.
These are:
\begin{itemize}
\item The number of \emph{constraints} in \flatzinc{}.
\item The number of \emph{\glspl{reif}} evaluated during the flattening process.
\item The number of \emph{\glspl{reif}} evaluated during the \gls{rewriting} process.
This includes both the \glspl{reif} that are decomposed and the \glspl{reif} that are present in the \flatzinc{}.
\item The number of \emph{\glspl{half-reif}} evaluated during the flattening process.
\item The number of \emph{\glspl{half-reif}} evaluated during the \gls{rewriting} process.
\item The number of \emph{implications removed} using the chain compression method.
\item The runtime of the flattening process (\ie{} the \emph{flattening time}).
\item The runtime of the \gls{rewriting} process.
\end{itemize}
The flattening statistics for the \gls{gecode} \solver{} library, shown in \cref{subtab:half-flat-gecode}, show significant changes in the resulting \flatzinc{}.
The \gls{rewriting} statistics for the \gls{gecode} \solver{} library, shown in \cref{subtab:half-flat-gecode}, show significant changes in the resulting \flatzinc{}.
Although the total number of constraints remains stable, we see that well over half of all \glspl{reif} are replaced by \glspl{half-reif}.
This replacement happens mostly 1-for-1; the difference between the number of \glspl{half-reif} introduced and the number of \glspl{reif} reduced is only 20. In comparison, the number of implications removed by chain compression looks small, but this number is highly dependent on the \minizinc{} model.
In many models, no implications can be removed, but for some problems an implication is removed for every \gls{half-reif} that is introduced.
Finally, the overhead of the introduction of \gls{half-reif} and the newly introduced optimisation techniques is minimal.
The \Cref{subtab:half-flat-lin} paints an equally positive picture for the usage of \glspl{half-reif} for linearisation.
Since both \glspl{reif} and \glspl{half-reif} are decomposed during the flattening process, the usage of \gls{half-reif} is able to remove almost 7.5\% of the overall constraints.
Since both \glspl{reif} and \glspl{half-reif} are decomposed during the \gls{rewriting} process, the usage of \gls{half-reif} is able to remove almost 7.5\% of the overall constraints.
The ratio of \glspl{reif} that is replaced with \glspl{half-reif} is not as high as \gls{gecode}.
This is caused by the fact that the linearisation process requires full \gls{reif} in the decomposition of many \glspl{global}.
Similar to \gls{gecode}, the number of implications that is removed is dependent on the problem.
Lastly, the flattening time slightly increases for the linearisation process.
Lastly, the \gls{rewriting} time slightly increases for the linearisation process.
Since there are many more constraints, the introduced optimisation mechanisms have an slightly higher overhead.
\todo{The \gls{sat} statistics currently only include 2019. 2020 is still WIP.}
Finally, statistics for the flattening the instances is shown in \cref{subtab:half-flat-bool}.
Finally, statistics for the \gls{rewriting} the instances is shown in \cref{subtab:half-flat-bool}.
Like linearisation, the usage of \gls{half-reif} significantly reduces number of constraints and \glspl{reif}.
Different, however, is that the booleanisation library is explicitly defined in terms of \glspl{half-reif}.
Some \constraints{} manually introduce \mzninline{_imp} call as part of their definition.
Furthermore, the usage of chain compression does not seem to have any effect.
Since all \glspl{half-reif} are defined in terms of clauses, the implications normally removed using chain compression are instead aggregated into bigger clauses.
Surprisingly, the usage of \gls{half-reif} also reduces the flattening time as it reduces the workload.
Surprisingly, the usage of \gls{half-reif} also reduces the \gls{rewriting} time as it reduces the workload.
\begin{table}
\input{assets/table/half_mznc}

34
chapters/4_half_reif_preamble.tex
View File

@ -1,16 +1,22 @@
\noindent{}\textcite{feydy-2011-half-reif} introduced the notion of \gls{half-reif}\todo{You need an example of what half reification is b -> c !!!} as an improvement over the use of \gls{reif}.
They show that some of the problems and expenses of the use of \gls{reif} can be mitigated using this technique.
In addition, the creation of propagators for \glspl{half-reif} of constraints can often be an easy process.
It is not always possible, however, to use a \gls{half-reif} instead of a \gls{reif}.
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.
Crucially, this algorithm does \emph{not} directly generalize to the full \minizinc{} language.
The chosen subset omits let-expressions, which can complicate the process.
An identifier for the same expression can suddenly occur in multiple locations.
\noindent{}Choosing if a \gls{reif} \(\texttt{b} \leftrightarrow{} c\) for a \constraint{} \(c\) has to be introduced 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 requires significantly more effort from the \solver{} than merely enforcing it.
A \gls{reified} \constraint{} results in a larger \gls{decomp} or a more complex \gls{native} \constraint{}.
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}.
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 \textcite{feydy-2011-half-reif}.
An additional benefit of \gls{half-reif} is that its decomposition can be significantly smaller than the decomposition of a \gls{reif}.
\Cref{sec:half-decomposition} shows the benefits of \gls{half-reif} when writing decompositions for \gls{mip} and \gls{sat} \solvers{}.
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}.
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 generalize to the full \minizinc{} language.
This chapter re-evaluates the usage of \gls{half-reif} and extends the \gls{rewriting} process to fully support \gls{half-reif} in \minizinc{}.
This chapter is organised as follows.
In \cref{sec:half-intro,sec:half-propagation} we introduce the core concepts of \gls{half-reif} and \glspl{propagator} for \gls{half-reified} \constraints{}, as discussed by \textcite{feydy-2011-half-reif}.
An additional benefit of \gls{half-reif} is that its \gls{decomp} can be significantly smaller than the \gls{decomp} of a \gls{reif}.
\Cref{sec:half-decomposition} shows the benefits of \gls{half-reif} when writing \glspl{decomp} 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 extension \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}.
Then, in \cref{sec:half-rewriting}, we elaborate on how the usage of \gls{half-reif} changes the \gls{rewriting} process.
Finally, the effects of \glspl{propagator} for \gls{half-reified} \constraints{} and the automatic introduction of \gls{half-reif} is analysed in \cref{sec:half-experiments}.