Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
This repository has been archived on 2025-03-06. You can view files and clone it, but cannot push or open issues or pull requests.
dekker-phd-thesis/chapters/4_half_reif.tex

1144 lines
67 KiB
TeX
Raw Blame History

%************************************************
\chapter{Reasoning about Reification}\label{ch:half-reif}
%************************************************
\glsreset{half-reif}
\glsreset{half-reified}
\glsreset{reif}
\glsreset{reified}
\input{chapters/4_half_reif_preamble}
\section{An Introduction to Half-Reification}
\label{sec:half-intro}
The complex expression language used in \cmls{}, such as \minizinc{}, often requires the use of \gls{reif} in order to arrive at 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.
We call \mzninline{b} the \gls{cvar} of the expression.
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 using \gls{reif} in the \gls{rewriting} process is well-understood, it suffers from certain weaknesses.
\begin{itemize}
\item Many \glspl{reif} are created in the \gls{rewriting} of \gls{partial} function calls to accommodate \minizinc{}'s \glspl{rel-sem}.
\item \Glspl{propagator} for the \glspl{reif} of \glspl{global} are scarce.
\end{itemize}
As an alternative, the authors introduce \gls{half-reif}.
It follows from the idea that in many cases it is sufficient to use the logical implication of an expression, \mzninline{b -> pred(...)}, instead of the logical equivalence, \mzninline{b <-> pred(...)}.
\Gls{rewriting} with \gls{half-reif} is an approach that improves upon all these weaknesses of \gls{rewriting} with ``full'' \gls{reif}.
\begin{itemize}
\item \Gls{rewriting} using \glspl{half-reif} can lead to significantly better \glspl{slv-mod} when translating \gls{partial} function calls.
\item \Glspl{propagator} for \glspl{half-reif} can usually be constructed by merely altering a \gls{propagator} implementation for its non-\gls{reified} \constraint{}.
\end{itemize}
Additionally, for many \solvers{} the \gls{decomp} of a \gls{reif} is more complex than the \gls{decomp} of a \gls{half-reif}.
We will show that using \glspl{half-reif} can therefore lead to a reduction in \gls{native} \constraints{} in the \gls{slv-mod}.
\Gls{half-reif} can be used instead of full \gls{reif} when the resulting \gls{cvar} can never be forced to be false.
This requirement follows from the difference between implication and logical equivalences.
Setting the left-hand side of an implication to false does not influence the value on the right-hand side.
This is why the \gls{cvar} should never be forced to be false, since this would not enforce the negation of the \constraint{}.
Setting the right-hand side of an implication to true also does not influence the left-hand side.
This is, however, not an issue since in this case the value can just be assigned by the \gls{propagation} of other \constraints{} or a \gls{search-decision}.
\begin{example}
For example, \gls{half-reif} can be used in the following disjunction.
\begin{mzn}
constraint (x = 5) \/ (y = 5);
\end{mzn}
This \constraint{} forces that, between \mzninline{x} and \mzninline{y}, at least one \variable{} is takes the value five.
The usual \gls{rewriting} would result in the following (intermediate) model, using \glspl{reif} for the equalities.
\begin{mzn}
var bool: b1;
var bool: b2;
constraint b1 <-> (x = 5);
constraint b2 <-> (y = 5);
constraint b1 \/ b2;
\end{mzn}
However, independent of the value of \mzninline{b1}, if \mzninline{b2} takes the value true, then it can never make the disjunction false.
Therefore, \mzninline{propagation} of the disjunction can never force \mzninline{b2} to take the value false.
Consequently, this means using \gls{half-reif} is \gls{eqsat}.
\Gls{rewriting} using \gls{half-reif} will result in the following model.
\begin{mzn}
var bool: b1;
var bool: b2;
constraint b1 -> (x = 5);
constraint b2 -> (y = 5);
constraint b1 \/ b2;
\end{mzn}
\end{example}
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 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}
Making the left-hand side of the \constraint{} bigger will only ever help satisfy the \constraint{}.
This means \mzninline{propagation} of the expressions \mzninline{x = 5} can never force them to take the value false.
The \gls{rewriting} process can thus use \glspl{half-reif} instead of \glspl{reif} for these expressions.
\end{example}
To systematically analyse whether Boolean expressions can be \gls{half-reified}, we study the \emph{monotonicity} of \constraints{} \wrt{} an expression.
A relation \( r( a_{n}, \ldots{}, a_{i}, \ldots{} , a_{m}) \) is said to be \emph{monotone} \wrt{} its argument \(a_{i}\) when given two possible values for \(a_{i}\), \(x\) and \(y\), if \(x > y\), then \(r( a_{n}, \ldots{}, x, \ldots{} , a_{m}) \geq{} r( a_{n}, \ldots{}, y, \ldots{} , a_{m})\), independent of other arguments.
Contrariwise, a relation \( r( a_{n}, \ldots{}, a_{i}, \ldots{} , a_{m}) \) is said to be \emph{antitone} \wrt{} its argument \(a_{i}\) if given two possible values for \(a_{i}\), \(x\) and \(y\), if \(x > y\), then \(r( a_{n}, \ldots{}, x, \ldots{} , a_{m}) \leq{} r( a_{n}, \ldots{}, y, \ldots{} , a_{m}) \), independent of the other arguments.
Where, for clarification, we assume \( \text{false} < \text{true} \).
Using these definitions, we introduce extra distinctions in the context of expressions.
Before, we would merely distinguish between \rootc{} context and non-\rootc{} context.
Now, we will categorize the latter into the following three contexts.
\begin{description}
\item[\posc{}] An expression is in \posc{} context when the enclosing \constraint{} (in \rootc{} context) is \textbf{monotone} \wrt{} the expression.
\item[\negc{}] An expression is in \negc{} context when the enclosing \constraint{} (in \rootc{} context) is \textbf{antitone} \wrt{} the expression.
\item[\mixc{}] An expression is in \mixc{} context when the enclosing \constraint{} (in \rootc{} context) it is \textbf{neither} monotone, nor antitone \wrt{} the expression.
\end{description}
Determining the monotonicity of a \constraint{} \wrt{} an expression is a hard problem.
An expression might be monotone or antitone only through complex interactions, possibly through unknown \gls{native} \constraints{}.
Therefore, for our analysis, we slightly relax these definitions.
We say an expression is in \mixc{} context when it cannot be determined whether its enclosing \constraint{} is monotone or antitone \wrt{} the expression.
Expressions in \posc{} context are the ones we discussed before.
A Boolean expression in \posc{} context cannot be forced to be false.
As such, the\gls{half-reif} can be used for expressions in \posc{} context.
Although expressions in a \negc{} context cannot be directly \gls{half-reified}, the negation of an expression in a \negc{} context can be \gls{half-reified}.
\begin{example}
Consider, for example, the following \constraint{}.
\begin{mzn}
constraint b \/ not (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 then also negates the context to \posc{}.
Our example can be transformed into the following \constraint{}.
\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 that are in this context.
\begin{example}
An example of a \constraint{} that introduces \mixc{} contexts is the following.
\begin{mzn}
constraint (x = 5) xor (y = 5);
\end{mzn}
This \constraint{} forces either \mzninline{x} or \mzninline{y}, but not both, to take the value five.
The equalities in this constraint are in \mixc{} context, because whether \mzninline{y} can and must take the value 5 now directly depends on if \mzninline{x} has already taken the value five, and vice versa.
As such, when \mzninline{x} takes the value five it forces \mzninline{y} to not take the value five.
This means we cannot use a \gls{half-reif}, since it does not enforce the negated \constraint{}
\end{example}
\section{Propagation and Half-Reification}%
\label{sec:half-propagation}
Logically, there are three tasks that a \gls{propagator} for any \constraint{} must perform:
\begin{enumerate}
\item \(check\) whether the \constraint{} can still be satisfied (and otherwise declare the current state \gls{unsat}),
\item \(prune\) values from the \glspl{domain} of \variables{} that would violate\glsadd{violated} the \constraint{}, and
\item check whether the \constraint{} is \(entailed\) (\ie{}, proven to be \gls{satisfied}).
\end{enumerate}
When creating a \gls{propagator} for the \gls{half-reif} of a \constraint{}, it can be constructed from these tasks.
The \gls{half-reified} \gls{propagator} is dependent on an additional argument \(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 true, or it can be assigned false.
Given \(check\), \(prune\), \(entailed\), and \(b\) \cref{alg:half-prop} shows pseudocode for the \gls{propagation} of the \gls{half-reif} of the \constraint{}.
\begin{algorithm}[t]
\KwIn{The functions \(check\), \(prune\), and \(entailed\) that form the for non-\gls{reified} propagator of \constraint{} \(c\) and a Boolean \gls{cvar} \(b\).
}
\KwResult{This pseudocode propagates the \gls{half-reif} of \(c\) (\ie{} \(b \implies\ c\)) and returns whether the \constraint is entailed.}
\BlankLine{}
\If{\(b \text{ is unassigned}\)}{
\If{\(\neg{}check()\)}{
\(b \longleftarrow \text{false}\)\;
\Return{} \(\text{true}\)\;
}
}
\If{\(\texttt{b} = \text{true}\)}{
\(prune()\)\;
\Return{} \(entailed()\)\;
}
\Return{} \(\text{false}\)\;
\caption{\label{alg:half-prop} \gls{propagation} pseudocode for the \gls{half-reif} of a \constraint{} \(c\), based on the \gls{propagator} for \(c\).}
\end{algorithm}
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, \glspl{propagator} do not explicitly define \(check\) as a separate step.
Instead, this process can be implicit.
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{}.
In comparison, a \gls{propagator} for the \gls{reif} of \(c\) cannot be created from these three logical task.
In addition, we require the logical task from a \gls{propagator} of \(\neg{} c\): \(checkNeg\), \(pruneNeg\), and \(entailedNeg\).
Using these additional functions, we can define an algorithm for the \gls{propagator}, shown in \cref{alg:reif-prop}
Although this might seem reasonable for small \constraints{}, such as integer equality, for many \glspl{global} their negation is hard to define.
\todo{Insert good example of global constraint.}
\begin{algorithm}[t]
\KwIn{The functions \(check\), \(prune\), and \(entailed\) that form the for non-\gls{reified} propagator of \(c\), The functions \(checkNeg\), \(pruneNeg\), and \(entailedNeg\) that form the for non-\gls{reified} \gls{propagator} of \(\neg{} c\), and a Boolean \gls{cvar} \(b\).
}
\KwResult{This pseudocode propagates the \gls{reif} of \(c\) (\ie{} \(b \leftrightarrow{} c\)) and returns whether the \constraint{} is entailed.}
\BlankLine{}
\If{\(b \text{ is unassigned}\)}{
\If{\(\neg{} check()\)}{
\(b \longleftarrow \text{false}\)\;
}
\If{\(\neg{} checkNeg()\)}{
\(b \longleftarrow \text{true}\)\;
}
}
\If{\(\texttt{b} = \text{true}\)}{
\(prune()\)\;
\Return{} \(entailed()\)\;
}
\If{\(\texttt{b} = \text{false}\)}{
\(pruneNeg()\)\;
\Return{} \(entailedNeg()\)\;
}
\Return{} \(\text{false}\)\;
\caption{\label{alg:reif-prop} \Gls{propagation} pseudocode for the \gls{reif} of a \constraint{} \(c\), based on the \glspl{propagator} for \(c\) and \(\neg{} c\).}
\end{algorithm}
\Gls{half-reified} \glspl{propagator} have certain advantages over \gls{reified} \glspl{propagator}, but also may suffer certain penalties.
\Gls{half-reif} can cause \glspl{propagator} that use their \gls{cvar} 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 can be advantageous, but has a corresponding disadvantage.
When a \gls{cvar} is fixed, it can allow the simplification of the \glspl{propagator} that use them, and hence make \gls{propagation} faster.
When a full \gls{reif} is required, we can still use \gls{half-reified} \glspl{propagator} to implement it.
A full \gls{reif} \mzninline{x <-> pred(...)} can be propagated using its \gls{half-reified} \gls{propagator}, \mzninline{x -> pred(...)}, the \gls{half-reified} \gls{propagator} of its negation, \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 \glspl{propagator} for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element} based on these principles.
\section{Decomposition and Half-Reification}%
\label{sec:half-decomposition}
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 have to implement the negation of the \constraint{}, and can therefore often be much more compact than the fully \gls{reified} version.
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 implications is required.
\begin{example}
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 linearized.
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 \gls{half-reified}, then the \gls{linearization} could be simplified to only the first \constraint{}.
\end{example}
The same principle can be applied all throughout the \gls{linearization} process.
Ultimately, \minizinc{}'s \gls{linearization} library rewrites most \glspl{reif} in terms of implied less than or equal to \constraints{}.
For all these \glspl{reif}, replacement by a \gls{half-reif} can remove half of the implications.
For \gls{sat} solvers, a \gls{decomp} for a \gls{half-reif} can be created from its regular \gls{decomp}.
Any \constraint{} \(c\) will decompose 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} \]
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 \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} \]
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, \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}
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.
\begin{mzn}
constraint let {
var bool: x = pred(a, b, c);
} in y -> x /\ x -> z;
\end{mzn}
The result of 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 on 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 \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 use \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.
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 \glspl{rel-sem} for partial functions.
This means that if the result of a function is undefined, then its nearest enclosing Boolean expression becomes 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 partiality context is the context in which this condition is placed.
\begin{example}
We can illustrate the difference between the two contexts in the following \minizinc{} fragment.
\begin{mzn}
var 0..10: x
constraint b \/ y div x < 4;
\end{mzn}
In this fragment, we study the context of the division expression \mzninline{y div x}.
The expression itself return an integer \variable{}, and it used on the left-hand side of a less than \constraint{}.
This result is therefore in a \negc{} context: it is only forced to take a smaller value.
This is its value context.
However, since the \domain{} of \mzninline{x} includes zero, \gls{rewriting} \mzninline{x div y} will introduce the condition under which its result can be used.
In this case, the expression \mzninline{x != 0} is added to the right-hand side of the disjunction as follows.
\begin{mzn}
var 0..10: x
constraint b \/ ( x != 0 /\ y div x < 4);
\end{mzn}
\noindent{}The partiality context of the division is the context in which this condition is added.
Here, the condition is added in a \posc{} context.
\end{example}
\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{}.
It requires knowledge about all usages of each \variable{} at the same time.
This information is not available during the interpretation of \microzinc{}.
Without loss of generality we can define the context analysis process for \microzinc{} models.
This has the advantage that \microzinc{} does not contain \gls{partial} function calls.
The partiality in \minizinc{} has already been translated using only total functions (see \cref{sec:rew-micronano}).
The context analysis therefore does not have to keep track of value and partiality contexts separately.
We describe the context analysis performed on the \microzinc{} syntax in the form of inference rules.
The full set of rules appears in \cref{fig:half-analysis-expr,fig:half-analysis-it}.
Each rule describes how an expression that is found in a context \(ctx\), above the line, changes the context of subordinate expressions, below the line.
The syntax \ctxeval{e}{ctx} is used to assert that the expression \(e\) is evaluated in the context \(ctx\).
We now specify two context transformations that will be used in further algorithms to transition between different contexts: \changepos{} and \changeneg{}.
The behaviour of these transformations is shown in \cref{fig:half-ctx-trans}.
\begin{figure*}
\begin{center}
\begin{tabular}{ccc}
\(
\begin{array}{lcl}
\changepos \rootc & = & \posc \\
\changepos \posc & = & \posc \\
\changepos \negc & = & \negc \\
\changepos \mixc & = & \mixc
\end{array}
\)
& ~ &
\(
\begin{array}{lcl}
\changeneg \rootc & = & \negc \\
\changeneg \posc & = & \negc \\
\changeneg \negc & = & \posc \\
\changeneg \mixc & = & \mixc
\end{array}
\)
\end{tabular}
\end{center}
\caption{\label{fig:half-ctx-trans} Definitions of the \changepos{} and \changeneg{} context transitions.}
\end{figure*}
\begin{figure*}
\centering
\begin{prooftree}
\hypo{\ctxeval{x}{ctx}}
\infer1[(Ident)]{\text{pushCtx}(x, ctx)}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxeval{ident\texttt{(} e_{1}, \ldots, e_{n} \texttt{)}}{ctx}}
\hypo{\text{argCtx}(ident, ctx) = \tuple{ ctx'_{1}, \ldots, ctx'_{n}}}
\infer2[(Call)]{\ctxfunc{ident}{ctx},~\ctxeval{e_{1}}{ctx'_{1}},~\ldots,~ \ctxeval{e_{n}}{ctx'_{n}}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxeval{x\texttt{[}i\texttt{]}}{ctx}}
\infer1[(Access)]{\ctxeval{x}{\changepos{}ctx}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxeval{\texttt{if }b\texttt{ then } e_{1} \texttt{ else } e_{2} \texttt{ endif}}{ctx}}
\infer1[(ITE)]{\ctxeval{b}{ctx},~\ctxeval{e_{1}}{\changepos{}ctx},~\ctxeval{e_{2}}{\changepos{}ctx}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxeval{\texttt{[}e~\texttt{|}~G\texttt{]}}{ctx}}
\infer1[(Compr)]{\ctxeval{e}{ctx}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxeval{\texttt{[}e_{1}, \ldots, e_{n}\texttt{]}}{ctx}}
\infer1[(Arr)]{\ctxeval{e_{1}}{ctx}, \ldots, \ctxeval{e_{n}}{ctx}}
\end{prooftree}
\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 \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.
Most changes in the context of \microzinc{} expressions stem from the (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.}
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 \glspl{annotation}, 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.
It may be possible to infer these \glspl{annotation} from the function body.
However, we currently do not provide such analysis and annotate functions by hand.
\begin{example}
Consider the user-defined \minizinc{} implementation of a logical implication in \cref{lst:half-impli}.
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 terms of context analysis, this function now is equivalent to the \minizinc{} operator.
\end{example}
\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}
\begin{algorithm}
\KwIn{A \minizinc{} operator \(op\) and calling context \(ctx\)}
\KwOut{A tuple containing the contexts of the arguments \(\tuple{ctx_{1}, \ldots{}, ctx_{n}}\)}
\Switch{op}{
\Case{\mzninline{ not }}{
\Return{\tuple{\changeneg{}ctx}}
}
\Case{\mzninline{ \/ }, \mzninline{+ }}{
\Return{\tuple{\changepos{}ctx, \changepos{}ctx}}
}
\Case{\mzninline{ -> }, \mzninline{< }, \mzninline{<= }}{
\Return{\tuple{\changeneg{}ctx, \changepos{}ctx}}
}
\Case{\mzninline{ > }, \mzninline{>= }, \mzninline{- }}{
\Return{\tuple{\changepos{}ctx, \changeneg{}ctx}}
}
\Case{\mzninline{ <-> }, \mzninline{= }, \mzninline{xor }, \mzninline{* }}{
\Return{\tuple{\mixc, \mixc}}
}
\Case{\mzninline{ /\ }}{
\Return{\tuple{ctx, ctx}}
}
\Other{
\Return{\tuple{\mixc, \ldots, \mixc}}
}
}
\caption{\label{alg:arg-ctx} Definition of the ``argCtx'' function for \minizinc\ operators.}
\end{algorithm}
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 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.
\begin{description}
\item[\posc] \glspl{half-reif} can be defined as \(ident\)\mzninline{_imp}.
\item[\negc] negations of \glspl{half-reif} can be defined as \(ident\)\mzninline{_imp_neg}.
\item[\mixc] \glspl{reif} can be defined as \(ident\)\mzninline{_reif}.
\end{description}
\item If \(ident\) is a \microzinc{} function with an expression body \(E\), then a copy of the function can be made that is evaluated in the desired context: \ctxeval{E}{ctx}.
\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 there is no definition for the \gls{reif} of a \constraint{}, \ie{} neither a \gls{native} constraint nor a \gls{decomp}.
\end{enumerate}
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.
We will revisit this issue in \cref{subsec:half-?root}.
Finally, the (Compr) and (Arr) rules show simple inference rules for \gls{array} construction expressions.
If such an expression is evaluated in the context \(ctx\), then its members can be evaluated in the same context \(ctx\).
\begin{figure*}
\centering
\begin{prooftree}
\hypo{\ctxeval{\texttt{let \{ }I\texttt{ \} in } e}{ctx}}
\infer1[(Let)]{\ctxeval{e}{ctx}, \ctxitem{I} }
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxitem{I \texttt{; constraint } e }}
\infer1[(Con)]{\ctxeval{e}{\rootc},~\ctxitem{I}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxitem{I \texttt{; } T: x \texttt{ = } e }}
\hypo{\text{collectCtx}(x) = [ctx_{1}, \ldots, ctx_{n}]}
\infer2[(Assign)]{\ctxeval{e}{\text{join}([ctx_{1}, \ldots, ctx_{n}])},~\ctxitem{I}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxitem{I \texttt{; } \texttt{tuple(}\ldots\texttt{):}~x \texttt{ = (} e_{1}, \ldots, e_{n}\texttt{)}}}
\hypo{\text{collectCtx}(x) = \tuple{ctx_{1}, \ldots, ctx_{n}}}
\infer2[(TupC)]{\ctxeval{e_{1}}{ctx_{1}}, \ldots, \ctxeval{e_{n}}{ctx_{n}}, ~\ctxitem{I}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxitem{I \texttt{; (} T_{1}: x_{1}, \ldots, T_{n}: x_{n} \texttt{) = } e }}
\infer[no rule]1{\text{collectCtx}(x_{1}) = [ctx^{1}_{1}, \ldots, ctx^{1}_{k}], \ldots, \text{collectCtx}(x_{n}) = [ctx^{n}_{1}, \ldots, ctx^{n}_{l}]}
\infer1[(TupD)]{\ctxeval{e}{\tuple{\text{join}\left(\left[ctx^{1}_{1}, \ldots, ctx^{1}_{k}\right]\right), \ldots, \text{join}\left(\left[ctx^{n}_{1}, \ldots, ctx^{n}_{l}\right]\right)}},~\ctxitem{I}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxitem{I \texttt{; } T: x}}
\infer1[(Decl)]{}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxitem{\epsilon{}}}
\infer1[(Item0)]{}
\end{prooftree}
\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 \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 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 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.
The expression that is assigned to the identifier must be evaluated in the combined context of its usages.
As previously discussed, the contexts in which the identifier was used can be retrieved using the ``collectCtx'' function.
These contexts are then combined using a ``join'' function.
This function repeatedly applies the symmetric join operation described by \cref{fig:half-join}.
The right-hand expression of the item is then evaluated in the resulting context.
\begin{figure*}
\begin{center}
\begin{tabular}{r | c c c c}
join & \rootc & \posc & \negc & \mixc \\
\hline
\rootc & \rootc & \rootc & \rootc & \rootc \\
\posc & \rootc & \posc & \mixc & \mixc \\
\negc & \rootc & \mixc & \negc & \mixc \\
\mixc & \rootc & \mixc & \mixc & \mixc \\
\end{tabular}
\end{center}
\caption{\label{fig:half-join} A table showing the result of joining two contexts.}
\end{figure*}
(TupC) and (TupD) handle the context inference during the construction and destructuring of tuples respectively.
The context of the individual members of tuples is tracked separately.
This means that individual members of a tuple, like the value and the partiality of a \minizinc{} expression, may be evaluated in different contexts.
Finally, the (Decl) and (Item0) rules describe two base cases in the inference.
The declaration item of a \variable{} does not further affect the context, and does not depend on it.
It merely triggers the creation of a new \variable{}.
The (Item0) rule is triggered when there are no more inner items in the let-expression.
\subsection{Potentially Root}%
\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 \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}
\label{ex:half-maybe-root}
For example, consider the following \microzinc{} fragment.
\begin{mzn}
constraint if b then
F(x, y, z)
else
G(x, y, z)
endif;
\end{mzn}
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 be 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.
Consider the following \microzinc{} fragment.
\begin{mzn}
let {
var bool: p = F(x, y, z);
var bool: q = G(x, y, z);
constraint if b then p else q endif;
var bool: ret = bool_or(p, r);
} in ret;
\end{mzn}
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.
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-expressions contexts is safe, but it places a large burden on the \solver{}.
The solver performs better without using \gls{reif}.
To detect the 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}.
Otherwise, it will act as a normal \rootc{} context.
\begin{figure*}
\begin{center}
\begin{tabular}{r | c c c c c}
join & \rootc & \mayberootc & \posc & \negc & \mixc \\
\hline
\rootc & \rootc & \rootc & \rootc & \rootc & \rootc \\
\mayberootc & \rootc & \mayberootc & \posc & \mixc & \mixc \\
\posc & \rootc & \posc & \posc & \mixc & \mixc \\
\negc & \rootc & \mixc & \mixc & \negc & \mixc \\
\mixc & \rootc & \mixc & \mixc & \mixc & \mixc \\
\end{tabular}
\end{center}
\caption{\label{fig:half-maybe-join} The join context operation extended with \mayberootc{}.}
\end{figure*}
\begin{figure*}
\centering
\begin{prooftree}
\hypo{\ctxeval{x\texttt{[}i\texttt{]}}{\rootc}}
\infer1[(Access-R)]{\ctxeval{x}{\mayberootc}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ctxeval{\texttt{if }b\texttt{ then } e_{1} \texttt{ else } e_{2} \texttt{ endif}}{\rootc}}
\infer1[(ITE-R)]{\ctxeval{c}{ctx},~\ctxeval{e_{1}}{\mayberootc},~\ctxeval{e_{2}}{\mayberootc}}
\end{prooftree}
\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 \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}.
At compile time, this is the only correct context to use.
We will, however, discuss how to adjust contexts dynamically during \gls{rewriting} in \cref{subsec:half-dyn-context}.
\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 an expression has to be \gls{reified}.
\begin{example}
\label{ex:half-rewriting}
Consider the \gls{rewriting} of the following \constraint{}.
\begin{mzn}
constraint (y -> f(x)) \/ not x = 5;
\end{mzn}
\noindent{}We will assume \mzninline{f} is a \gls{native} \constraint{} that can be both \gls{reified} or \gls{half-reified}.
For this \constraint{} we can determine the following contexts for its sub-expressions:
\begin{itemize}
\item the disjunction itself is in \rootc{} context,
\item \mzninline{y} and \mzninline{x = 5} are in \negc{} context,
\item and the rest are in \posc{} context.
\end{itemize}
\Gls{rewriting} using full \gls{reif} could produce the following \gls{native} \constraints{}.
\begin{mzn}
constraint bool_clause([b1, b2], []); % b1 \/ b2
constraint bool_clause_reif([b3], [y], b1); % b1 <-> y -> b3
constraint f_reif(x, b3); % b3 <-> f(x)
constraint bool_not(b4, b2); % b2 <-> not b4
constraint int_eq_reif(x, 5, b4); % b4 <-> x = 5
\end{mzn}
\Gls{rewriting} using \gls{half-reif} can simplify it to the following \gls{native} \constraints{}.
\begin{mzn}
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, 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{}.
Note, however, that the rewriting produced many extra implications.
If the Boolean \mzninline{y} was not further constrained 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); % y -> f(x)
constraint int_ne_imp(x, 5, b2); % b2 -> x != 5
\end{mzn}
\end{example}
As this example shows, the use of \gls{half-reif} can form so-called \glspl{implication-chain}.
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 next section, we present a new post-processing method we call \gls{chain-compression}.
It can be used to eliminate these \glspl{implication-chain}.
The \gls{rewriting} with \gls{half-reif} also interacts with some simplification 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 an 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 an expression is evaluated can be adjusted during the \gls{rewriting} process.
\subsection{Chain compression}%
\label{subsec:half-compress}
\Gls{rewriting} with \gls{half-reif} will in many cases result in \glspl{implication-chain}: \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 generalized to
\begin{mzn}
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}
constraint forall(i in N)(b1 -> c[i])
\end{mzn}
\noindent{}after which \texttt{b2} can be removed from the model.
An algorithm to remove these chains of implications is best comprehended through the use of an implication graph.
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, the algorithm requires vertices to be marked when their corresponding \variables{} are used in other \constraints{} in the \cmodel{}.
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 \gls{chain-compression} method in pseudocode.
\begin{algorithm}
\KwIn{An implication \constraint{} graph \(G=\tuple{V, E}\) and a set \(M
\subseteq{} V\) of vertices used in other \constraints{}.}
\KwOut{An equisatisfiable graph \(G'=\tuple{V', E'}\) where chained
implications have been removed.}
\(V' \longleftarrow V\)\;
\(E' \longleftarrow E\)\;
\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 \} \)\;
}
}
}
\(G' \longleftarrow \tuple{V', E'}\)\;
\caption{\label{alg:half-compression} implication \gls{chain-compression} algorithm}
\end{algorithm}
The algorithm can be further improved by considering implied conjunctions.
These can be split up into multiple implications.
\begin{mzn}
constraint b -> forall(x in N)(x)
\end{mzn}
The expression above is logically equivalent to the following expression.
\begin{mzn}
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 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 \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 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}
When using full \gls{reif}, all \glspl{reif} are stored in the \gls{cse} table.
This ensures that if the same expression is \gls{reified} twice, then the resulting \gls{cvar} will be reused.
This avoids that the solver has to enforce the same functional relation twice.
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{cvar} of the first \gls{half-reif} cannot be used for the second expression.
In general the following rules apply.
\begin{itemize}
\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 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 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 \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 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 \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 joint context.
The context recorded in the \gls{cse} table and the found context are joined 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 \gls{cvar} are 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 for 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 \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 a \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.
\begin{example}
Consider for example the \mzninline{=} operator on integers, which \microzinc{} represents as an \mzninline{int_eq} call.
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 an \mzninline{int_ne} call.
\end{example}
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 \gls{reif} of its negation.
Moreover, this mechanism also allows us to detect when an expression and its negation occur in \rootc{} context.
Since a \constraint{} and its negation cannot both hold at the same time, this is a simple way to detect that the \cmodel{} is \gls{unsat}.
\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 \microzinc{}.
The context may depend on data that is only known at an \instance{} level.
The same situation can be caused by \gls{propagation}.
\begin{example}
Consider the following \minizinc{} fragment
\begin{mzn}
var 1..4: x;
var 5..10: y;
var bool: b = x < y;
constraint b -> (2*x = y);
\end{mzn}
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}
constraint 2*x = y;
\end{mzn}
The linear \constraint{} could be evaluated in \rootc{} context, instead of the \posc{} context that is detected by our context analysis.
\end{example}
The situation shown in the example is the most common change of context.
If the \gls{cvar} of a \gls{reif} is fixed, the context 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{} is trivially \gls{satisfied}.
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 a layer of indirection.
In this layer, it checks the \gls{cvar}.
If the \gls{cvar} is already fixed, then it rewrites itself into the corresponding 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.
\begin{example}
Let's assume the \compiler{} finds a call to \mzninline{int_eq} in \posc{} context.
Instead of outputting the call to \mzninline{int_eq_imp} directly, it will instead output a call to \mzninline{int_eq_imp_check}.
This predicate is then generated as shown in \cref{lst:half-check-reif}.
The \gls{rewriting} of the calls to the generated predicate then follow the normal process.
\end{example}
\begin{listing}
\mznfile{assets/listing/half_reif_check.mzn}
\caption{\label{lst:half-check-reif}A generated predicate for \mzninline{int_eq_imp} that checks the \gls{cvar} to ensure a \gls{half-reif} is still required.}
\end{listing}
\section{Experiments}
\label{sec:half-experiments}
We now present an experimental evaluation of the presented techniques.
First, to show the benefit of implementing \glspl{propagator} for \gls{half-reified} \constraints{} by comparing their performance against their \glspl{decomp}.
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}.
We adapt the \glspl{propagator} for the non-\gls{reified} \constraints{} to take into account the \gls{cvar}, by reusing the code for checking and pruning as described in \cref{sec:half-propagation}.
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}.
\subsection{Half-Reified Propagators}
\label{sec:half-exp-prop}
Our first experiment considers the QCP-max quasi-group completion problem.
In this problem, we need to decide the value of a \((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 as possible where all \variables{} take a unique value.
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 using a \gls{reified} \mzninline{all_different} \constraint{}.
Since the goal of the problem is to maximize the number of \mzninline{all_different} \constraints{} that hold, these \constraints{} are never forced to be \mzninline{false}.
This means these \constraints{} are in \posc{} context and can be \gls{half-reified}.
\Cref{tab:half-qcp} shows the comparison of two solving configurations in \gls{chuffed} for the QCP-max problem.
The results are grouped based on their size of the instance.
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 \gls{propagator}.
This \gls{propagator} is an adjusted version from the existing \gls{bounds-con} \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 the \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 \gls{propagator} have to be adjusted as well.
These adjustments happen similar to the adjustments of the general algorithm: explanations used for the violation\glsadd{violated} of the \constraint{} can now be used to set the \gls{cvar} to \mzninline{false}, and the explanations given to prune a \variable{} are extended with a literal that ensures the \gls{cvar} is \mzninline{true}.
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{} library.}
\end{listing}
\begin{table}
\begin{center}
\input{assets/table/half_qcp}
\caption{\label{tab:half-qcp} 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 specialized \gls{propagator} has a significant advantage over the use of the \gls{decomp}.
Although it only allows us to solve 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.
In addition, we consider a variation on the prize collecting travelling salesman problem \autocite{balas-1989-pctsp} referred to as the ``prize collecting path'' problem.
In the problem we are given a graph with weighted edges, both positive and negative.
The aim of the problem is to find the optimal acyclic path from a given start node that maximizes the weights on the path.
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 an \gls{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 \gls{array}.
Otherwise, it will set its surrounding context to \mzninline{false}.
The \gls{half-reif} implicitly performs the same task by setting its \gls{cvar} to \mzninline{false} whenever the resulting \variable{} does not equal the element to which the index \variable{} points, or when the index points outside the \gls{array}.
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.}
\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 \gls{propagator} consistently outperforms 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{Rewriting with Half-Reification}
\label{sec:half-exp-rewriting}
The usage of context analysis and introduction of \glspl{half-reif} allows us to evaluate \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 have \glspl{propagator} for \glspl{half-reif} of many basic \constraints{}, and \minizinc{}'s \gls{linearization} and \gls{booleanization} libraries, 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 \gls{half-reif}.
The solving of the linearized \instances{} are tested using the \gls{cbc} and \gls{cplex} \gls{mip} \solvers{}.
The solving of the Booleanized \instances{} are testing using the \gls{openwbo} \solver{}.
\begin{table}
\begin{subtable}[b]{\linewidth}
\input{assets/table/half_flat_gecode}
\caption{\label{subtab:half-flat-gecode}\gls{gecode} library}
\end{subtable}
\begin{subtable}[b]{\linewidth}
\input{assets/table/half_flat_linear}
\caption{\label{subtab:half-flat-lin}\Gls{linearization} library}
\end{subtable}
\begin{subtable}[b]{\linewidth}
\input{assets/table/half_flat_sat}
\caption{\label{subtab:half-flat-bool}\Gls{booleanization} library}
\end{subtable}
\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-rewrite} shows the following cumulative figures from the \gls{rewriting} process of the \minizinc{} challenge.
\begin{itemize}
\item The number of \constraints{} in \flatzinc{}.
\item The number of \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 \glspl{half-reif} evaluated during the \gls{rewriting} process.
\item The number of implications removed using the \gls{chain-compression} method.
\item The runtime of the \gls{rewriting} process.
\end{itemize}
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 \gls{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 optimization techniques is minimal.
The \Cref{subtab:half-flat-lin} paints an equally positive picture of \glspl{half-reif} for linearization.
Since both \glspl{reif} and \glspl{half-reif} are decomposed during the \gls{rewriting} process, \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 with \gls{gecode}.
This is caused by the fact that the linearization 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 \gls{rewriting} time slightly increases for the linearization process.
Since there are many more \constraints{}, the introduced optimization mechanisms have a slightly higher overhead.
Finally, statistics for \gls{rewriting} the \instances{} for a \gls{maxsat} \solver{} are shown in \cref{subtab:half-flat-bool}.
Unlike linearization, \gls{half-reif} does not significantly reduce the number of \constraints{} and, although still significant, the number of \glspl{reif} is reduced by only slightly over ten percent.
We also see that the \gls{booleanization} library is explicitly defined in terms of \glspl{half-reif}.
Some \constraints{} manually introduce \mzninline{_imp} call as part of their definition.
Even when we do not automatically introduce \glspl{half-reif}, they are still introduced by other \constraints{}.
Furthermore, \gls{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 \gls{chain-compression} are instead aggregated into bigger clauses.
Surprisingly, \gls{half-reif} slightly reduces the \gls{rewriting} time as it reduces the workload.
The relatively small changes shown might indicate that additional work might be warranted in the \gls{booleanization} library.
It might be possible to create more dedicated \glspl{decomp} for \gls{half-reified} \constraints{}, and to analyse the library to see if \glspl{annotation} could be added to more function arguments to retain \posc{} contexts.
\begin{table}
\input{assets/table/half_mznc}
\caption{\label{tab:half-mznc} Status overview of solving \minizinc{} Challenge 2019 \& 2020 with and without \gls{half-reif}.}
\end{table}
\Cref{tab:half-mznc} shows the results reported by the solvers. The \solver{} reports
\begin{description}
\item[Unsatisfiable] when it proves the instance does not have a solution,
\item[Optimal solution] when it has found a solution and has proven it optimal,
\item[Satisfied] when it has found a solution for the problem,
\item[Unknown] when no solution is found, and
\item[Error] when the \solver{} program crashes.
\end{description}
\noindent{}For \solver{} statuses that end the solving process before the time-out of 15 minutes we also show the average time.
The results shown in this table are very mixed.
For \gls{gecode}, \gls{half-reif} does not seem to impact its solving performance.
We would have hoped that \glspl{propagator} for \glspl{half-reif} would be more efficient and reduce the number of \glspl{propagator} scheduled in general.
However, neither number of \instances{} solved, nor the required solving time improved.
A single \instance{}, however, is negatively impacted by the change; an \gls{opt-sol} for this \instance{} is no longer found.
We expect that this \instance{} has benefited from the increased Boolean \gls{propagation} that is caused by full \gls{reif}.
Overall, these results do not show any significant positive or negative effects in \gls{gecode}'s performance when using \gls{half-reif}.
When using \gls{cplex}, \gls{half-reif} clearly has a positive effect.
Although it no longer proves the unsatisfiability of one instance and slightly increases the number of solver errors, an optimal solution is found for five more instances.
The same linearized instances when using the \gls{cbc} solver seem to have the opposite effect.
Even though it reduces the time required to prove that two instances are unsatisfiable, it can no longer find six optimal solutions.
These results are hard to explain.
In general, we would expect the reduction of \constraints{} in a \gls{mip} instance would help the \gls{mip} solver.
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 patterns, such as cliques, during the pre-processing of the \gls{mip} instance.
Some patterns can only be detected when using 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{lodi-2013-variability,fischetti-2014-erratiscism}.
When using \gls{half-reif} in addition to \gls{aggregation} and \gls{del-rew}, the order and form of the \gls{slv-mod} can be exceedingly different.
The solving statistics for \gls{openwbo} might be most positive.
Through the use of \gls{half-reif}, \gls{openwbo} is able to find and prove the \gls{opt-sol} for 3 more \instances{}.
It negatively impacts one \instance{}, that no longer finds any \gls{sol}.
That the effect is so positive is surprising since its \gls{rewriting} statistics for \gls{maxsat} showed the least amount of change.
% \section{Summary}
% \label{sec:half-summary}
Reference in New Issue View Git Blame Copy Permalink