|
|
|
|
@ -9,73 +9,115 @@
|
|
|
|
|
|
|
|
|
|
\input{chapters/4_half_reif_preamble}
|
|
|
|
|
|
|
|
|
|
\section{An Introduction to Half Reification}
|
|
|
|
|
\section{An Introduction to Half-Reification}
|
|
|
|
|
\label{sec:half-intro}
|
|
|
|
|
|
|
|
|
|
The complex expressions language used in \cmls{}, such as \minizinc{}, often require the use of \gls{reif} in the \gls{rewriting} process to reach a \gls{slv-mod}.
|
|
|
|
|
If the Boolean expression \mzninline{pred(...)} is seen in a non-\rootc{} context, then a new Boolean \variable{} \mzninline{b} is introduced to replace the expression, its \gls{cvar}.
|
|
|
|
|
The 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 the usage of \gls{reif} in the \gls{rewriting} process is well-understood, it suffers from certain weaknesses:
|
|
|
|
|
\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{enumerate}
|
|
|
|
|
\item Many \glspl{reif} are created in the rewriting of partial expressions to accommodate \minizinc{}'s \glspl{rel-sem}.
|
|
|
|
|
\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.
|
|
|
|
|
\item A \gls{reif} sometimes provides too much information to its surrounding context, triggering \glspl{propagator} that will never be able to prune any values from a \gls{domain}.
|
|
|
|
|
\end{enumerate}
|
|
|
|
|
\end{itemize}
|
|
|
|
|
|
|
|
|
|
As an alternative, the authors introduce \gls{half-reif}.
|
|
|
|
|
\gls{half-reif} follows from the idea that in many cases it is sufficient to use the logical implication of an expression, \mzninline{b -> pred(...)}, instead of the logical equivalence, \mzninline{b <-> pred(...)}.
|
|
|
|
|
\Gls{rewriting} with \gls{half-reif} is an approach that improves upon all these weaknesses of \gls{rewriting} with ``full'' \gls{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{enumerate}
|
|
|
|
|
\item \Gls{rewriting} using \glspl{half-reif} naturally produces \glspl{rel-sem}.
|
|
|
|
|
\item \Glspl{propagator} for a \glspl{half-reif} can usually be constructed by merely altering a \gls{propagator} implementation for its regular \constraint{}.
|
|
|
|
|
\item \Gls{half-reif} does not often interact with its \gls{cvar}, limiting the amount of triggered \glspl{propagator} that are known to be unable to prune any \domains{}.
|
|
|
|
|
\end{enumerate}
|
|
|
|
|
\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 the usage of \glspl{half-reif} can therefore lead to a reduction in \gls{native} \constraints{} in the \gls{slv-mod}.
|
|
|
|
|
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.
|
|
|
|
|
We see this in, for example, a disjunction \(a \lor b\).
|
|
|
|
|
No matter the value of \(a\), setting the value of \(b\) to be true can never make the overall expression false.
|
|
|
|
|
\(b\) is thus never forced to be false.
|
|
|
|
|
This requirement follows from the difference between implication and logical equivalences.
|
|
|
|
|
Setting the left hand side of a implication to false, does not influence the value on the right hand side.
|
|
|
|
|
So if we know that this is never required in the overall expression, then using an implication instead of a logical equivalence (\ie{} a \gls{half-reif} instead of a full \gls{reif}) does not change the meaning of the \constraint{}.
|
|
|
|
|
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}.
|
|
|
|
|
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}
|
|
|
|
|
|
|
|
|
|
Since the increasing left hand side of the \constraint{} will only ever help satisfy the \constraint{}, the expression \mzninline{x = 5} will never forced to be false.
|
|
|
|
|
This means that the expression can be \gls{half-reified}.
|
|
|
|
|
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 introduce extra distinctions in the context of expressions.
|
|
|
|
|
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} with regards to 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} with regards to 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 categorise the latter into:
|
|
|
|
|
Now, we will categorise the latter into the following three contexts.
|
|
|
|
|
|
|
|
|
|
\begin{description}
|
|
|
|
|
|
|
|
|
|
\item[\posc{}] when an expression must reach \textbf{at least} a certain value to satisfy its enclosing \constraint{}.
|
|
|
|
|
The expression is never forced to take a lower value.
|
|
|
|
|
\item[\posc{}] An expression is in \posc{} context when its enclosing \constraint{} (in \rootc{} context) is \textbf{monotone} \wrt{} the expression.
|
|
|
|
|
|
|
|
|
|
\item[\negc{}] when an expression can reach \textbf{at most} a certain value to satisfy its enclosing \constraint{}.
|
|
|
|
|
The expression is never forced to take a higher value.
|
|
|
|
|
\item[\negc{}] An expression is in \negc{} context when its enclosing \constraint{} (in \rootc{} context) is \textbf{antitone} \wrt{} the expression.
|
|
|
|
|
|
|
|
|
|
\item[\mixc{}] when an expression must take an \textbf{exact value}, be within a \textbf{specified range} or when during \gls{rewriting} it cannot be determined whether the expression must be increased or decreased to satisfy the enclosing \constraint{}.
|
|
|
|
|
\item[\mixc{}] An expression is in \mixc{} context when its enclosing \constraint{} (in \rootc{} context) it is \textbf{neither} monotone, nor antitone \wrt{} the expression.
|
|
|
|
|
|
|
|
|
|
\end{description}
|
|
|
|
|
|
|
|
|
|
As previously explained, \gls{half-reif} can be used for expressions in \posc{} context.
|
|
|
|
|
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}
|
|
|
|
|
@ -86,7 +128,7 @@ Although expressions in a \negc{} context cannot be directly \gls{half-reified},
|
|
|
|
|
\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.
|
|
|
|
|
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}
|
|
|
|
|
@ -99,44 +141,58 @@ Although expressions in a \negc{} context cannot be directly \gls{half-reified},
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
\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}
|
|
|
|
|
|
|
|
|
|
The tasks of a \gls{propagator} for any \constraint{} can logically be split into two:
|
|
|
|
|
Logically, there are three tasks that a \gls{propagator} for any \constraint{} must perform:
|
|
|
|
|
|
|
|
|
|
\begin{enumerate}
|
|
|
|
|
\item to \(check\) if the \constraint{} can still be satisfied (and otherwise declare the current state \gls{unsat}),
|
|
|
|
|
\item and to \(prune\) values from the \glspl{domain} of \variables{} that would violate\glsadd{violated} the \constraint{}.
|
|
|
|
|
\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 two tasks.
|
|
|
|
|
The \gls{half-reified} \gls{propagator} is dependent on an additional argument \texttt{b}, the \gls{cvar}.
|
|
|
|
|
The Boolean \variable{} can be in three states, it can currently not have been assigned a value, it can be assigned \mzninline{true}, or it can be assigned \mzninline{false}.
|
|
|
|
|
Given \texttt{b}, \(check\), and \(prune\), \cref{alg:half-prop} shows pseudo code for the \gls{propagation} of the \gls{half-reif} of the \constraint{}.
|
|
|
|
|
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 pseudo code for the \gls{propagation} of the \gls{half-reif} of the \constraint{}.
|
|
|
|
|
|
|
|
|
|
\begin{algorithm}
|
|
|
|
|
\begin{algorithm}[t]
|
|
|
|
|
|
|
|
|
|
\KwIn{A function \(check\), that returns false when the \constraint{} \(c\) cannot be satisfied, a function \(prune\), that eliminates values from \variable{} \glspl{domain} that violate\glsadd{violated} the \constraint{} \(c\), and a Boolean \gls{cvar} \texttt{b}.
|
|
|
|
|
\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 pseudo code propagates the \gls{half-reif} of \(c\) (\ie{} \(\texttt{b} \implies\ c\)).}
|
|
|
|
|
\KwResult{This pseudo code propagates the \gls{half-reif} of \(c\) (\ie{} \(b \implies\ c\)) and returns whether the \constraint is entailed.}
|
|
|
|
|
|
|
|
|
|
\BlankLine{}
|
|
|
|
|
\If{\texttt{b} {\normalfont is unassigned} }{
|
|
|
|
|
\If{\(b \text{ is unassigned}\)}{
|
|
|
|
|
\If{\(\neg{}check()\)}{
|
|
|
|
|
\(\texttt{b} \longleftarrow \) \mzninline{false}\;
|
|
|
|
|
\(b \longleftarrow \text{false}\)\;
|
|
|
|
|
\Return{} \(\text{true}\)\;
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
\If{\(\texttt{b} = \mzninline{true}\)}{
|
|
|
|
|
\If{\(\texttt{b} = \text{true}\)}{
|
|
|
|
|
\(prune()\)\;
|
|
|
|
|
\Return{} \(entailed()\)\;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
\caption{\label{alg:half-prop} Propagation pseudo code for the \gls{half-reif} of a \constraint{} \(c\), based on the propagator for \(c\).}
|
|
|
|
|
\Return{} \(\text{false}\)\;
|
|
|
|
|
\caption{\label{alg:half-prop} \gls{propagation} pseudo code 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.
|
|
|
|
|
@ -148,29 +204,62 @@ When a \gls{domain} is found to be empty, then the \gls{propagator} declares the
|
|
|
|
|
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{}.
|
|
|
|
|
|
|
|
|
|
\Glspl{propagator} gain certain advantages from \gls{half-reif}, but also may suffer certain penalties.
|
|
|
|
|
\Gls{half-reif} can cause propagators to wake up less frequently: \glspl{cvar} that are fixed to true by full \gls{reif} will never be fixed by \gls{half-reif}.
|
|
|
|
|
This is advantageous, but a corresponding disadvantage is that \glspl{cvar} that are fixed can allow the simplification of the \glspl{propagator} that use them, and hence make \gls{propagation} faster.
|
|
|
|
|
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.}
|
|
|
|
|
|
|
|
|
|
When a full \gls{reif} is required, its \gls{propagation} might still be performed using \gls{half-reif}.
|
|
|
|
|
A full \gls{reif} \mzninline{x <-> pred(...)} can be propagated using two half reified propagators, \mzninline{x -> pred(...)} and \mzninline{y -> not pred(...)}, and the \constraint{} \mzninline{x <-> not y}.
|
|
|
|
|
\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 pseudo code 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} pseudo code 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}.
|
|
|
|
|
Both \glspl{propagator} are designed and implemented in \gls{chuffed} according to the principles explained above.
|
|
|
|
|
In \cref{sec:half-experiments} we assess the implementation of \glspl{propagator} for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element} 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 need to keep track of as much information.
|
|
|
|
|
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 implication is required.
|
|
|
|
|
If, however, a \gls{reif} is replaced by a \gls{half-reif}, then only one of these implications is required.
|
|
|
|
|
|
|
|
|
|
\begin{example}
|
|
|
|
|
|
|
|
|
|
@ -188,10 +277,10 @@ If, however, a \gls{reif} is replaced by a \gls{half-reif}, then only one of the
|
|
|
|
|
|
|
|
|
|
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}, its replacement by a \gls{half-reif} can remove half of the implications required for the \gls{reif}.
|
|
|
|
|
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 \gls{decomp} into \gls{cnf} of the following form.
|
|
|
|
|
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} \]
|
|
|
|
|
@ -213,12 +302,6 @@ In \cref{sec:half-experiments} we assess the effects when \gls{rewriting} with \
|
|
|
|
|
\section{Context Analysis}%
|
|
|
|
|
\label{sec:half-context}
|
|
|
|
|
|
|
|
|
|
When taking into account the possible undefinedness of an expression, every expression in a \minizinc{} model has two different contexts: the context in which the expression itself occurs, its value context, and the context in which the partiality of the expression is captured, its partiality context.
|
|
|
|
|
As described in \cref{subsec:back-mzn-partial}, \minizinc{} uses \glspl{rel-sem} for partial functions.
|
|
|
|
|
This means that if a function does not have a result, then its nearest enclosing Boolean expression is set to false.
|
|
|
|
|
In practice, this means that a condition that tests if the function will return a value is added to the nearest enclosing Boolean expression.
|
|
|
|
|
The 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 an identifier can be used multiple times in expressions that influence their context.
|
|
|
|
|
|
|
|
|
|
@ -231,7 +314,7 @@ Expressions bound to an identifier can be used multiple times in expressions tha
|
|
|
|
|
} in y -> x /\ x -> z;
|
|
|
|
|
\end{mzn}
|
|
|
|
|
|
|
|
|
|
The predicate call \mzninline{pred(a, b, c)} is bound to the identifier \mzninline{x}.
|
|
|
|
|
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}.
|
|
|
|
|
|
|
|
|
|
@ -240,23 +323,56 @@ Expressions bound to an identifier can be used multiple times in expressions tha
|
|
|
|
|
\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 \gls{half-reified} versions of both the call and the negation of the call.
|
|
|
|
|
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 a function 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 a 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 certain \variable{} at the same time.
|
|
|
|
|
This information is not available during during the interpretation of \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 the value and partiality have already been explicitly separated and no longer requires special handling.
|
|
|
|
|
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 rules describe how an expression is found in a context \(ctx\), above the line, changes the context of subordinate expressions, below the line.
|
|
|
|
|
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}.
|
|
|
|
|
@ -328,29 +444,27 @@ 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 consequent (Call) rule.
|
|
|
|
|
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 annotations, the context of the argument in a call in context \(ctx\) is transformed with the operation corresponding to the annotation (\eg\ \(\changepos{}ctx\) or \(\changeneg{}ctx\)).
|
|
|
|
|
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}.
|
|
|
|
|
|
|
|
|
|
\begin{listing}
|
|
|
|
|
\mznfile{assets/listing/half_impli.mzn}
|
|
|
|
|
\caption{\label{lst:half-impli} A user-defined predicate of a logical implication using \glspl{annotation} to define the context usage of its arguments.}
|
|
|
|
|
\end{listing}
|
|
|
|
|
|
|
|
|
|
The \glspl{annotation} placed on the argument of the \mzninline{impli} function will apply the same context transformations as the \mzninline{->} operator shown in \cref{alg:arg-ctx}.
|
|
|
|
|
In term of context analysis, this function now is equivalent to the \minizinc{} operator.
|
|
|
|
|
|
|
|
|
|
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\)}
|
|
|
|
|
@ -398,12 +512,12 @@ Otherwise, the \compiler{} follows the following steps to try to introduce the m
|
|
|
|
|
\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 copy of the function can be made that is evaluated in the desired context: \ctxeval{E}{ctx}.
|
|
|
|
|
\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 a \gls{native} \constraint{} does not define a \gls{reif}.
|
|
|
|
|
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.
|
|
|
|
|
@ -469,7 +583,7 @@ And, unlike \minizinc{}, the \constraint{} is not dependent on the context of th
|
|
|
|
|
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.
|
|
|
|
|
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}.
|
|
|
|
|
@ -494,7 +608,7 @@ 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.
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
@ -519,7 +633,7 @@ It is, however, not always safe to do so.
|
|
|
|
|
\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 evaluated, and that call will then globally constrain the \cmodel{}.
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
@ -541,10 +655,10 @@ It is, however, not always safe to do so.
|
|
|
|
|
In this situation, it is not safe for the \compiler{} to output calls for the \rootc{} variants of these calls.
|
|
|
|
|
\end{example}
|
|
|
|
|
|
|
|
|
|
Using the \changepos{} transformation for sub-expression contexts is safe, but it places a large burden on the \solver{}.
|
|
|
|
|
The solver performs better when the no \gls{reif} has to be used.
|
|
|
|
|
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 situation where the sub-expression are only used in an \gls{array} access or \gls{conditional} expression we introduce the \mayberootc{} context.
|
|
|
|
|
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}.
|
|
|
|
|
@ -583,8 +697,8 @@ Otherwise, it will act as a normal \rootc{} context.
|
|
|
|
|
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 \gls{rewriting} in \cref{subsec:half-dyn-context}.
|
|
|
|
|
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}
|
|
|
|
|
@ -600,7 +714,7 @@ During the \gls{rewriting} process the contexts assigned to the different expres
|
|
|
|
|
constraint (y -> f(x)) \/ not x = 5;
|
|
|
|
|
\end{mzn}
|
|
|
|
|
|
|
|
|
|
\noindent{}We will assume \mzninline{f} is a \gls{native} \constraint{} that be both \gls{reified} or \gls{half-reified}.
|
|
|
|
|
\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}
|
|
|
|
|
@ -609,7 +723,7 @@ During the \gls{rewriting} process the contexts assigned to the different expres
|
|
|
|
|
\item and the rest are in \posc{} context.
|
|
|
|
|
\end{itemize}
|
|
|
|
|
|
|
|
|
|
\Gls{rewriting} using full \gls{reif} could produce the following \gls{native} \constraint{}.
|
|
|
|
|
\Gls{rewriting} using full \gls{reif} could produce the following \gls{native} \constraints{}.
|
|
|
|
|
|
|
|
|
|
\begin{mzn}
|
|
|
|
|
constraint bool_clause([b1, b2], []); % b1 \/ b2
|
|
|
|
|
@ -629,8 +743,8 @@ During the \gls{rewriting} process the contexts assigned to the different expres
|
|
|
|
|
\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 did form many extra implications.
|
|
|
|
|
If the Boolean \mzninline{y} was not further \constraint{} in the problem, then we could further reduce it to the following \constraints{}.
|
|
|
|
|
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
|
|
|
|
|
@ -643,13 +757,13 @@ During the \gls{rewriting} process the contexts assigned to the different expres
|
|
|
|
|
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 \cref{subsec:half-compress} we present a new post-processing method we call \gls{chain-compression}.
|
|
|
|
|
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 of the optimisation methods used during the \gls{rewriting} process.
|
|
|
|
|
Most importantly, \gls{half-reif} has to be considered when using \gls{cse} and \gls{propagation} can change the context of expression.
|
|
|
|
|
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 executed can be adjusted during the \gls{rewriting} process.
|
|
|
|
|
Finally, in \cref{subsec:half-dyn-context} we will discuss how the context in which an expression is evaluated can be adjusted during the \gls{rewriting} process.
|
|
|
|
|
|
|
|
|
|
\subsection{Chain compression}%
|
|
|
|
|
\label{subsec:half-compress}
|
|
|
|
|
@ -674,7 +788,7 @@ An algorithm to remove these chains of implications is best comprehended through
|
|
|
|
|
An implication graph \(\tuple{V,E}\) is a directed graph.
|
|
|
|
|
The vertices \(V\) represent the \variables{} in the \instance{}.
|
|
|
|
|
An edge \((x,y) \in E\) represents the presence of an implication \mzninline{x -> y} in the instance.
|
|
|
|
|
Additionally, for the benefit of the algorithm, is marked when it is used in other \constraints{} in the \constraint{} model.
|
|
|
|
|
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 pseudo code.
|
|
|
|
|
|
|
|
|
|
@ -717,7 +831,7 @@ The expression above is logically equivalent to the following expression.
|
|
|
|
|
\end{mzn}
|
|
|
|
|
|
|
|
|
|
Adopting this transformation both simplifies a complicated \constraint{} and possibly allows for the further compression of \glspl{implication-chain}.
|
|
|
|
|
It should however be noted that although this transformation can increase the number of \constraints{} in the \gls{slv-mod}, it generally increases the \gls{propagation} efficiency.
|
|
|
|
|
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.
|
|
|
|
|
@ -727,11 +841,11 @@ In the case where a \variable{} has one incoming edge, but it is marked as used
|
|
|
|
|
\label{subsec:half-cse}
|
|
|
|
|
|
|
|
|
|
When using full \gls{reif}, all \glspl{reif} are stored in the \gls{cse} table.
|
|
|
|
|
This ensure that if the same expression is \gls{reified} twice, then the resulting \gls{reif} will be reused.
|
|
|
|
|
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{half-reif} from the first cannot be used for the second expression.
|
|
|
|
|
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}
|
|
|
|
|
@ -741,7 +855,7 @@ In general the following rules apply.
|
|
|
|
|
\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 a \gls{rewriting} an expression in \negc{} context pushes the negation inwards, the \gls{reif} does, however, need to be negated.
|
|
|
|
|
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).
|
|
|
|
|
|
|
|
|
|
@ -752,40 +866,37 @@ It would always be better to encounter the expression in a context that results
|
|
|
|
|
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 joint using the join operator, as described in \cref{fig:half-join}.
|
|
|
|
|
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 result is replaced by the new result.
|
|
|
|
|
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 the earlier version are correctly removed.
|
|
|
|
|
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 an \gls{half-reif} for its negation, then we instead evaluate the expression in \mixc{} context.
|
|
|
|
|
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, in \microzinc{} seen as a \mzninline{int_eq} call.
|
|
|
|
|
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.
|
|
|
|
|
This is simple way to detect conflicts between \constraints{} and, by extend, prove that the \cmodel{} is \gls{unsat}.
|
|
|
|
|
Clearly, a \constraint{} and its negation cannot both hold at the same time.
|
|
|
|
|
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{unsatisfiable}.
|
|
|
|
|
|
|
|
|
|
\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{}.
|
|
|
|
|
Its context depends on data that is only known at an \instance{} level.
|
|
|
|
|
The context may depends on data that is only known at an \instance{} level.
|
|
|
|
|
The same situation can be caused by \gls{propagation}.
|
|
|
|
|
|
|
|
|
|
\begin{example}
|
|
|
|
|
@ -810,43 +921,39 @@ The same situation can be caused by \gls{propagation}.
|
|
|
|
|
\end{example}
|
|
|
|
|
|
|
|
|
|
The situation shown in the example is the most common change of context.
|
|
|
|
|
If the \gls{cvar} of a \gls{reif} is fixed, the context often changes to either \rootc{} or a negated \rootc{} context.
|
|
|
|
|
If, on the other hand, the \gls{cvar} of a \gls{half-reif} is fixed, then either the context becomes \rootc{} or the \constraint{} already holds.
|
|
|
|
|
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 another layer of \gls{decomp}.
|
|
|
|
|
In this layer, it checks its \gls{cvar}.
|
|
|
|
|
If the \gls{cvar} is already fixed, then it rewrites itself into its form in another context.
|
|
|
|
|
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_lin_le} in \posc{} context.
|
|
|
|
|
Instead of outputting the call to \mzninline{int_lin_le_imp} directly, it will instead output a call to \mzninline{_int_lin_le_imp}.
|
|
|
|
|
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}.
|
|
|
|
|
This new predicate (calls) can then be rewritten normally.
|
|
|
|
|
|
|
|
|
|
\begin{listing}
|
|
|
|
|
\mznfile{assets/listing/half_reif_check.mzn}
|
|
|
|
|
\caption{\label{lst:half-check-reif}A generated predicate for \mzninline{int_lin_le_imp} that checks its \gls{cvar} to ensure a \gls{half-reif} is still required.}
|
|
|
|
|
\end{listing}
|
|
|
|
|
|
|
|
|
|
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 experimental evaluation of the presented techniques.
|
|
|
|
|
First, to show the benefit of implementing propagators for \gls{half-reified} \constraint{}, we compare their performance against their \glspl{decomp}.
|
|
|
|
|
To do this, we recreate two experiments presented by \textcite{feydy-2011-half-reif} in the original \gls{half-reif} paper in a modern \gls{cp} solver, \gls{chuffed}.
|
|
|
|
|
In the experiment, we use \glspl{propagator} implemented according to the principles described in this paper.
|
|
|
|
|
No new algorithm has been devised to perform the \gls{propagation}.
|
|
|
|
|
The \gls{propagator} of the direct \constraint{} is merely adjusted to influence and watch a \gls{cvar}.
|
|
|
|
|
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 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}.
|
|
|
|
|
@ -856,13 +963,13 @@ A description of the used computational environment, \minizinc{} instances, and
|
|
|
|
|
|
|
|
|
|
Our first experiment considers the 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.
|
|
|
|
|
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 maximise the number of \mzninline{all_different} \constraints{} that hold, these \constraints{} are never forced to be \mzninline{false}.
|
|
|
|
|
This means these \constraints{} in a \posc{} context and can be \gls{half-reified}.
|
|
|
|
|
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.
|
|
|
|
|
@ -870,18 +977,18 @@ For each group we show the number of instances solved by the configuration and t
|
|
|
|
|
|
|
|
|
|
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 \variables{}.
|
|
|
|
|
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 in a similar fashion to the adjustments of the general algorithm: explanations used for the violation of the \constraint{} can now be used to set the \gls{cvar} to \mzninline{false} and the explanations given to prune a variable are appended by requirement that the \gls{cvar} is \mzninline{true}.
|
|
|
|
|
These adjustments happen in a similar fashion 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{}.
|
|
|
|
|
Their conjunction then represent the \gls{reif} of the \mzninline{all_different} \constraint{}.
|
|
|
|
|
|
|
|
|
|
\begin{listing}
|
|
|
|
|
\mznfile{assets/listing/half_alldiff.mzn}
|
|
|
|
|
\caption{\label{lst:half-alldiff}The standard \gls{decomp} for \mzninline{all_different} in the \minizinc{} standard library.}
|
|
|
|
|
\caption{\label{lst:half-alldiff}The standard \gls{decomp} for \mzninline{all_different} in the \minizinc{} library.}
|
|
|
|
|
\end{listing}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@ -894,22 +1001,22 @@ Their conjunction, then represent the \gls{reif} of the \mzninline{all_different
|
|
|
|
|
\end{center}
|
|
|
|
|
\end{table}
|
|
|
|
|
|
|
|
|
|
The results in \cref{tab:half-qcp} show that the usage of the specialised \gls{propagator} has a significant advantage over the use of the \gls{decomp}.
|
|
|
|
|
Although it only allows us to solve a one extra instance, there is a significant reduction in solving time for most \instances{}.
|
|
|
|
|
The results in \cref{tab:half-qcp} show that the specialised \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.
|
|
|
|
|
|
|
|
|
|
For our second experiment we consider a variation on the prize collecting travelling salesman problem \autocite{balas-1989-pctsp} referred to as the ``prize collecting path'' problem.
|
|
|
|
|
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 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 \gls{array} lookup \mzninline{pos[next[i]]}, where the \domain{} of \mzninline{next[i]} is larger than the index set of \mzninline{pos}.
|
|
|
|
|
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 result of the \mzninline{element} \constraint{} does not match the value of the index variable.
|
|
|
|
|
The \gls{half-reif} implicitly performs the same task by setting its \gls{cvar} to \mzninline{false} whenever the resulting \variable{} does not 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}
|
|
|
|
|
@ -922,20 +1029,20 @@ Again, for the implementation of the \gls{propagator} of the \gls{half-reif} \co
|
|
|
|
|
\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 usage of the \gls{decomp}.
|
|
|
|
|
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 the usage of \gls{half-reif} on a larger scale.
|
|
|
|
|
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 has propagators 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 the usage of \gls{half-reif}.
|
|
|
|
|
The solving of the linearised \instances{} are tested using the \gls{cbc} and \gls{cplex} \gls{mip} \solvers{}.
|
|
|
|
|
The solving of the Booleanised \instances are testing using the \gls{openwbo} \solver{}.
|
|
|
|
|
is
|
|
|
|
|
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}
|
|
|
|
|
@ -971,23 +1078,24 @@ This replacement happens mostly 1-for-1; the difference between the number of \g
|
|
|
|
|
In many models, no implications can be removed, but for some problems an implication is removed for every \gls{half-reif} that is introduced.
|
|
|
|
|
Finally, the overhead of the introduction of \gls{half-reif} and the newly introduced optimisation techniques is minimal.
|
|
|
|
|
|
|
|
|
|
The \Cref{subtab:half-flat-lin} paints an equally positive picture for the usage of \glspl{half-reif} for linearization.
|
|
|
|
|
Since both \glspl{reif} and \glspl{half-reif} are decomposed during the \gls{rewriting} process, the usage of \gls{half-reif} is able to remove almost 7.5\% of the overall \constraints{}.
|
|
|
|
|
The ratio of \glspl{reif} that is replaced with \glspl{half-reif} is not as high as \gls{gecode}.
|
|
|
|
|
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 optimisation mechanisms have an slightly higher overhead.
|
|
|
|
|
Since there are many more \constraints{}, the introduced optimisation mechanisms have a slightly higher overhead.
|
|
|
|
|
|
|
|
|
|
Finally, statistics for the \gls{rewriting} the \instances{} for a \gls{maxsat} \solver{} is shown in \cref{subtab:half-flat-bool}.
|
|
|
|
|
Unlike linearization, the usage of \gls{half-reif} does not significantly reduces number of \constraints{} and, although still significant, the number of \glspl{reif} is reduced by only slightly over ten percent.
|
|
|
|
|
We also see that that the \gls{booleanization} library is explicitly defined in terms of \glspl{half-reif}.
|
|
|
|
|
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, the usage of \gls{chain-compression} does not seem to have any effect.
|
|
|
|
|
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, the usage of \gls{half-reif} slightly reduces the \gls{rewriting} time as it reduces the workload.
|
|
|
|
|
The relatively small changes shown might indicate that additional work is required to correctly annotate predicates and functions in the Booleanisation library.
|
|
|
|
|
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 Booleanisation 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}
|
|
|
|
|
@ -997,7 +1105,7 @@ The relatively small changes shown might indicate that additional work is requir
|
|
|
|
|
\Cref{tab:half-mznc} shows the results reported by the solvers. The \solver{} reports
|
|
|
|
|
|
|
|
|
|
\begin{description}
|
|
|
|
|
\item[Unsatisfiable] when it proofs the instance does not have a solution,
|
|
|
|
|
\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
|
|
|
|
|
@ -1006,25 +1114,25 @@ The relatively small changes shown might indicate that additional work is requir
|
|
|
|
|
|
|
|
|
|
\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 is this table are very mixed.
|
|
|
|
|
For \gls{gecode}, the usage of \gls{half-reif} does not seem to impact its solving performance.
|
|
|
|
|
Although we would have hoped that propagators for \glspl{half-reif} would be more efficient and reduce the number of propagators scheduled in general.
|
|
|
|
|
Neither number of instances solved, nor the solving time required improved.
|
|
|
|
|
A single instance, however, is negatively impacted by the change; an optimal solution for this instance is no longer found.
|
|
|
|
|
We expect that this \instance{} has benefited from the increased Boolean propagation that is caused by full \gls{reif}.
|
|
|
|
|
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{propagators} 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 solving time required 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} the usage of \gls{half-reif} is clearly a positive one.
|
|
|
|
|
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 linearised instances when using the \gls{cbc} solver seem to have the opposite effect.
|
|
|
|
|
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 pattern, such as cliques, during the pre-processing of the \gls{mip} instance.
|
|
|
|
|
Some patterns can only be detected when using a full \gls{reif}.
|
|
|
|
|
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}.
|
|
|
|
|
With the usage of the \gls{aggregation} and \gls{del-rew}, these can be exceedingly different when using \gls{half-reif}.
|
|
|
|
|
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{}.
|
|
|
|
|
|
