923 lines
52 KiB
TeX
923 lines
52 KiB
TeX
%************************************************
|
|
\chapter{Half Reification}\label{ch:half-reif}
|
|
%************************************************
|
|
|
|
\input{chapters/4_half_reif_preamble}
|
|
|
|
\section{Introduction to Half Reification}
|
|
|
|
The complex expressions language used in \cmls{}, such as \minizinc{}, often require the use of \gls{reification} in the flattening process to reach a solver level constraint model.
|
|
If the Boolean expression \mzninline{pred(...)} is seen in a non-root context, then a new Boolean \variable{} \mzninline{b} is introduced to replace the expression.
|
|
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(...)}).
|
|
|
|
A weakness of reification is that each reified version of a constraint requires further implementation to create, and indeed most solvers do not provide any reified versions of their \gls{global} \constraints{}.
|
|
|
|
\begin{example}\label{ex:hr-alldiff}
|
|
Consider the complex constraint
|
|
|
|
\begin{mzn}
|
|
constraint i <= 4 -> all_different([i,x-i,x]);
|
|
\end{mzn}
|
|
|
|
The usual flattened form would be
|
|
|
|
\begin{mzn}
|
|
constraint int_le_reif(i, 4, b1); % b1 holds iff i <= 4
|
|
constraint int_minus(x, i, t1); % t1 = x - i
|
|
constraint all_different_reif([i,t1,x], b2);
|
|
constraint bool_clause([b2], [b1]) % b1 implies b2
|
|
\end{mzn}
|
|
|
|
but no solver we are aware of implements the third primitive constraint.
|
|
%
|
|
\footnote{Although there are versions of soft \mzninline{all_different}, they
|
|
do not define this form.}
|
|
\end{example}
|
|
|
|
Reified \gls{global} \constraints{} are not implemented because a reified constraint \mzninline{b <-> pred(...)} must also implement a propagator for \mzninline{not pred(...)} (in the case that \mzninline{b = false}).
|
|
While for some global \constraints{}, \eg\ \mzninline{all_different}, this may be reasonable to implement, for most, such as \texttt{cumulative}, the task seems to be very difficult.
|
|
|
|
Another weakness of the reification is that it may keep track of more information than is required.
|
|
In a typical solver, the first reified constraint \mzninline{b1 <-> i <= 4} will wake up whenever the upper bound of \texttt{i} changes in order to check whether it should set \texttt{b1} to \mzninline{true}.
|
|
But setting \mzninline{b1} to \mzninline{true} will \emph{never} cause any further propagation.
|
|
There is no reason to check this.
|
|
|
|
This is particularly important when the target solver is a mixed integer programming solver.
|
|
In order to linearise a reified linear constraint we need to create two linear \constraints{}, but if we are only interested in half of the behaviour we can manage this with one linear constraint.
|
|
|
|
\begin{example}
|
|
Consider the constraint \mzninline{b1 <-> i <= 4}, where \texttt{i} can take
|
|
values in the domain \mzninline{0..10} then its linearisation is
|
|
|
|
\begin{mzn}
|
|
constraint i <= 10 - 6 * b1; % b1 -> i <= 4
|
|
constraint i >= 5 - 5 * b1; % not b1 -> i >= 5
|
|
\end{mzn}
|
|
|
|
But in the system of \constraints{} where this constraint occurs knowing that
|
|
\texttt{b1} is 0 will never cause the system to fail, hence we do not need to
|
|
keep track of it.
|
|
%
|
|
We can simply use the second constraint in the linearisation, which always
|
|
allows that \texttt{b1} takes the value 0.
|
|
\end{example}
|
|
|
|
The simple flattening used above treats partial functions in the following
|
|
manner.
|
|
%
|
|
Application of a partial function to a value for which it is not defined gives
|
|
value \undefined, and this \undefined\ function percolates up through every
|
|
expression to the top level conjunction, making the model unsatisfiable.
|
|
%
|
|
For the example
|
|
%
|
|
\jip{TODO:\ What goes here???}
|
|
|
|
In this chapter we study the usage of \gls{half-reif}. \gls{half-reif} follows
|
|
from the notion that in many cases it might be 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.
|
|
|
|
\begin{itemize}
|
|
\item Half reified \constraints{} add no burden to the solver writer; if they
|
|
have a propagator for constraint \mzninline{pred(....)} then they can
|
|
straightforwardly construct a half reified propagator for \mzninline{b ->
|
|
pred(...)}.
|
|
|
|
\item Flattening with \gls{half-reif} can produce smaller linear models when
|
|
used with a mixed integer programming solver.
|
|
|
|
\item Half reified \constraints{} \mzninline{b -> pred(...)} can implement fully
|
|
reified \constraints{} without any loss of propagation strength (assuming
|
|
reified \constraints{} are negatable). \jip{TODO:\ should this still be here?}
|
|
|
|
\item Flattening with half reification can naturally produce the relational
|
|
semantics when flattening partial functions in positive contexts.
|
|
\jip{TODO:\ should this still be here?}
|
|
|
|
\item Flattening with half reification can produce more efficient propagation
|
|
when flattening complex \constraints{}. \jip{TODO:\ should this still be
|
|
here?}
|
|
\end{itemize}
|
|
|
|
The remainder of the chapter is organised as follows.
|
|
\Cref{sec:half-propagation} discusses the propagation of half-reified \constraints{}.
|
|
\Cref{sec:half-decomposition} discusses the decomposition of half-reified constraint.
|
|
\Cref{sec:half-context} introduces the notion of context analysis: a way to determine if \gls{half-reif} can be used for a certain expression.
|
|
Finally, \cref{sec:half-flattening} explains how this information can be used during the flattening process.
|
|
|
|
\section{Propagation and Half Reification}%
|
|
\label{sec:half-propagation}
|
|
|
|
The tasks of a propagator for any constraint can logically be split into two tasks:
|
|
|
|
\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.
|
|
\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{}.
|
|
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.
|
|
|
|
\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\).
|
|
}
|
|
\KwResult{This pseudo code propagates the \gls{half-reif} of \(c\) (\ie{} \(b \implies\ c\)).}
|
|
|
|
\BlankLine{}
|
|
\If{\(b\) {\normalfont is unassigned} }{
|
|
\If{\(\neg{}check()\)}{
|
|
\(b \longleftarrow \) \mzninline{false}\;
|
|
}
|
|
}
|
|
\If{\(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.
|
|
In practice, however, this is not always possible.
|
|
In some cases, propagators 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}.
|
|
|
|
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.
|
|
|
|
\begin{itemize}
|
|
\item custom implemented half-reified propagations.
|
|
\item benefits
|
|
\item downside
|
|
\item experimental results
|
|
\end{itemize}
|
|
|
|
Another weakness of the reification is that it may keep track of more information than is required.
|
|
In a typical solver, the first reified constraint \mzninline{b1 <-> i <= 4} will wake up whenever the upper bound of \texttt{i} changes in order to check whether it should set \texttt{b1} to \mzninline{true}.
|
|
But setting \mzninline{b1} to \mzninline{true} will \emph{never} cause any further propagation.
|
|
There is no reason to check this.
|
|
|
|
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.
|
|
|
|
When full reification is applicable (where we are not using half reified predicates) an alternative to half reification is to implement full reification \mzninline{x <-> pred(...)} by two half reified propagators \mzninline{x -> pred(...)}, \mzninline{y \half \neg pred(...)}, \mzninline{x <-> not y}.
|
|
This does not lose propagation strength.
|
|
For Booleans appearing in a positive context we can make the propagator \mzninline{y -> not pred(...)} 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.
|
|
|
|
\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{reification}, 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.
|
|
If, however, a \gls{reification} is replaced by a \gls{half-reif}, then only one of these implication is required.
|
|
|
|
\begin{example}
|
|
|
|
Consider the \gls{reification} 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{reification} 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.
|
|
\end{example}
|
|
|
|
The same principle can be applied all throughout the linearisation process.
|
|
Ultimately, \minizinc{}'s linearisation library rewrites most \glspl{reification} in terms of implied less than or equal to constraint.
|
|
For all these \glspl{reification}, its replacement by a \gls{half-reif} can remove half of the implications required for the \gls{reification}.
|
|
|
|
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}:
|
|
\[ 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.
|
|
|
|
It is, however, not as straightforward to construct its full \gls{reification}.
|
|
In addition to the half-reified \gls{cnf}, a generic \gls{reification} would require the reverse implication, \(\neg 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}.
|
|
This overhead can be avoided when using \gls{half-reif}.
|
|
\jip{TODO: it would be great to conclude here that all these clauses are unnecessary in a positive context, since \(b\) would never be set to false.}
|
|
|
|
According to the principles above, decomposition libraries for the full \minizinc{} language have been implemented for \gls{mip} and \gls{sat} solvers.
|
|
In \cref{sec:half-experiments} we asses the effects when flattening with \gls{half-reif}.
|
|
|
|
\section{Context Analysis}%
|
|
\label{sec:half-context}
|
|
|
|
\Gls{half-reif} can be used instead of full \gls{reification} when the \gls{reification} can never be forced to be false.
|
|
We see this in, for example, a disjunction \(a \lor b\).
|
|
No matter the value of \(a\), setting the value of \(b\) to be true can never make the overall expression false.
|
|
At any \(b\) is thus never forced to be false.
|
|
This requirement follows from the difference between implication and logical equivalences.
|
|
Setting the left hand side of a implication to false, does not influence the value on the right hand side.
|
|
So if we know that this is never required in the overall expression, then using an implication instead of a logical equivalence, \ie a \gls{half-reif} instead of a full \gls{reification}, does not change the meaning of the constraint.
|
|
|
|
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.
|
|
For example the left hand side of the constraint
|
|
|
|
\begin{mzn}
|
|
constraint count(x in arr)(x = 5) > 5;
|
|
\end{mzn}
|
|
|
|
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 can half-reify the expression.
|
|
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
|
|
\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
|
|
|
|
\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 are then placed in a \posc{} context.
|
|
Our example can be transformed into:
|
|
|
|
\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''.
|
|
|
|
Expressions in a \mixc{} context are in a position where \gls{half-reif} is impossible.
|
|
Only full \gls{reification} can be used for expressions in that are in this context.
|
|
This occurs, for example, when using an exclusive or expression in a constraint.
|
|
The value that one side must take directly depends on the value that the other side takes.
|
|
Each side can thus be forced to be true or false.
|
|
The \mixc{} context can also be used as a ``fall back'' context.
|
|
If it cannot be determined if an expression is in a \posc{} or \negc{} context, then it is always safe to say the expression is in a \mixc{} context.
|
|
|
|
When taking into account the possible undefinedness of an expression, every expression in a \minizinc{} model has two different contexts: the context in which the expression itself occurs, its \emph{value context}, and the context in which the partiality of the expression is captured, its \emph{partiality context}.
|
|
As described in \cref{subsec:back-mzn-partial}, \minizinc{} uses relational semantics of partial values.
|
|
This means that if a function does not have a result, then its nearest enclosing Boolean expression is set to false.
|
|
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 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.
|
|
|
|
\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 predicate call \mzninline{pred(a, b, c)} is bound to the variable \mzninline{x}.
|
|
The call is in \posc\ context, and can be half-reified, if the variable \mzninline{x} is only used in \posc{} context.
|
|
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 fully 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 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{reification} of the call.
|
|
In this scenario, we prefer to create the full \gls{reification} as it decreases the number of \variables{} and \constraint{} 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.
|
|
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.
|
|
|
|
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 rules describe how an expression 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{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 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 are found are 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 an value is used in an implicit global state.
|
|
|
|
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.}
|
|
|
|
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\)).
|
|
If a function argument is not annotated, then the argument is evaluated in \mixc context.
|
|
|
|
\begin{example}
|
|
|
|
Consider the following user-defined \minizinc\ implementation of a logical implication.
|
|
|
|
\begin{mzn}
|
|
predicate impli(
|
|
var bool: x ::promise_ctx_antitone,
|
|
var bool: y ::promise_ctx_monotone
|
|
) =
|
|
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.
|
|
|
|
\end{example}
|
|
|
|
\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{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 \emph{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 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:
|
|
|
|
\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{reification} can be defined as \(ident\)\mzninline{_reif}.
|
|
\end{description}
|
|
|
|
\item If \(ident\) is a \microzinc{} function with an expression body \(E\), then 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 non of the earlier steps were successful, then the compilation fails.
|
|
Note that this can only occurr when a solver-level predicate does not have an \gls{reification}.
|
|
\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.
|
|
We will revisit this issue in \cref{subsec:half-?root}.
|
|
|
|
Finally, the (Compr) and (Arr) rules show simple inference rules for 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{x}{\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 let expressions 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.
|
|
|
|
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.
|
|
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 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 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 \rootc{}}%
|
|
\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 array access or if-then-else expression is found in \rootc{} context, it often makes sense to evaluate its sub-expression in \rootc context as well.
|
|
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}
|
|
|
|
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.
|
|
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 if-then-else expression is not also used in a disjunction.
|
|
If \mzninline{b} evaluates to \mzninline{true}, then \mzninline{p} is evaluated in \rootc{} context, and \mzninline{p} can take the value \mzninline{true} in the disjunction.
|
|
Otherwise, \mzninline{q} is evaluated in \rootc{} context, and \mzninline{p} in the disjunction must be evaluated in \posc{} context.
|
|
It is, therefore, not safe to assume that all sides of the if-then-else expressions are evaluated in \rootc{} context.
|
|
\end{example}
|
|
|
|
Using the \changepos{} transformation for sub-expression contexts is safe, but it might place a large burden on the \solver{}.
|
|
The solver is likely to perform better when the direct constraint predicate is 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.
|
|
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{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 array access and if-then-else 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 only correct context to use.
|
|
We will, however, discuss the dynamically adjusting of contexts during flattening in \cref{subsec:half-dyn-context}.
|
|
|
|
\section{Flattening and Half Reification}%
|
|
\label{sec:half-flattening}
|
|
|
|
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.
|
|
|
|
\jip{TODO: Add example of flattening with \gls{half-reif}}
|
|
|
|
The flattening with \gls{half-reif} does, however, interact with some of the optimisations used during the flattening process.
|
|
Most importantly, \gls{half-reif} has to be considered when using \gls{cse}.
|
|
In \cref{subsec:half-cse} we will discuss how \gls{cse} can be adjusted to handle \gls{half-reif}.
|
|
|
|
As shown in \jip{insert reference}, a consequence of the use of \gls{half-reif} is that it might form 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.
|
|
|
|
\subsection{Common Sub-expression Elimination}%
|
|
\label{subsec:half-cse}
|
|
|
|
When using full \gls{reification}, all \glspl{reification} 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 avoids that the solver has to enforce the same functional relationship twice.
|
|
|
|
If the flattener uses \gls{half-reif}, in addition to full \gls{reification}, 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:
|
|
|
|
\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 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 flattening result of a \mixc{} context, a \gls{reification}, 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{reification} 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).
|
|
|
|
\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.
|
|
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{reification} 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.
|
|
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.
|
|
|
|
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.
|
|
|
|
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{reification} 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.
|
|
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.
|
|
Clearly, a \constraint{} and its negation cannot both hold at the same time.
|
|
|
|
\subsection{Dynamic Context Switching}%
|
|
\label{subsec:half-dyn-context}
|
|
|
|
\subsection{Chain compression}%
|
|
\label{subsec:half-compress}
|
|
|
|
As shown in \cref{ex:hr-half}, 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.
|
|
The case shown in the example can be generalised to
|
|
|
|
\begin{mzn}
|
|
b1 -> b2 /\ forall(i in N)(b2 -> c[i])
|
|
\end{mzn}
|
|
|
|
\noindent{}which, if \texttt{b2} has no other usage in the instance, can be resolved to
|
|
|
|
\begin{mzn}
|
|
forall(i in N)(b1 -> c[i])
|
|
\end{mzn}
|
|
|
|
\noindent{}after which \texttt{b1} 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 \(\tuple{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.
|
|
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.
|
|
|
|
\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\)} {
|
|
\If{\(x \not\in M\) \textbf{ and }\(\left|\left\{\tuple{a,x}| \tuple{a,x} \in E\right\}\right| = 1\)}{
|
|
\For{\(\tuple{x, b} \in E\)}{
|
|
\(E' \longleftarrow E' \cup \{ \tuple{a,b} \} \)\;
|
|
\(E' \longleftarrow E' \backslash \{ \tuple{x,b} \} \)\;
|
|
}
|
|
\(E' \longleftarrow E' \backslash \{ \tuple{a,x} \} \)\;
|
|
\(V' \longleftarrow V' \backslash \{ x \} \)\;
|
|
}
|
|
}
|
|
\(G' \longleftarrow \tuple{V', E'}\)\;
|
|
\caption{\label{alg:half-compression} Implication 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}
|
|
b -> forall(x in N)(x)
|
|
\end{mzn}
|
|
|
|
\noindent{}is equivalent to
|
|
|
|
\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.
|
|
|
|
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.
|
|
|
|
\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.
|
|
To do this, we recreate two experiments presented by Feydy et al.\ 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{}.
|
|
|
|
Additionally, we assess the effects of automatically detecting and introducing \glspl{half-reif} during the flattening process. We flatten and solve
|
|
|
|
A description of the used computational environment, \minizinc{} instances, and versioned software has been included in \cref{ch:benchmarks}.
|
|
|
|
\subsection{Propagators}
|
|
\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}.
|
|
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 \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.
|
|
|
|
\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.
|
|
|
|
The first configuration uses a newly created propagator for half-reified \mzninline{all_different} \constraints{}.
|
|
This propagator is an adjusted version from the existing bounds consistent \mzninline{all_different} propagator in 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{}.
|
|
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}.
|
|
|
|
The second configuration uses the following decomposition for the \mzninline{all_different} constraint.
|
|
|
|
\begin{mzn}
|
|
predicate all_different(array[int] of var int: x) =
|
|
forall(i,j in index_set(x) where i < j)(
|
|
x[i] != x[j]
|
|
);
|
|
\end{mzn}
|
|
|
|
The \mzninline{!=} constraints produced by this redefinition are reified.
|
|
Their conjunction, then represent the reification 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.}
|
|
|
|
\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.
|
|
|
|
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.
|
|
The aim of the problem is to find the optimal acyclic path from a given start node that maximises 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 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.
|
|
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.
|
|
|
|
\begin{table}[tb]
|
|
\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 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.
|
|
|
|
\subsection{Decomposition experiments}
|
|
\label{sec:half-exp-decomp}
|
|
|
|
To verify the effectiveness of the half reification implementation within the \minizinc{} distribution we compare the results of the current version of the \minizinc{} translator (rev.\jip{add revision}) against the equivalent version for which we have implemented half reification.
|
|
We use the model instances used by the \minizinc{} challenges \autocite{stuckey-2010-challenge,stuckey-2014-challenge} from 2019 and 2020. The performance of the generated \flatzinc{} models will be tested using Gecode, flattened with its own library, and Gurobi and CBC, flattened with the linear library.
|
|
|
|
\begin{table} [tb]
|
|
\caption{\label{tab:hr-flat-results} Flattening results: Average changes in the
|
|
generated the \flatzinc{} models}
|
|
\begin{center}
|
|
\begin{tabular}{|l|r||r|r|r||r|}
|
|
\hline
|
|
Library & Nr. Instances & Full Reifications
|
|
& Constraints & Variables & Chains Compressed \\
|
|
\hline
|
|
Gecode & 274 & -38.19\% & -6.29\% & -8.66\% & 21.35\% \\
|
|
\hline
|
|
Linear & 346 & - 33.11\% & -13.77\% & -3.70\% & 11.63\% \\
|
|
\hline
|
|
\end{tabular}
|
|
\end{center}
|
|
\end{table}
|
|
\jip{Better headers for \cref{tab:hr-flat-results} and update with current results}
|
|
|
|
\Cref{tab:hr-flat-results} shows the average change on the number of full reification, constraints, and variables between the \flatzinc\ models generated by the different versions of the translator using the different libraries.
|
|
We find that the number full reifications is reduced by a significant amount.
|
|
Together with the chain compression mechanism this has a positive effect on the number of constraints and the number of variables.
|
|
|
|
\jip{Add something regarding the chain compression. Is this the right
|
|
statistic? (Compressions in terms of reifications)}
|
|
|
|
We ran our experiments on a computer with a 3.40GHz Intel i7-3770 CPU and 16Gb of memory running the Ubuntu 16.04.3 LTS operating system.
|
|
|
|
\jip{Scatter plot of the runtimes + discussion!}
|
|
|
|
|
|
\section{Summary}
|
|
\label{sec:half-summary}
|