1196 lines
69 KiB
TeX
1196 lines
69 KiB
TeX
%************************************************
|
|
\chapter{Reasoning about Reification}\label{ch:half-reif}
|
|
%************************************************
|
|
|
|
\glsreset{half-reif}
|
|
\glsreset{half-reified}
|
|
\glsreset{reif}
|
|
\glsreset{reified}
|
|
|
|
\input{chapters/4_half_reif_preamble}
|
|
|
|
\section{An Introduction to Half-Reification}
|
|
\label{sec:half-intro}
|
|
|
|
The complex expression language used in \cmls{}, such as \minizinc{}, often requires the use of \gls{reif} in order to arrive at a \gls{slv-mod}.
|
|
If the Boolean expression \mzninline{pred(...)} is seen in a non-\rootc{} context, then a new Boolean \variable{} \mzninline{b} is introduced to replace the expression.
|
|
We call \mzninline{b} the \gls{cvar} of the expression.
|
|
The \gls{rewriting} process then enforces a \constraint{} \mzninline{pred_reif(...,b)}, which binds the \variable{} to be the truth-value of the expression (i.e., \mzninline{b <-> pred(...)}).
|
|
|
|
\textcite{feydy-2011-half-reif} show that although using \gls{reif} in the \gls{rewriting} process is well-understood, it suffers from certain weaknesses.
|
|
|
|
\begin{itemize}
|
|
\item Many \glspl{reif} are created in the \gls{rewriting} of \gls{partial} function calls to accommodate \minizinc{}'s \gls{rel-sem}.
|
|
\item \Glspl{propagator} for the \glspl{reif} of \glspl{global} are scarce.
|
|
\end{itemize}
|
|
|
|
As an alternative, the authors introduce \gls{half-reif}.
|
|
It follows from the idea that in many cases it is sufficient to use the logical implication of an expression, \mzninline{b -> pred(...)}, instead of the logical equivalence, \mzninline{b <-> pred(...)}.
|
|
\Gls{rewriting} with \gls{half-reif} is an approach that improves upon all these weaknesses of \gls{rewriting} with ``full'' \gls{reif}.
|
|
|
|
\begin{itemize}
|
|
\item \Gls{rewriting} using \glspl{half-reif} can lead to significantly better \glspl{slv-mod} when translating \gls{partial} function calls.
|
|
\item \Glspl{propagator} for \glspl{half-reif} can usually be constructed by merely altering a \gls{propagator} implementation for its non-\gls{reified} \constraint{}.
|
|
\end{itemize}
|
|
|
|
Additionally, for many \solvers{} the \gls{decomp} of a \gls{reif} is more complex than the \gls{decomp} of a \gls{half-reif}.
|
|
We will show that using \glspl{half-reif} can therefore lead to a reduction in \gls{native} \constraints{} in the \gls{slv-mod}.
|
|
|
|
\Gls{half-reif} can be used instead of full \gls{reif} when the resulting \gls{cvar} can never be forced to be \false{}.
|
|
This requirement follows from the difference between implication and logical equivalences.
|
|
Setting the left-hand side of an implication to \false{} does not influence the value on the right-hand side.
|
|
This is why the \gls{cvar} should never be forced to be \false{}, since this would not enforce the negation of the \constraint{}.
|
|
Setting the right-hand side of an implication to \true{} also does not influence the left-hand side.
|
|
This is, however, not an issue since in this case the value can just be assigned by the \gls{propagation} of other \constraints{} or a \gls{search-decision}.
|
|
|
|
\begin{example}
|
|
For example, \gls{half-reif} can be used in the following disjunction.
|
|
|
|
\begin{mzn}
|
|
constraint (x = 5) \/ (y = 5);
|
|
\end{mzn}
|
|
|
|
This \constraint{} forces that, between \mzninline{x} and \mzninline{y}, at least one \variable{} is takes the value five.
|
|
The usual \gls{rewriting} would result in the following (intermediate) model, using \glspl{reif} for the equalities.
|
|
|
|
\begin{mzn}
|
|
var bool: b1;
|
|
var bool: b2;
|
|
constraint b1 <-> (x = 5);
|
|
constraint b2 <-> (y = 5);
|
|
constraint b1 \/ b2;
|
|
\end{mzn}
|
|
|
|
However, independent of the value of \mzninline{b1}, if \mzninline{b2} takes the value \true{}, then it can never make the disjunction \false{}.
|
|
Therefore, \gls{propagation} of the disjunction can never force \mzninline{b2} to take the value \false{}.
|
|
Consequently, this means using \gls{half-reif} is \gls{eqsat}.
|
|
\Gls{rewriting} using \gls{half-reif} will result in the following model.
|
|
|
|
\begin{mzn}
|
|
var bool: b1;
|
|
var bool: b2;
|
|
constraint b1 -> (x = 5);
|
|
constraint b2 -> (y = 5);
|
|
constraint b1 \/ b2;
|
|
\end{mzn}
|
|
|
|
\end{example}
|
|
|
|
This property can be extended to include non-Boolean expressions.
|
|
Since Boolean expressions in \minizinc{} can be used in, for example, integer expressions, we can apply similar reasoning to these types of expressions.
|
|
|
|
\begin{example}
|
|
For example, the left-hand side of the following \constraint{} is an integer expression that contains the Boolean expression \mzninline{x = 5}.
|
|
|
|
\begin{mzn}
|
|
constraint count(x in arr)(x = 5) > 5;
|
|
\end{mzn}
|
|
|
|
Making the left-hand side of the \constraint{} larger will only ever help satisfy the \constraint{}.
|
|
This means \gls{propagation} of the expressions \mzninline{x = 5} can never force them to take the value \false{}.
|
|
The \gls{rewriting} process can thus use \glspl{half-reif} instead of \glspl{reif} for these expressions.
|
|
\end{example}
|
|
|
|
To systematically analyse whether Boolean expressions can be \gls{half-reified}, we study the \emph{monotonicity} of \constraints{} w.r.t. an expression.
|
|
A relation \( r(\ldots{}, a, \ldots{}) \) is said to be \emph{monotone} w.r.t. its argument \(a\) when given two possible values for \(a\), \(x\) and \(y\), if \(x > y\), then \(r(\ldots{}, x, \ldots{}) \geq{} r(\ldots{}, y, \ldots{})\), independent of any other arguments.
|
|
Contrariwise, the relation is said to be \emph{antitone} w.r.t. its argument \(a\) if given two possible values for \(a\), \(x\) and \(y\), if \(x > y\), then \(r(\ldots{}, x, \ldots{}) \leq{} r(\ldots{}, y, \ldots{}) \), independent of any other arguments.
|
|
Where, for clarification, we assume \( \false{} < \true{} \).
|
|
|
|
Using these definitions, we introduce extra distinctions in the context of expressions.
|
|
Before, we would merely distinguish between \rootc{} context and non-\rootc{} context.
|
|
Now, we will categorize the latter into the following three contexts.
|
|
|
|
\begin{description}
|
|
|
|
\item[\posc{}] An expression is in \posc{} context when the enclosing \constraint{} (in \rootc{} context) is \textbf{monotone} w.r.t. the expression.
|
|
|
|
\item[\negc{}] An expression is in \negc{} context when the enclosing \constraint{} (in \rootc{} context) is \textbf{antitone} w.r.t. the expression.
|
|
|
|
\item[\mixc{}] An expression is in \mixc{} context when the enclosing \constraint{} (in \rootc{} context) it is \textbf{neither} monotone, nor antitone w.r.t. the expression.
|
|
|
|
\end{description}
|
|
|
|
Determining the monotonicity of a \constraint{} w.r.t. 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 the enclosing \constraint{} is monotone or antitone w.r.t. the expression.
|
|
|
|
Expressions in \posc{} context are the ones we discussed before.
|
|
A Boolean expression in \posc{} context cannot be forced to be \false{}.
|
|
As such, the\gls{half-reif} can be used for expressions in \posc{} context.
|
|
Although expressions in a \negc{} context cannot be directly \gls{half-reified}, the negation of an expression in a \negc{} context can be \gls{half-reified}.
|
|
|
|
\begin{example}
|
|
Consider, for example, the following \constraint{}.
|
|
|
|
\begin{mzn}
|
|
constraint b \/ not (x = 5);
|
|
\end{mzn}
|
|
|
|
The expression \mzninline{x = 5} is in a \negc{} context.
|
|
Although a \gls{half-reif} cannot be used directly, in some cases the \solver{} can negate the expression which then also negates the context to \posc{}.
|
|
Our example can be transformed into the following \constraint{}.
|
|
|
|
\begin{mzn}
|
|
constraint b \/ x != 5;
|
|
\end{mzn}
|
|
|
|
The transformed expression, \mzninline{x != 5}, is now in a \posc{} context.
|
|
We can also speak of this process as ``pushing the negation inwards''.
|
|
\end{example}
|
|
|
|
Expressions in a \mixc{} context are in a position where \gls{half-reif} is impossible.
|
|
Only full \gls{reif} can be used for expressions that are in this context.
|
|
|
|
\begin{example}
|
|
An example of a \constraint{} that introduces \mixc{} contexts is the following.
|
|
|
|
\begin{mzn}
|
|
constraint (x = 5) xor (y = 5);
|
|
\end{mzn}
|
|
|
|
This \constraint{} forces either \mzninline{x} or \mzninline{y}, but not both, to take the value five.
|
|
The equalities in this constraint are in \mixc{} context, because whether \mzninline{y} can and must take the value 5 now directly depends on if \mzninline{x} has already taken the value five, and vice versa.
|
|
As such, when \mzninline{x} takes the value five it forces \mzninline{y} to not take the value five.
|
|
This means we cannot use a \gls{half-reif}, since it does not enforce the negated \constraint{}.
|
|
\end{example}
|
|
|
|
|
|
\section{Propagation and Half-Reification}%
|
|
\label{sec:half-propagation}
|
|
|
|
Logically, there are three tasks that a \gls{propagator} for any \constraint{} must perform:
|
|
|
|
\begin{enumerate}
|
|
\item \(check\) whether the \constraint{} can still be satisfied (and otherwise declare the current state \gls{unsat}),
|
|
\item \(prune\) values from the \glspl{domain} of \variables{} that would violate\glsadd{violated} the \constraint{}, and
|
|
\item check whether the \constraint{} is \(entailed\) (i.e., proven to be \gls{satisfied}).
|
|
\end{enumerate}
|
|
|
|
When creating a \gls{propagator} for the \gls{half-reif} of a \constraint{}, it can be constructed from these tasks.
|
|
The \gls{half-reified} \gls{propagator} is dependent on an additional argument \(b\), the \gls{cvar}.
|
|
The Boolean \variable{} can be in three states, it can currently not have been assigned a value, it can be assigned \true{}, or it can be assigned \false{}.
|
|
Given \(check\), \(prune\), \(entailed\), and \(b\) \cref{alg:half-prop} shows pseudocode for the \gls{propagation} of the \gls{half-reif} of the \constraint{}.
|
|
|
|
\begin{algorithm}[t]
|
|
|
|
\KwIn{The functions \(check\), \(prune\), and \(entailed\) that form the for non-\gls{reified} propagator of \constraint{} \(c\) and a Boolean \gls{cvar} \(b\).
|
|
}
|
|
\KwResult{This pseudocode propagates the \gls{half-reif} of \(c\) (i.e., \(b \implies\ c\)) and returns whether the \constraint is entailed.}
|
|
|
|
\BlankLine{}
|
|
\If{\(b \text{ is unassigned}\)}{
|
|
\If{\(\neg{}check()\)}{
|
|
\(b \longleftarrow \false{}\)\;
|
|
\Return{} \(\true{}\)\;
|
|
}
|
|
}
|
|
\If{\(\texttt{b} = \true{}\)}{
|
|
\(prune()\)\;
|
|
\Return{} \(entailed()\)\;
|
|
}
|
|
\Return{} \(\false{}\)\;
|
|
\caption{\label{alg:half-prop} \gls{propagation} pseudocode for the \gls{half-reif} of a \constraint{} \(c\), based on the \gls{propagator} for \(c\).}
|
|
\end{algorithm}
|
|
|
|
Logically, the creation of \glspl{propagator} for \glspl{half-reif} can always follow this simple principle.
|
|
In practice, however, this is not always possible.
|
|
In some cases, \glspl{propagator} do not explicitly define \(check\) as a separate step.
|
|
Instead, this process can be implicit.
|
|
The \gls{propagator} merely prunes the \glspl{domain} of the \variables{}.
|
|
When a \gls{domain} is found to be empty, then the \gls{propagator} declares the current state \gls{unsat}.
|
|
It is not possible to construct the \gls{half-reified} \gls{propagator} from such an implicit \(check\) operation.
|
|
Instead, a new explicit \(check\) method has to be devised to implement the \gls{propagator} of the \gls{half-reif} \constraint{}.
|
|
|
|
In comparison, a \gls{propagator} for the \gls{reif} of \(c\) cannot be created from these three logical task.
|
|
In addition, we require the logical task from a \gls{propagator} of \(\neg{} c\): \(checkNeg\), \(pruneNeg\), and \(entailedNeg\).
|
|
Using these additional functions, we can define an algorithm for the \gls{propagator}, shown in \cref{alg:reif-prop}
|
|
Although this might seem reasonable for small \constraints{}, such as integer equality, for many \glspl{global} their negation is hard to define.
|
|
\todo{Insert good example of global constraint.}
|
|
|
|
\begin{algorithm}[t]
|
|
|
|
\KwIn{The functions \(check\), \(prune\), and \(entailed\) that form the for non-\gls{reified} propagator of \(c\), The functions \(checkNeg\), \(pruneNeg\), and \(entailedNeg\) that form the for non-\gls{reified} \gls{propagator} of \(\neg{} c\), and a Boolean \gls{cvar} \(b\).
|
|
}
|
|
\KwResult{This pseudocode propagates the \gls{reif} of \(c\) (i.e., \(b \leftrightarrow{} c\)) and returns whether the \constraint{} is entailed.}
|
|
|
|
\BlankLine{}
|
|
\If{\(b \text{ is unassigned}\)}{
|
|
\If{\(\neg{} check()\)}{
|
|
\(b \longleftarrow \false{}\)\;
|
|
}
|
|
\If{\(\neg{} checkNeg()\)}{
|
|
\(b \longleftarrow \true{}\)\;
|
|
}
|
|
}
|
|
\If{\(\texttt{b} = \true{}\)}{
|
|
\(prune()\)\;
|
|
\Return{} \(entailed()\)\;
|
|
}
|
|
\If{\(\texttt{b} = \false{}\)}{
|
|
\(pruneNeg()\)\;
|
|
\Return{} \(entailedNeg()\)\;
|
|
}
|
|
\Return{} \(\false{}\)\;
|
|
\caption{\label{alg:reif-prop} \Gls{propagation} pseudocode for the \gls{reif} of a \constraint{} \(c\), based on the \glspl{propagator} for \(c\) and \(\neg{} c\).}
|
|
\end{algorithm}
|
|
|
|
\Gls{half-reified} \glspl{propagator} have certain advantages over \gls{reified} \glspl{propagator}, but also may suffer certain penalties.
|
|
\Gls{half-reif} can cause \glspl{propagator} that use their \gls{cvar} to wake up less frequently: \glspl{cvar} that are \gls{fixed} to \true{} by full \gls{reif} will never be fixed by \gls{half-reif}.
|
|
This can be advantageous, but has a corresponding disadvantage.
|
|
When a \gls{cvar} is fixed, it can allow the simplification of the \glspl{propagator} that use them, and hence make \gls{propagation} faster.
|
|
|
|
When a full \gls{reif} is required, we can still use \gls{half-reified} \glspl{propagator} to implement it.
|
|
A full \gls{reif} \mzninline{x <-> pred(...)} can be propagated using its \gls{half-reified} \gls{propagator}, \mzninline{x -> pred(...)}, the \gls{half-reified} \gls{propagator} of its negation, \mzninline{y -> not pred(...)}, and the \constraint{} \mzninline{x <-> not y}.
|
|
This does not lose \gls{propagation} strength.
|
|
For Booleans appearing in \posc{} context we can make the \gls{propagator} of the negated \gls{half-reif} run at the lowest priority, since it will never detect if the state is \gls{unsat}.
|
|
Similarly, in \negc{} context we can make the propagator \mzninline{b -> pred(...)} run at the lowest priority.
|
|
This means that the \glspl{cvar} are still fixed at the same time, but there is less overhead.
|
|
|
|
In \cref{sec:half-experiments} we assess the implementation of \glspl{propagator} for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element} based on these principles.
|
|
|
|
\section{Decomposition and Half-Reification}%
|
|
\label{sec:half-decomposition}
|
|
|
|
The use of \gls{half-reif} does not only offer a benefit when a \gls{propagator} for the \gls{half-reified} \constraint{} is available.
|
|
It can also be beneficial in the \gls{decomp} of \constraints{}.
|
|
Compared to full \gls{reif}, the \gls{decomp} of a \gls{half-reif} does not have to implement the negation of the \constraint{}, and can therefore often be much more compact than the fully \gls{reified} version.
|
|
In particular, this can be beneficial when the target \solver{} is a \gls{mip} or \gls{sat} \solver{}.
|
|
The \glspl{decomp} for these \solver{} technologies often explicitly encode \gls{reified} \constraints{} using two implications.
|
|
If, however, a \gls{reif} is replaced by a \gls{half-reif}, then only one of these implications is required.
|
|
|
|
\begin{example}
|
|
|
|
Consider the \gls{reif} of the \constraint{} \mzninline{i <= 4} using the \gls{cvar} \mzninline{b}, where \mzninline{i} can take values in the domain \mzninline{0..10}.
|
|
If the target \solver{} is a \gls{mip} \solver{}, then this \gls{reif} would be linearized.
|
|
It would take the following form.
|
|
|
|
\begin{mzn}
|
|
constraint i <= 10 - 6 * b; % b -> i <= 4
|
|
constraint i >= 5 - 5 * b; % not b -> i >= 5
|
|
\end{mzn}
|
|
|
|
Instead, if we could determine that the \constraint{} could be \gls{half-reified}, then the \gls{linearization} could be simplified to only the first \constraint{}.
|
|
\end{example}
|
|
|
|
The same principle can be applied all throughout the \gls{linearization} process.
|
|
Ultimately, \minizinc{}'s \gls{linearization} library rewrites most \glspl{reif} in terms of implied less than or equal to \constraints{}.
|
|
For all these \glspl{reif}, replacement by a \gls{half-reif} can remove half of the implications.
|
|
|
|
For \gls{sat} solvers, a \gls{decomp} for a \gls{half-reif} can be created from its regular \gls{decomp}.
|
|
Any \constraint{} \(c\) will decompose into \gls{cnf} of the following form.
|
|
\[ c = \forall_{i} \exists_{j} lit_{ij} \]
|
|
The \gls{half-reif}, with \gls{cvar} \texttt{b}, could take the following encoding.
|
|
\[ \texttt{b} \implies c = \forall_{i} \neg \texttt{b} \lor \exists_{j} lit_{ij} \]
|
|
The transition from the \gls{cnf} of the regular \constraint{} \(c\) to its \gls{half-reif} \(\texttt{b} \implies{} c\) only adds a single literal to each clause.
|
|
|
|
It is, however, not as straightforward to construct its full \gls{reif}.
|
|
In addition to the \gls{half-reified} \gls{cnf}, a generic \gls{reif} would require the implication \(\neg \texttt{b} \implies \neg c\).
|
|
Based on the \gls{cnf} of \(c\), this would result in the following logical formula:
|
|
\[ \neg b \implies \neg c = \forall_{i} b \lor \neg \exists_{j} lit_{ij} \]
|
|
This formula, however, is not direct set of clauses.
|
|
Rewriting this formula into \gls{cnf} would result in:
|
|
\[ \neg b \implies \neg c = \forall_{i,j} b \lor lit_{ij} \]
|
|
It adds a new binary clause for every literal in the original \gls{cnf}.
|
|
In general, many more clauses are needed to decompose a \gls{reif} compared to a \gls{half-reif}.
|
|
|
|
According to the principles above, \gls{decomp} libraries for the full \minizinc{} language have been implemented for \gls{mip} and \gls{sat} \solvers{}.
|
|
In \cref{sec:half-experiments} we assess the effects when \gls{rewriting} with \gls{half-reif}.
|
|
|
|
\section{Context Analysis}%
|
|
\label{sec:half-context}
|
|
|
|
The context of an expression cannot always be determined by merely considering \minizinc{} expressions top-down.
|
|
Expressions bound to an identifier can be used multiple times in expressions that influence their context.
|
|
|
|
\begin{example}
|
|
Consider the following \minizinc{} fragment.
|
|
|
|
\begin{mzn}
|
|
constraint let {
|
|
var bool: x = pred(a, b, c);
|
|
} in y -> x /\ x -> z;
|
|
\end{mzn}
|
|
|
|
The result of predicate call \mzninline{pred(a, b, c)} is bound to the identifier \mzninline{x}.
|
|
If \mzninline{x} is only used in a \posc{} context, then the call itself is in a \posc{} context as well.
|
|
As such, the call could then be \gls{half-reified}.
|
|
|
|
Although this is the case on the left side of the conjunction, the other side uses \mzninline{x} in a \negc{} context.
|
|
This means that \mzninline{pred(a, b, c)} is in a \mixc{} context and must be fully \gls{reified}.
|
|
\end{example}
|
|
|
|
Note that an alternative approach for this example would be to replace the identifier with its definition.
|
|
It would then be possible to use \gls{half-reified} versions of both the call and the negation of the call.
|
|
Although this would increase the use of \gls{half-reif}, it should be noted that the \gls{propagation} of these two \glspl{half-reif} would be equivalent to the \gls{propagation} of the full \gls{reif} of the call.
|
|
In this scenario, we prefer to create the full \gls{reif} as it decreases the number of \variables{} and \constraints{} in the model.
|
|
|
|
When taking into account the possible undefinedness of an expression, every expression in a \minizinc{} model has two different contexts: the context in which the expression itself occurs, its \emph{value context}, and the context in which the partiality of the expression is captured, its \emph{partiality context}.
|
|
As described in \cref{subsec:back-mzn-partial}, \minizinc{} uses \gls{rel-sem} for partial functions.
|
|
This means that if the result of a function is undefined, then its nearest enclosing Boolean expression becomes \false{}.
|
|
In practice, this means that a condition that tests if the function will return a value is added to the nearest enclosing Boolean expression.
|
|
The partiality context is the context in which this condition is placed.
|
|
|
|
\begin{example}
|
|
We can illustrate the difference between the two contexts in the following \minizinc{} fragment.
|
|
|
|
\begin{mzn}
|
|
var 0..10: x
|
|
constraint b \/ y div x < 4;
|
|
\end{mzn}
|
|
|
|
In this fragment, we study the context of the division expression \mzninline{y div x}.
|
|
The expression itself return an integer \variable{}, and it used on the left-hand side of a less than \constraint{}.
|
|
This result is therefore in a \negc{} context: it is only forced to take a smaller value.
|
|
This is its value context.
|
|
|
|
However, since the \domain{} of \mzninline{x} includes zero, \gls{rewriting} \mzninline{x div y} will introduce the condition under which its result can be used.
|
|
In this case, the expression \mzninline{x != 0} is added to the right-hand side of the disjunction as follows.
|
|
|
|
\begin{mzn}
|
|
var 0..10: x
|
|
constraint b \/ ( x != 0 /\ y div x < 4);
|
|
\end{mzn}
|
|
|
|
\noindent{}The partiality context of the division is the context in which this condition is added.
|
|
Here, the condition is added in a \posc{} context.
|
|
\end{example}
|
|
|
|
\subsection{Automated analysis}%
|
|
\label{subsec:half-automated}
|
|
|
|
In the architecture introduced in \cref{ch:rewriting}, contexts of the expressions can be determined automatically.
|
|
The analysis is best performed during the compilation process from \minizinc{} to \microzinc{}.
|
|
It requires knowledge about all usages of each \variable{} at the same time.
|
|
This information is not available during the interpretation of \microzinc{}.
|
|
Without loss of generality we can define the context analysis for \microzinc{} models.
|
|
This has the advantage that \microzinc{} does not contain \gls{partial} function calls.
|
|
The partiality in \minizinc{} has already been translated using only total functions (see \cref{sec:rew-micronano}).
|
|
The context analysis therefore does not have to keep track of value and partiality contexts separately.
|
|
|
|
We describe the context analysis performed on the \microzinc{} syntax in the form of inference rules.
|
|
The full set of rules appears in \cref{fig:half-analysis-expr,fig:half-analysis-it}.
|
|
Each rule describes how an expression that is found in a context \(ctx\), above the line, changes the context of subordinate expressions, below the line.
|
|
The syntax \ctxeval{e}{ctx} is used to assert that the expression \(e\) is evaluated in the context \(ctx\).
|
|
We now specify two context transformations that will be used in further algorithms to transition between different contexts: \changepos{} and \changeneg{}.
|
|
The behaviour of these transformations is shown in \cref{fig:half-ctx-trans}.
|
|
|
|
\begin{figure*}
|
|
\begin{center}
|
|
\begin{tabular}{ccc}
|
|
\(
|
|
\begin{array}{lcl}
|
|
\changepos \rootc & = & \posc \\
|
|
\changepos \posc & = & \posc \\
|
|
\changepos \negc & = & \negc \\
|
|
\changepos \mixc & = & \mixc
|
|
\end{array}
|
|
\)
|
|
& ~ &
|
|
\(
|
|
\begin{array}{lcl}
|
|
\changeneg \rootc & = & \negc \\
|
|
\changeneg \posc & = & \negc \\
|
|
\changeneg \negc & = & \posc \\
|
|
\changeneg \mixc & = & \mixc
|
|
\end{array}
|
|
\)
|
|
\end{tabular}
|
|
\end{center}
|
|
\caption{\label{fig:half-ctx-trans} Definitions of the \changepos{} and \changeneg{} context transitions.}
|
|
\end{figure*}
|
|
|
|
\begin{figure*}
|
|
\centering
|
|
\begin{prooftree}
|
|
\hypo{\ctxeval{x}{ctx}}
|
|
\infer1[(Ident)]{\text{pushCtx}(x, ctx)}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\ctxeval{ident\texttt{(} e_{1}, \ldots, e_{n} \texttt{)}}{ctx}}
|
|
\hypo{\text{argCtx}(ident, ctx) = \tuple{ ctx'_{1}, \ldots, ctx'_{n}}}
|
|
\infer2[(Call)]{\ctxfunc{ident}{ctx},~\ctxeval{e_{1}}{ctx'_{1}},~\ldots,~ \ctxeval{e_{n}}{ctx'_{n}}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\ctxeval{x\texttt{[}i\texttt{]}}{ctx}}
|
|
\infer1[(Access)]{\ctxeval{x}{\changepos{}ctx}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\ctxeval{\texttt{if }b\texttt{ then } e_{1} \texttt{ else } e_{2} \texttt{ endif}}{ctx}}
|
|
\infer1[(ITE)]{\ctxeval{b}{ctx},~\ctxeval{e_{1}}{\changepos{}ctx},~\ctxeval{e_{2}}{\changepos{}ctx}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\ctxeval{\texttt{[}e~\texttt{|}~G\texttt{]}}{ctx}}
|
|
\infer1[(Compr)]{\ctxeval{e}{ctx}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\ctxeval{\texttt{[}e_{1}, \ldots, e_{n}\texttt{]}}{ctx}}
|
|
\infer1[(Arr)]{\ctxeval{e_{1}}{ctx}, \ldots, \ctxeval{e_{n}}{ctx}}
|
|
\end{prooftree}
|
|
\caption{\label{fig:half-analysis-expr} Context inference rules for \microzinc{} expressions.}
|
|
\end{figure*}
|
|
|
|
\Cref{fig:half-analysis-expr} shows the inference rules for all \microzinc{} expressions, apart from \glspl{let}.
|
|
The first rule, (Ident), is unique in the sense that the context of an identifier does not directly affect other expressions.
|
|
Instead, every context in which the identifier is found is collected and will be processed when evaluating the corresponding declaration.
|
|
Note that the presented inference rules do not have any explicit state object.
|
|
Instead, we introduce the functions ``pushCtx'' and ``collectCtx''.
|
|
These functions track and combine the contexts in which a value is used in an implicit global state.
|
|
|
|
Most changes in the context of \microzinc{} expressions stem from the (Call) rule.
|
|
A call expression can change the context in which its arguments should be evaluated.
|
|
As an input to the inference process, a ``argCtx'' function is used to give the context of the arguments of a function, given the function itself and the context of the call.
|
|
A definition for this function for the \minizinc{} operators can be found in \cref{alg:arg-ctx}.\footnote{We use \minizinc\ operator syntax instead of \microzinc{} identifiers for brevity and clarity.}
|
|
|
|
Although a standard definition for the ``argCtx'' function may cover the most common cases, it does not cover user-defined functions.
|
|
To address this issue, we introduce the \glspl{annotation} \mzninline{promise_ctx_monotone} and \mzninline{promise_ctx_antitone} to represent the operations \changepos{} and \changeneg{} respectively.
|
|
When a function argument is annotated with one of these \glspl{annotation}, the context of the argument in a call in context \(ctx\) is transformed with the operation corresponding to the annotation (e.g., \(\changepos{}ctx\) or \(\changeneg{}ctx\)).
|
|
If a function argument is not annotated, then the argument is evaluated in \mixc{} context.
|
|
It may be possible to infer these \glspl{annotation} from the function body.
|
|
However, we currently do not provide such analysis and annotate functions by hand.
|
|
|
|
\begin{example}
|
|
Consider the user-defined \minizinc{} implementation of a logical implication in \cref{lst:half-impli}.
|
|
The \glspl{annotation} placed on the argument of the \mzninline{impli} function will apply the same context transformations as the \mzninline{->} operator shown in \cref{alg:arg-ctx}.
|
|
In terms of context analysis, this function now is equivalent to the \minizinc{} operator.
|
|
\end{example}
|
|
\begin{listing}
|
|
\mznfile{assets/listing/half_impli.mzn}
|
|
\caption{\label{lst:half-impli} A user-defined predicate of a logical implication using \glspl{annotation} to define the context usage of its arguments.}
|
|
\end{listing}
|
|
|
|
\begin{algorithm}
|
|
\KwIn{A \minizinc{} operator \(op\) and calling context \(ctx\)}
|
|
|
|
\KwOut{A tuple containing the contexts of the arguments \(\tuple{ctx_{1}, \ldots{}, ctx_{n}}\)}
|
|
|
|
\Switch{op}{
|
|
\Case{\mzninline{ not }}{
|
|
\Return{\tuple{\changeneg{}ctx}}
|
|
}
|
|
\Case{\mzninline{ \/ }, \mzninline{+ }}{
|
|
\Return{\tuple{\changepos{}ctx, \changepos{}ctx}}
|
|
}
|
|
\Case{\mzninline{ -> }, \mzninline{< }, \mzninline{<= }}{
|
|
\Return{\tuple{\changeneg{}ctx, \changepos{}ctx}}
|
|
}
|
|
\Case{\mzninline{ > }, \mzninline{>= }, \mzninline{- }}{
|
|
\Return{\tuple{\changepos{}ctx, \changeneg{}ctx}}
|
|
}
|
|
\Case{\mzninline{ <-> }, \mzninline{= }, \mzninline{xor }, \mzninline{* }}{
|
|
\Return{\tuple{\mixc, \mixc}}
|
|
}
|
|
\Case{\mzninline{ /\ }}{
|
|
\Return{\tuple{ctx, ctx}}
|
|
}
|
|
\Other{
|
|
\Return{\tuple{\mixc, \ldots, \mixc}}
|
|
}
|
|
}
|
|
\caption{\label{alg:arg-ctx} Definition of the ``argCtx'' function for \minizinc{} operators.}
|
|
\end{algorithm}
|
|
|
|
The context in which the result of a call expression is used must also be considered.
|
|
The (Call) rule, therefore, introduces the \ctxfunc{ident}{ctx} syntax.
|
|
This syntax is used to declare that the \compiler{} must introduce a \microzinc{} function variant that rewrites the function call to \(ident\) in the context \(ctx\).
|
|
This means that if \(ctx\) is \rootc{}, the \compiler{} can use the function as defined.
|
|
Otherwise, the \compiler{} follows the following steps to try to introduce the most compatible variant of the function:
|
|
|
|
\begin{enumerate}
|
|
\item If a direct definition for \(ctx\) definition exists, then use this definition.
|
|
|
|
\begin{description}
|
|
\item[\posc] \glspl{half-reif} can be defined as \(ident\)\mzninline{_imp}.
|
|
\item[\negc] negations of \glspl{half-reif} can be defined as \(ident\)\mzninline{_imp_neg}.
|
|
\item[\mixc] \glspl{reif} can be defined as \(ident\)\mzninline{_reif}.
|
|
\end{description}
|
|
|
|
\item If \(ident\) is a \microzinc{} function with an expression body \(E\), then a copy of the function can be made that is evaluated in the desired context: \ctxeval{E}{ctx}.
|
|
|
|
\item If \(ctx\) is \posc{} or \negc{}, then change \(ctx\) to \mixc{} and return to step 1.
|
|
|
|
\item Finally, if none of the earlier steps were successful, then the compilation fails.
|
|
Note that this can only occur when there is not a definition for the \gls{reif} of a \constraint{}, i.e., neither a \gls{native} constraint nor a \gls{decomp}.
|
|
\end{enumerate}
|
|
|
|
The (Access) and (ITE) rules show the context inference for \gls{array} access and \gls{conditional} expressions respectively.
|
|
Their inner expressions are evaluated in \(\changepos{}ctx\).
|
|
The inner expressions cannot be simply be evaluated in \(ctx\), because it is not yet certain which expression will be chosen.
|
|
This is important for when \(ctx\) is \rootc{}, since we, at compile time, cannot say which expression will hold globally.
|
|
We will revisit this issue in \cref{subsec:half-?root}.
|
|
|
|
Finally, the (Compr) and (Arr) rules show simple inference rules for \gls{array} construction expressions.
|
|
If such an expression is evaluated in the context \(ctx\), then its members can be evaluated in the same context \(ctx\).
|
|
|
|
\begin{figure*}
|
|
\centering
|
|
\begin{prooftree}
|
|
\hypo{\ctxeval{\texttt{let \{ }I\texttt{ \} in } e}{ctx}}
|
|
\infer1[(Let)]{\ctxeval{e}{ctx}, \ctxitem{I} }
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\ctxitem{I \texttt{; constraint } e }}
|
|
\infer1[(Con)]{\ctxeval{e}{\rootc},~\ctxitem{I}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\ctxitem{I \texttt{; } T: x \texttt{ = } e }}
|
|
\hypo{\text{collectCtx}(x) = [ctx_{1}, \ldots, ctx_{n}]}
|
|
\infer2[(Assign)]{\ctxeval{e}{\text{join}([ctx_{1}, \ldots, ctx_{n}])},~\ctxitem{I}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\ctxitem{I \texttt{; } \texttt{tuple(}\ldots\texttt{):}~x \texttt{ = (} e_{1}, \ldots, e_{n}\texttt{)}}}
|
|
\hypo{\text{collectCtx}(x) = \tuple{ctx_{1}, \ldots, ctx_{n}}}
|
|
\infer2[(TupC)]{\ctxeval{e_{1}}{ctx_{1}}, \ldots, \ctxeval{e_{n}}{ctx_{n}}, ~\ctxitem{I}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\ctxitem{I \texttt{; (} T_{1}: x_{1}, \ldots, T_{n}: x_{n} \texttt{) = } e }}
|
|
\infer[no rule]1{\text{collectCtx}(x_{1}) = [ctx^{1}_{1}, \ldots, ctx^{1}_{k}], \ldots, \text{collectCtx}(x_{n}) = [ctx^{n}_{1}, \ldots, ctx^{n}_{l}]}
|
|
\infer1[(TupD)]{\ctxeval{e}{\tuple{\text{join}\left(\left[ctx^{1}_{1}, \ldots, ctx^{1}_{k}\right]\right), \ldots, \text{join}\left(\left[ctx^{n}_{1}, \ldots, ctx^{n}_{l}\right]\right)}},~\ctxitem{I}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\ctxitem{I \texttt{; } T: x}}
|
|
\infer1[(Decl)]{}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\ctxitem{\epsilon{}}}
|
|
\infer1[(Item0)]{}
|
|
\end{prooftree}
|
|
\caption{\label{fig:half-analysis-it} Context inference rules for \microzinc{} let-expressions.}
|
|
\end{figure*}
|
|
|
|
\Cref{fig:half-analysis-it} shows the inference rules for \glspl{let} and their inner items.
|
|
The first rule, (Let), propagates the context in which the expression is evaluated, \(ctx\), directly to the \mzninline{in}-expression.
|
|
Thereafter, the analysis will continue by iterating over its inner items.
|
|
This is described using the syntax \ctxitem{I}.
|
|
Note that the \(ctx\) of the \gls{let} itself, is irrelevant for the analysis of its inner items.
|
|
|
|
The inference for \constraint{} items is described by the (Con) rule.
|
|
Since all expressions in well-formed \microzinc{} are total, the \constraint{} can be assumed to hold globally.
|
|
And, unlike \minizinc{}, the \constraint{} is not dependent on the context of the \gls{let}.
|
|
The \constraint{}'s expression is evaluated in \rootc{} context.
|
|
|
|
The (Assign) rule reasons about declarations that have a right-hand side.
|
|
The expression that is assigned to the identifier must be evaluated in the combined context of its usages.
|
|
As previously discussed, the contexts in which the identifier was used can be retrieved using the ``collectCtx'' function.
|
|
These contexts are then combined using a ``join'' function.
|
|
This function repeatedly applies the symmetric join operation described by \cref{fig:half-join}.
|
|
The right-hand expression of the item is then evaluated in the resulting context.
|
|
|
|
\begin{figure*}
|
|
\begin{center}
|
|
\begin{tabular}{r | c c c c}
|
|
join & \rootc & \posc & \negc & \mixc \\
|
|
\hline
|
|
\rootc & \rootc & \rootc & \rootc & \rootc \\
|
|
\posc & \rootc & \posc & \mixc & \mixc \\
|
|
\negc & \rootc & \mixc & \negc & \mixc \\
|
|
\mixc & \rootc & \mixc & \mixc & \mixc \\
|
|
\end{tabular}
|
|
\end{center}
|
|
\caption{\label{fig:half-join} A table showing the result of joining two contexts.}
|
|
\end{figure*}
|
|
|
|
(TupC) and (TupD) handle the context inference during the construction and destructuring of tuples respectively.
|
|
The context of the individual members of tuples is tracked separately.
|
|
This means that individual members of a tuple, like the value and the partiality of a \minizinc{} expression, may be evaluated in different contexts.
|
|
|
|
Finally, the (Decl) and (Item0) rules describe two base cases in the inference.
|
|
The declaration item of a \variable{} does not further affect the context, and does not depend on it.
|
|
It merely triggers the creation of a new \variable{}.
|
|
The (Item0) rule is triggered when the inner items in the let-expression have been depleted.
|
|
|
|
\subsection{Potentially Root}%
|
|
\label{subsec:half-?root}
|
|
|
|
In the previous section, we briefly discussed the context transformations for the (Access) and (ITE) rules in \cref{fig:half-analysis-expr}.
|
|
Different from the rules described, when an \gls{array} access or \gls{conditional} expression is found in \rootc{} context, it often makes sense to evaluate its sub-expression in \rootc{} context as well.
|
|
It is, however, not always safe to do so.
|
|
|
|
\begin{example}
|
|
\label{ex:half-maybe-root}
|
|
|
|
For example, consider the following \microzinc{} fragment.
|
|
|
|
\begin{mzn}
|
|
constraint if b then
|
|
F(x, y, z)
|
|
else
|
|
G(x, y, z)
|
|
endif;
|
|
\end{mzn}
|
|
|
|
Let us assume that \mzninline{b} is a \parameter{}, but that its value is not known during the compilation from \minizinc{} to \microzinc{}.
|
|
In this case, we know that only one side of the \gls{conditional} expression will be evaluated, and that call will then globally constrain the \cmodel{}.
|
|
As such, the \compiler{} can output calls to the \rootc{} variant of the functions.
|
|
This will enforce the \constraint{} in the most efficient way.
|
|
|
|
Things, however, change when the situation gets more complex.
|
|
Consider the following \microzinc{} fragment.
|
|
|
|
\begin{mzn}
|
|
let {
|
|
var bool: p = F(x, y, z);
|
|
var bool: q = G(x, y, z);
|
|
constraint if b then p else q endif;
|
|
var bool: ret = bool_or(p, r);
|
|
} in ret;
|
|
\end{mzn}
|
|
|
|
One side of the \gls{conditional} expression is also used in a disjunction.
|
|
If \mzninline{b} evaluates to \true{}, then \mzninline{p} is evaluated in \rootc{} context, and \mzninline{p} can take the value \true{} in the disjunction.
|
|
Otherwise, \mzninline{q} is evaluated in \rootc{} context, and \mzninline{p} in the disjunction must be evaluated in \posc{} context.
|
|
In this situation, it is not safe for the \compiler{} to output calls for the \rootc{} variants of these calls.
|
|
\end{example}
|
|
|
|
Using the \changepos{} transformation for sub-expressions contexts is safe, but it places a large burden on the \solver{}.
|
|
The solver performs better without using \gls{reif}.
|
|
|
|
To detect the situation where the sub-expression are only used in an \gls{array} access or \gls{conditional} expression we introduce the \mayberootc{} context.
|
|
This context functions as a ``weak'' \rootc{} context.
|
|
If it is joined with any other context, then it acts as \posc{}.
|
|
The extended join operation is shown in \cref{fig:half-maybe-join}.
|
|
Otherwise, it will act as a normal \rootc{} context.
|
|
|
|
\begin{figure*}
|
|
\begin{center}
|
|
\begin{tabular}{r | c c c c c}
|
|
join & \rootc & \mayberootc & \posc & \negc & \mixc \\
|
|
\hline
|
|
\rootc & \rootc & \rootc & \rootc & \rootc & \rootc \\
|
|
\mayberootc & \rootc & \mayberootc & \posc & \mixc & \mixc \\
|
|
\posc & \rootc & \posc & \posc & \mixc & \mixc \\
|
|
\negc & \rootc & \mixc & \mixc & \negc & \mixc \\
|
|
\mixc & \rootc & \mixc & \mixc & \mixc & \mixc \\
|
|
\end{tabular}
|
|
\end{center}
|
|
\caption{\label{fig:half-maybe-join} A table showing the result of joining two contexts, considering the \mayberootc{} context.}
|
|
\end{figure*}
|
|
|
|
\begin{figure*}
|
|
\centering
|
|
\begin{prooftree}
|
|
\hypo{\ctxeval{x\texttt{[}i\texttt{]}}{\rootc}}
|
|
\infer1[(Access-R)]{\ctxeval{x}{\mayberootc}}
|
|
\end{prooftree} \\
|
|
\bigskip
|
|
\begin{prooftree}
|
|
\hypo{\ctxeval{\texttt{if }b\texttt{ then } e_{1} \texttt{ else } e_{2} \texttt{ endif}}{\rootc}}
|
|
\infer1[(ITE-R)]{\ctxeval{c}{ctx},~\ctxeval{e_{1}}{\mayberootc},~\ctxeval{e_{2}}{\mayberootc}}
|
|
\end{prooftree}
|
|
\caption{\label{fig:half-analysis-maybe-root} Updated context inference rules for \mayberootc{}.}
|
|
\end{figure*}
|
|
|
|
\Cref{fig:half-analysis-maybe-root} shows the additional inference rules for \gls{array} access and \gls{conditional} expressions.
|
|
Looking back at \cref{ex:half-maybe-root}, these additional rules and updated join operation will ensure that the first case will correctly use \rootc{} context calls.
|
|
For the second case, however, it detects that \mzninline{p} is used in both \posc{} and \mayberootc{} context.
|
|
Therefore, it will output the \posc{} call for the right-hand side of \mzninline{p}, even when \mzninline{b} evaluates to \true{}.
|
|
At compile time, this is the only correct context to use.
|
|
We will, however, discuss how to adjust contexts dynamically during \gls{rewriting} in \cref{subsec:half-dyn-context}.
|
|
|
|
\section{Rewriting and Half-Reification}%
|
|
\label{sec:half-rewriting}
|
|
|
|
During the \gls{rewriting} process the contexts assigned to the different expressions can be used directly to determine if and how an expression has to be \gls{reified}.
|
|
|
|
\begin{example}
|
|
\label{ex:half-rewriting}
|
|
|
|
Consider the \gls{rewriting} of the following \constraint{}.
|
|
|
|
\begin{mzn}
|
|
constraint (y -> f(x)) \/ not x = 5;
|
|
\end{mzn}
|
|
|
|
\noindent{}We will assume \mzninline{f} is a \gls{native} \constraint{} that can be both \gls{reified} or \gls{half-reified}.
|
|
For this \constraint{} we can determine the following contexts for its sub-expressions:
|
|
|
|
\begin{itemize}
|
|
\item the disjunction itself is in \rootc{} context,
|
|
\item \mzninline{y} and \mzninline{x = 5} are in \negc{} context,
|
|
\item and the rest are in \posc{} context.
|
|
\end{itemize}
|
|
|
|
\Gls{rewriting} using full \gls{reif} could produce the following \gls{native} \constraints{}.
|
|
|
|
\begin{mzn}
|
|
constraint bool_clause([b1, b2], []); % b1 \/ b2
|
|
constraint bool_clause_reif([b3], [y], b1); % b1 <-> y -> b3
|
|
constraint f_reif(x, b3); % b3 <-> f(x)
|
|
constraint bool_not(b4, b2); % b2 <-> not b4
|
|
constraint int_eq_reif(x, 5, b4); % b4 <-> x = 5
|
|
\end{mzn}
|
|
|
|
\Gls{rewriting} using \gls{half-reif} can simplify it to the following \gls{native} \constraints{}.
|
|
|
|
\begin{mzn}
|
|
constraint bool_clause([b1, b2], []); % b1 \/ b2
|
|
constraint bool_clause_imp([b3], [y], b1); % b1 -> (y -> b3)
|
|
constraint f_imp(x, b3); % b3 -> f(x)
|
|
constraint int_ne_imp(x, 5, b2); % b2 -> x != 5
|
|
\end{mzn}
|
|
|
|
We are able to replace the two \glspl{reif} and push the negation inwards, transforming the equals \constraint{} into a not equals \constraint{}.
|
|
Note, however, that the rewriting produced many extra implications.
|
|
If the Boolean \mzninline{y} was not further constrained in the problem, then we could further reduce it to the following \constraints{}.
|
|
|
|
\begin{mzn}
|
|
constraint bool_clause([y, b2], []); % y \/ b2
|
|
constraint f_imp(x, y); % y -> f(x)
|
|
constraint int_ne_imp(x, 5, b2); % b2 -> x != 5
|
|
\end{mzn}
|
|
|
|
\end{example}
|
|
|
|
As this example shows, the use of \gls{half-reif} can form so-called \glspl{implication-chain}.
|
|
This happens when the right-hand side of an implication is \gls{half-reified} and a \gls{cvar} is created to represent the expression.
|
|
Instead, we could have used the left-hand side of the implication as the \gls{cvar} of the \gls{half-reified} \constraint{}.
|
|
In next section, we present a new post-processing method we call \gls{chain-compression}.
|
|
It can be used to eliminate these \glspl{implication-chain}.
|
|
|
|
The \gls{rewriting} with \gls{half-reif} also interacts with some simplification methods used during the \gls{rewriting} process.
|
|
Most importantly, \gls{half-reif} has to be considered when using \gls{cse}, and \gls{propagation} can change the context of an expression.
|
|
In \cref{subsec:half-cse} we will discuss how \gls{cse} can be adjusted to handle \gls{half-reif}.
|
|
Finally, in \cref{subsec:half-dyn-context} we will discuss how the context in which an expression is evaluated can be adjusted during the \gls{rewriting} process.
|
|
|
|
\subsection{Chain compression}%
|
|
\label{subsec:half-compress}
|
|
|
|
\Gls{rewriting} with \gls{half-reif} will in many cases result in \glspl{implication-chain}: \mzninline{b1 -> b2 /\ b2 -> c}, where \texttt{b2} does not occur elsewhere.
|
|
In this case the conjunction can be replaced by \mzninline{b1 -> c} and \texttt{b2} can be removed from the \cmodel{}.
|
|
The case shown in the example can be generalized to
|
|
|
|
\begin{mzn}
|
|
constraint b1 -> b2 /\ forall(i in N)(b2 -> c[i])
|
|
\end{mzn}
|
|
|
|
\noindent{}which, if \texttt{b2} does not occur elsewhere in the \instance{}, can be resolved to
|
|
|
|
\begin{mzn}
|
|
constraint forall(i in N)(b1 -> c[i])
|
|
\end{mzn}
|
|
|
|
\noindent{}after which \texttt{b2} can be removed from the model.
|
|
|
|
An algorithm to remove these chains of implications is best comprehended through the use of an implication graph.
|
|
An implication graph \(\tuple{V,E}\) is a directed graph.
|
|
The vertices \(V\) represent the \variables{} in the \instance{}.
|
|
An edge \((x,y) \in E\) represents the presence of an implication \mzninline{x -> y} in the instance.
|
|
Additionally, the algorithm requires vertices to be marked when their corresponding \variables{} are used in other \constraints{} in the \cmodel{}.
|
|
The goal of the algorithm is now to identify and remove vertices that are not marked and have only one incoming edge.
|
|
\Cref{alg:half-compression} provides a formal specification of the \gls{chain-compression} method in pseudocode.
|
|
|
|
\begin{algorithm}
|
|
\KwIn{An implication \constraint{} graph \(G=\tuple{V, E}\) and a set \(M
|
|
\subseteq{} V\) of vertices used in other \constraints{}.}
|
|
|
|
\KwOut{An equisatisfiable graph \(G'=\tuple{V', E'}\) where chained
|
|
implications have been removed.}
|
|
|
|
\(V' \longleftarrow V\)\;
|
|
\(E' \longleftarrow E\)\;
|
|
\For{\( x \in V \backslash{} M \)} {
|
|
\Switch{\( \left\{ a~|~(a,x) \in E \right\} \)}{
|
|
\Case{\( \left\{ a \right \} \)}{
|
|
\For{\((x, b) \in E\)}{
|
|
\(E' \longleftarrow E' \cup \{ (a,b) \} \)\;
|
|
\(E' \longleftarrow E' \backslash \{ (x,b) \} \)\;
|
|
}
|
|
\(E' \longleftarrow E' \backslash \{ (a,x) \} \)\;
|
|
\(V' \longleftarrow V' \backslash \{ x \} \)\;
|
|
}
|
|
}
|
|
}
|
|
\(G' \longleftarrow \tuple{V', E'}\)\;
|
|
\caption{\label{alg:half-compression} implication \gls{chain-compression} algorithm.}
|
|
\end{algorithm}
|
|
|
|
The algorithm can be further improved by considering implied conjunctions.
|
|
These can be split up into multiple implications.
|
|
|
|
\begin{mzn}
|
|
constraint b -> forall(x in N)(x)
|
|
\end{mzn}
|
|
|
|
The expression above is logically equivalent to the following expression.
|
|
|
|
\begin{mzn}
|
|
constraint forall(x in N)(b -> x)
|
|
\end{mzn}
|
|
|
|
Adopting this transformation both simplifies a complicated \constraint{} and possibly allows for the further compression of \glspl{implication-chain}.
|
|
It should be noted that, although this transformation can increase the number of \constraints{} in the \gls{slv-mod}, it generally increases the \gls{propagation} efficiency.
|
|
|
|
To adjust the algorithm to simplify implied conjunctions, more introspection from the \minizinc{} \compiler{} is required.
|
|
The \compiler{} must be able to tell if a \variable{} is (only) a \gls{cvar} of a reified conjunction and what the elements of that conjunction are.
|
|
In the case where a \variable{} has one incoming edge, but it is marked as used in another \constraint{}, we can now check if it is only a \gls{cvar} for a \gls{reified} conjunction and perform the transformation in this case.
|
|
|
|
\subsection{Common Sub-expression Elimination}%
|
|
\label{subsec:half-cse}
|
|
|
|
When using full \gls{reif}, all \glspl{reif} are stored in the \gls{cse} table.
|
|
This ensures that if the same expression is \gls{reified} twice, then the resulting \gls{cvar} will be reused.
|
|
This avoids that the solver has to enforce the same functional relation twice.
|
|
|
|
If the \gls{rewriting} uses \gls{half-reif}, in addition to full \gls{reif}, then \gls{cse} needs to ensure not just that the expressions are equivalent, but also that the context of the two expressions are compatible.
|
|
For example, if an expression was first found in a \posc{} context and later found in a \mixc{} context, then the resulting \gls{cvar} of the first \gls{half-reif} cannot be used for the second expression.
|
|
In general the following rules apply.
|
|
|
|
\begin{itemize}
|
|
|
|
\item The result of \gls{rewriting} an expression in \posc{} context, a \gls{half-reif}, can only be reused if the same expression is again found in \posc{} context.
|
|
|
|
\item The result of \gls{rewriting} an expression in \negc{} context, a \gls{half-reif} with its negation pushed inwards, can only be reused if the same expression is again found in \negc{} context.
|
|
|
|
\item The result of \gls{rewriting} an expression in \mixc{} context, a \gls{reif}, can be reused in \posc{}, \negc{}, and \mixc{} context.
|
|
Since we assume that the result of \gls{rewriting} an expression in \negc{} context pushes the negation inwards, the \gls{reif} does, however, need to be negated.
|
|
|
|
\item If the expression was already seen in \rootc{} context, then any repeated usage of the expression can be assumed to take the value \true{} (or \false{} in \negc{} context).
|
|
|
|
\end{itemize}
|
|
|
|
When considering these compatibility rules, the result of \gls{rewriting} is highly dependent on the order in which expressions are seen.
|
|
It would always be better to encounter the expression in a context that results in a reusable expression, e.g., \mixc{}, before seeing the same expression in another context, e.g., \posc{}.
|
|
This avoids creating both a full \gls{reif} and a \gls{half-reif} of the same expression.
|
|
|
|
In the \microzinc{} \interpreter{}, this problem is resolved by only keeping the result of their joint context.
|
|
The context recorded in the \gls{cse} table and the found context are joined using the join operator, as described in \cref{fig:half-join}.
|
|
If this context is different from the recorded context, then the expression is re-evaluated in the joint context and its result kept in the \gls{cse} table.
|
|
All usages of the previously recorded \gls{cvar} are replaced by the new result.
|
|
The dependency tracking, through the use of \constraints{} attached to \variables{}, ensures that all defining \constraints{} are removed from the model.
|
|
This ensures that all \variables{} and \constraints{} created for the earlier version are correctly removed.
|
|
|
|
\begin{example}
|
|
|
|
Consider, for example, the following \minizinc{} fragment, which uses the linearization of \mzninline{int_le}.
|
|
|
|
\begin{mzn}
|
|
predicate int_le_imp(var int: x, int: y, var bool: b) =
|
|
x <= ub(x) - (ub(x) - y) * b;
|
|
|
|
predicate int_le_reif(var int: x, int: y, var bool: b) =
|
|
x <= ub(x) - (ub(x) - y) * b /\ x >= (y + 1) - (y + 1) * b;
|
|
|
|
var 1..10: i;
|
|
constraint j \/ int_le(i, 4);
|
|
constraint k xor int_le(i, 4);
|
|
\end{mzn}
|
|
|
|
In this fragment the call \mzninline{int_le(i, 4)} occurs both in \posc{} and \mixc{} context.
|
|
Although, in this case, the \compiler{} is able to hoist the expression to share it between the two \constraint{}, as discussed in \cref{sec:rew-cse}, the same expressions might result from function \gls{rewriting} were this is not possible.
|
|
After \gls{rewriting} the first \constraint{}, the \nanozinc{} program would contain the following definitions.
|
|
|
|
\begin{nzn}
|
|
var bool: b1;
|
|
↳ constraint int_lin_le([1, 6], [i, b1], 10);
|
|
constraint bool_clause([j, b1], []);
|
|
\end{nzn}
|
|
|
|
In this program \mzninline{b1} is the \gls{cvar} of the \gls{half-reif} of the \mzninline{int_le(i, 4)} call.
|
|
The \gls{cvar} is added to the \gls{cse} table as the result of the call.
|
|
However, since the second call is in \mixc{} context, it cannot use the \gls{half-reif}, and must create the \gls{reif} instead.
|
|
This results in the following \nanozinc{} program.
|
|
|
|
\begin{nzn}
|
|
var bool: b1;
|
|
↳ constraint int_lin_le([1, 6], [i, b1], 10);
|
|
constraint bool_clause([j, b1], []);
|
|
var bool: b2;
|
|
↳ constraint int_lin_le([1, 6], [i, b2], 10);
|
|
↳ constraint int_lin_le([-1, -5], [i, b2], -5);
|
|
constraint bool_not(k, b2);
|
|
\end{nzn}
|
|
|
|
Now when \mzninline{b2} is added to the \gls{cse} table as the \gls{cvar} of the \gls{reif} of the \mzninline{int_le(i, 4)} call, it notices that there is already a result in table for the same call in a weaker context.
|
|
As such, it replaces all occurrences of the \gls{cvar} of the \gls{half-reif}, found in the table, with the \gls{cvar} of the \gls{reif}.
|
|
Once all usage of the \gls{cvar} have been removed, it and its dependent \constraints{} are removed, resulting in the following \nanozinc{} program.
|
|
|
|
\begin{nzn}
|
|
constraint bool_clause([j, b2], []);
|
|
var bool: b2;
|
|
↳ constraint int_lin_le([1, 6], [i, b2], 10);
|
|
↳ constraint int_lin_le([-1, -5], [i, b2], -5);
|
|
constraint bool_not(k, b2);
|
|
\end{nzn}
|
|
\end{example}
|
|
|
|
Because the expression itself is changed when a negation is moved inwards, it may not always be clear when the same expression is used in both \posc{} and \negc{} context.
|
|
This problem is solved by introducing a canonical form for expressions where negations can be pushed inwards.
|
|
In this form the result of \gls{rewriting} an expression and its negation are collected in the same place within the \gls{cse} table.
|
|
If it is found that for an expression that is about to be \gls{half-reified} there already exists a \gls{half-reif} for its negation, then we instead evaluate the expression in \mixc{} context.
|
|
The expression is \gls{reified} and replaces the existing \gls{half-reified} expression.
|
|
|
|
\begin{example}
|
|
Consider for example the \mzninline{=} operator on integers, which \microzinc{} represents as an \mzninline{int_eq} call.
|
|
When its expression is negated, pushing the negation inwards will result in a \mzninline{!=} operator, a \mzninline{int_ne} call.
|
|
The opposite happens when a negation is pushed inwards for an expression using \mzninline{!=} operator.
|
|
So to ensure that a \negc{} occurrence of \mzninline{int_eq} and a \posc{} occurrence of \mzninline{int_ne} use the same \gls{cvar} they are both mapped to \mzninline{int_eq} in the \gls{cse} table.
|
|
The mapping ensures that the context is correctly transformed when accessing the \gls{cse} table for an \mzninline{int_ne} call.
|
|
\end{example}
|
|
|
|
This canonical form for expressions and their negations can also be used for the expressions in other contexts.
|
|
Using the canonical form we can now also be sure that we never create a full \gls{reif} for both an expression and its negation.
|
|
Instead, when one is created, the negation of the resulting \variable{} can directly be used as the \gls{reif} of its negation.
|
|
Moreover, this mechanism also allows us to detect when an expression and its negation occur in \rootc{} context.
|
|
Since a \constraint{} and its negation cannot both hold at the same time, this is a simple way to detect that the \cmodel{} is \gls{unsat}.
|
|
|
|
\subsection{Dynamic Context Switching}%
|
|
\label{subsec:half-dyn-context}
|
|
|
|
In \cref{subsec:half-?root} we discussed the fact that the correct context of an expression is not always known when analysing \microzinc{}.
|
|
The context may depend on data that is only known at an \instance{} level.
|
|
The same situation can be caused by \gls{propagation}.
|
|
|
|
\begin{example}
|
|
Consider the following \minizinc{} fragment
|
|
|
|
\begin{mzn}
|
|
var 1..4: x;
|
|
var 5..10: y;
|
|
var bool: b = x < y;
|
|
constraint b -> (2*x = y);
|
|
\end{mzn}
|
|
|
|
Since the values in the \domain{} of \mzninline{x} are strictly smaller than the values in the \domain{} of \mzninline{y}, \gls{propagation} of \mzninline{b} will set it to the value \true{}.
|
|
This however means that the \constraint{} is equivalent to the following \constraint{}.
|
|
|
|
\begin{mzn}
|
|
constraint 2*x = y;
|
|
\end{mzn}
|
|
|
|
The linear \constraint{} could be evaluated in \rootc{} context, instead of the \posc{} context that is detected by our context analysis.
|
|
|
|
\end{example}
|
|
|
|
The situation shown in the example is the most common change of context.
|
|
If the \gls{cvar} of a \gls{reif} is fixed, the context changes to either \rootc{} or a negated \rootc{} context.
|
|
If, on the other hand, the \gls{cvar} of a \gls{half-reif} is fixed, then either the context becomes \rootc{} or the \constraint{} is trivially \gls{satisfied}.
|
|
Since direct \constraints{} are strongly preferred over any form of \gls{reif}, it is important to dynamically pick the correct form during the \gls{rewriting} process.
|
|
|
|
This problem can be solved by the \compiler{}.
|
|
For each \gls{reif} and \gls{half-reif} the \compiler{} introduces a layer of indirection.
|
|
In this layer, it checks the \gls{cvar}.
|
|
If the \gls{cvar} is already fixed, then it rewrites itself into the corresponding form in another context.
|
|
Otherwise, it behaves as it would have done normally.
|
|
The \gls{cvar} is thus used to communicate the change in context.
|
|
|
|
\begin{example}
|
|
Let's assume the \compiler{} finds a call to \mzninline{int_eq} in \posc{} context.
|
|
Instead of outputting the call to \mzninline{int_eq_imp} directly, it will instead output a call to \mzninline{int_eq_imp_check}.
|
|
This predicate is then generated as shown in \cref{lst:half-check-reif}.
|
|
The \gls{rewriting} of the calls to the generated predicate then follow the normal process.
|
|
\end{example}
|
|
\begin{listing}
|
|
\mznfile{assets/listing/half_reif_check.mzn}
|
|
\caption{\label{lst:half-check-reif}A generated predicate for \mzninline{int_eq_imp} that checks the \gls{cvar} to ensure a \gls{half-reif} is still required.}
|
|
\end{listing}
|
|
|
|
|
|
\section{Experiments}
|
|
\label{sec:half-experiments}
|
|
|
|
We now present an experimental evaluation of the presented techniques.
|
|
First, to show the benefit of implementing \glspl{propagator} for \gls{half-reified} \constraints{} by comparing their performance against their \glspl{decomp}.
|
|
We recreate two experiments presented by \textcite{feydy-2011-half-reif} in the original \gls{half-reif} paper in a modern \gls{cp} solver, \gls{chuffed}.
|
|
We adapt the \glspl{propagator} for the non-\gls{reified} \constraints{} to take into account the \gls{cvar}, by reusing the code for checking and pruning as described in \cref{sec:half-propagation}.
|
|
|
|
Additionally, we assess the effects of automatically detecting and introducing \glspl{half-reif} during the \gls{rewriting} process.
|
|
We rewrite and solve 200 \minizinc{} \instances{} for several \solvers{} with and without the use of \gls{half-reif}.
|
|
We then analyse the trends in the generated \glspl{slv-mod} and their solving performance.
|
|
|
|
A description of the used computational environment, \minizinc{} instances, and versioned software has been included in \cref{ch:benchmarks}.
|
|
|
|
\subsection{Half-Reified Propagators}
|
|
\label{sec:half-exp-prop}
|
|
|
|
Our first experiment considers the QCP-max quasi-group completion problem.
|
|
In this problem, we need to decide the value of a \((n \times n)\) matrix of integer \variables{}, with \domains{} \mzninline{1..n}.
|
|
The aim of the problem is to create as many rows and columns as possible where all \variables{} take a unique value.
|
|
In each \instance{} certain values have already been fixed.
|
|
It is not always possible for all rows and columns to contain only distinct values.
|
|
|
|
In \minizinc{} counting the number of rows/columns with all different values can be accomplished using a \gls{reified} \mzninline{all_different} \constraint{}.
|
|
Since the goal of the problem is to maximize the number of \mzninline{all_different} \constraints{} that hold, these \constraints{} are never forced to be \false{}.
|
|
This means these \constraints{} are in \posc{} context and can be \gls{half-reified}.
|
|
|
|
\Cref{tab:half-qcp} shows the comparison of two solving configurations in \gls{chuffed} for the QCP-max problem.
|
|
The results are grouped based on their size of the instance.
|
|
For each group we show the number of instances solved by the configuration and the average time used for this process.
|
|
|
|
In our first configuration the half-reified \mzninline{all_different} \constraint{} is enforced using a \gls{propagator}.
|
|
This \gls{propagator} is an adjusted version from the existing \gls{boundsz-con} \mzninline{all_different} \gls{propagator} in \gls{chuffed}.
|
|
The implementation of the \gls{propagator} was already split into parts that check the violation of the \constraint{} and parts that prune the \glspl{domain} of the \variables{}.
|
|
Therefore, the transformation described in \cref{sec:half-propagation} can be directly applied.
|
|
Since \gls{chuffed} is a \gls{lcg} \solver{}, the explanations created by the \gls{propagator} have to be adjusted as well.
|
|
These adjustments happen similar to the adjustments of the general algorithm: explanations used for the violation\glsadd{violated} of the \constraint{} can now be used to set the \gls{cvar} to \false{}, and the explanations given to prune a \variable{} are extended with a literal that ensures the \gls{cvar} is \true{}.
|
|
|
|
In our second configuration the \mzninline{all_different} \constraint{} is enforced using the \gls{decomp} shown in \cref{lst:half-alldiff}.
|
|
The \mzninline{!=} \constraints{} produced by this redefinition are \gls{reified}.
|
|
Their conjunction then represent the \gls{reif} of the \mzninline{all_different} \constraint{}.
|
|
|
|
\begin{listing}
|
|
\mznfile{assets/listing/half_alldiff.mzn}
|
|
\caption{\label{lst:half-alldiff}The standard \gls{decomp} for \mzninline{all_different} in the \minizinc{} library.}
|
|
\end{listing}
|
|
|
|
|
|
\begin{table}
|
|
\begin{center}
|
|
\input{assets/table/half_qcp}
|
|
|
|
\caption{\label{tab:half-qcp} QCP-max problems: number of solved \instances{} and average time (in seconds) with a 300s timeout.}
|
|
|
|
\end{center}
|
|
\end{table}
|
|
|
|
The results in \cref{tab:half-qcp} show that the specialized \gls{propagator} has a significant advantage over the use of the \gls{decomp}.
|
|
Although it only allows us to solve one extra instance, there is a significant reduction in solving time for most \instances{}.
|
|
Note that the qcp-15 \instances{} are the only exception.
|
|
It appears that none of the \instances{} in this group proved to be a real challenge to either method, and we see similar solve times between the two methods.
|
|
|
|
In addition, we consider a variation on the prize collecting travelling salesman problem \autocite{balas-1989-pctsp} referred to as the ``prize collecting path'' problem.
|
|
In the problem we are given a graph with weighted edges, both positive and negative.
|
|
The aim of the problem is to find the optimal acyclic path from a given start node that maximizes the weights on the path.
|
|
It is not required to visit every node.
|
|
|
|
In this experiment we can show how \gls{half-reif} can reduce the overhead of handling partial functions correctly.
|
|
The \minizinc{} model for this problem contains an \gls{array} lookup \mzninline{pos[next[i]]}, where the \domain{} of \mzninline{next[i]} is larger than the index set of \mzninline{pos}.
|
|
We compare safe \gls{decomp} of this \mzninline{element} \constraint{} against a \gls{propagator} of its \gls{half-reif}.
|
|
The \gls{decomp} creates a new \variable{} that takes the value of the index only when it is within the index set of the \gls{array}.
|
|
Otherwise, it will set its surrounding context to \false{}.
|
|
The \gls{half-reif} implicitly performs the same task by setting its \gls{cvar} to \false{} whenever the resulting \variable{} does not equal the element to which the index \variable{} points, or when the index points outside the \gls{array}.
|
|
Again, for the implementation of the \gls{propagator} of the \gls{half-reif} \constraint{} we adjust the direct \gls{propagator} as described above.
|
|
|
|
\begin{table}
|
|
\begin{center}
|
|
|
|
\input{assets/table/half_prize}
|
|
|
|
\caption{\label{tab:half-prize} Prize collecting paths: number of solved \instances{} and average time (in seconds) and with a 300s timeout.}
|
|
\end{center}
|
|
\end{table}
|
|
|
|
The results of the experiment are shown in \cref{tab:half-prize}.
|
|
Although the performance on smaller \instances{} is similar, the dedicated \gls{propagator} consistently outperforms the \gls{decomp}.
|
|
The difference in performance becomes more pronounced in the larger \instances{}.
|
|
In the 32-4-8 group, we even see that usage of the \gls{propagator} allows us to solve an additional three \instances{}.
|
|
|
|
\subsection{Rewriting with Half-Reification}
|
|
\label{sec:half-exp-rewriting}
|
|
|
|
The usage of context analysis and introduction of \glspl{half-reif} allows us to evaluate \gls{half-reif} on a larger scale.
|
|
In our second experiment we assess its effects on the \gls{rewriting} and solving of the \instances{} of the 2019 and 2020 \minizinc{} challenge \autocite{stuckey-2010-challenge,stuckey-2014-challenge}.
|
|
These experiments are conducted using the \gls{gecode} \solver{}, which have \glspl{propagator} for \glspl{half-reif} of many basic \constraints{}, and \minizinc{}'s \gls{linearization} and \gls{booleanization} libraries, which has been adapted to use \gls{half-reif} as earlier described.
|
|
The \minizinc{} instances are rewritten using the \minizinc{} 2.5.5 \compiler{}, which can enable and disable \gls{half-reif}.
|
|
The solving of the linearized \instances{} are tested using the \gls{cbc} and \gls{cplex} \gls{mip} \solvers{}.
|
|
The solving of the Booleanized \instances{} are testing using the \gls{openwbo} \solver{}.
|
|
|
|
\begin{table}
|
|
\begin{subtable}[b]{\linewidth}
|
|
\input{assets/table/half_flat_gecode}
|
|
\caption{\label{subtab:half-flat-gecode}\gls{gecode} library}
|
|
\end{subtable}
|
|
\begin{subtable}[b]{\linewidth}
|
|
\input{assets/table/half_flat_linear}
|
|
\caption{\label{subtab:half-flat-lin}\Gls{linearization} library}
|
|
\end{subtable}
|
|
\begin{subtable}[b]{\linewidth}
|
|
\input{assets/table/half_flat_sat}
|
|
\caption{\label{subtab:half-flat-bool}\Gls{booleanization} library}
|
|
\end{subtable}
|
|
\caption{\label{tab:half-rewrite} Cumulative statistics of \gls{rewriting} all \minizinc{} \instances{} from \minizinc{} challenge 2019 \& 2020 (200 \instances{}).}
|
|
\end{table}
|
|
|
|
Grouped by \solver{} library and whether \gls{half-reif} is used, \cref{tab:half-rewrite} shows the following cumulative figures from the \gls{rewriting} process of the \minizinc{} challenge.
|
|
|
|
\begin{itemize}
|
|
|
|
\item The number of \constraints{} in \flatzinc{}.
|
|
\item The number of \glspl{reif} evaluated during the \gls{rewriting} process.
|
|
This includes both the \glspl{reif} that are decomposed and the \glspl{reif} that are present in the \flatzinc{}.
|
|
\item The number of \glspl{half-reif} evaluated during the \gls{rewriting} process.
|
|
\item The number of implications removed using the \gls{chain-compression} method.
|
|
\item The runtime of the \gls{rewriting} process.
|
|
|
|
\end{itemize}
|
|
|
|
The \gls{rewriting} statistics for the \gls{gecode} \solver{} library, shown in \cref{subtab:half-flat-gecode}, show significant changes in the resulting \flatzinc{}.
|
|
Although the total number of \constraints{} remains stable, we see that well over half of all \glspl{reif} are replaced by \glspl{half-reif}.
|
|
This replacement happens mostly 1-for-1; the difference between the number of \glspl{half-reif} introduced and the number of \glspl{reif} reduced is only 20. In comparison, the number of implications removed by \gls{chain-compression} looks small, but this number is highly dependent on the \minizinc{} model.
|
|
In many models \gls{chain-compression} does not remove any implications, but in some models an implication is removed for every \gls{half-reif} that is introduced.
|
|
Finally, the overhead of the introduction of \gls{half-reif} and the newly introduced optimization techniques is minimal.
|
|
|
|
The \Cref{subtab:half-flat-lin} paints an equally positive picture of \glspl{half-reif} for linearization.
|
|
Since both \glspl{reif} and \glspl{half-reif} are decomposed during the \gls{rewriting} process, \gls{half-reif} is able to remove almost 7.5\% of the overall \constraints{}.
|
|
The ratio of \glspl{reif} that is replaced with \glspl{half-reif} is not as high as with \gls{gecode}.
|
|
This is caused by the fact that the linearization process requires full \gls{reif} in the decomposition of many \glspl{global}.
|
|
Similar to \gls{gecode}, the number of implications that is removed is dependent on the problem.
|
|
Lastly, the \gls{rewriting} time slightly increases for the linearization process.
|
|
Since there are many more \constraints{}, the introduced optimization mechanisms have a slightly higher overhead.
|
|
|
|
Finally, statistics for \gls{rewriting} the \instances{} for a \gls{maxsat} \solver{} are shown in \cref{subtab:half-flat-bool}.
|
|
Unlike linearization, \gls{half-reif} does not significantly reduce the number of \constraints{} and, although still significant, the number of \glspl{reif} is reduced by only slightly over ten percent.
|
|
We also see that the \gls{booleanization} library is explicitly defined in terms of \glspl{half-reif}.
|
|
Some \constraints{} manually introduce \mzninline{_imp} call as part of their definition.
|
|
Even when we do not automatically introduce \glspl{half-reif}, they are still introduced by other \constraints{}.
|
|
Furthermore, \gls{chain-compression} does not seem to have any effect.
|
|
Since all \glspl{half-reif} are defined in terms of clauses, the implications normally removed using \gls{chain-compression} are instead aggregated into larger clauses.
|
|
Surprisingly, \gls{half-reif} slightly reduces the \gls{rewriting} time as it reduces the workload.
|
|
The relatively small changes shown might indicate that additional work might be warranted in the \gls{booleanization} library.
|
|
It might be possible to create more dedicated \glspl{decomp} for \gls{half-reified} \constraints{}, and to analyse the library to see if \glspl{annotation} could be added to more function arguments to retain \posc{} contexts.
|
|
|
|
\begin{table}
|
|
\input{assets/table/half_mznc}
|
|
\caption{\label{tab:half-mznc} Status overview of solving \minizinc{} Challenge 2019 \& 2020 with and without \gls{half-reif}.}
|
|
\end{table}
|
|
|
|
\Cref{tab:half-mznc} shows the results reported by the solvers. The \solver{} reports
|
|
|
|
\begin{description}
|
|
\item[Unsatisfiable] when it proves the \instance{} does not have a \gls{sol},
|
|
\item[Optimal solution] when it has found a \gls{sol} and has proven the \gls{sol} to be optimal,
|
|
\item[Satisfied] when it has found a \gls{sol} for the problem,
|
|
\item[Unknown] when it does not find a \gls{sol} is found within the time limit, and
|
|
\item[Error] when the \solver{} program crashes.
|
|
\end{description}
|
|
|
|
\noindent{}For \solver{} statuses that end the solving process before the time-out of 15 minutes we also show the average time.
|
|
|
|
The results shown in this table are very mixed.
|
|
For \gls{gecode}, \gls{half-reif} does not seem to impact its solving performance.
|
|
We would have hoped that \glspl{propagator} for \glspl{half-reif} would be more efficient and reduce the number of \glspl{propagator} scheduled in general.
|
|
However, neither number of \instances{} solved, nor the required solving time improved.
|
|
A single \instance{}, however, is negatively impacted by the change; for this \instance{} it cannot find an \gls{opt-sol} any longer.
|
|
We expect that this \instance{} has benefited from the increased Boolean \gls{propagation} that is caused by full \gls{reif}.
|
|
Overall, these results do not show any significant positive or negative effects in \gls{gecode}'s performance when using \gls{half-reif}.
|
|
|
|
When using \gls{cplex}, \gls{half-reif} clearly has a positive effect.
|
|
Although it does not prove the unsatisfiability of one instance any longer and slightly increases the number of solver errors, an \gls{opt-sol} is found for five more instances.
|
|
The same linearized instances when using the \gls{cbc} solver seem to have the opposite effect.
|
|
Even though it reduces the time required to prove that two instances are \gls{unsat}, it cannot find six \glspl{opt-sol} any longer.
|
|
These results are hard to explain.
|
|
In general, we would expect the reduction of \constraints{} in a \gls{mip} instance would help the \gls{mip} solver.
|
|
However, we can imagine that the removed \constraints{} in some cases help the \gls{mip} solver.
|
|
An important technique used by \gls{mip} solvers is to detect certain patterns, such as cliques, during the pre-processing of the \gls{mip} instance.
|
|
Some patterns can only be detected when using full \gls{reif}.
|
|
Furthermore, the performance of \gls{mip} solvers is often dependent on the order and form in which the \constraints{} are given \autocite{lodi-2013-variability,fischetti-2014-erratiscism}.
|
|
When using \gls{half-reif} in addition to \gls{aggregation} and \gls{del-rew}, the order and form of the \gls{slv-mod} can be exceedingly different.
|
|
|
|
The solving statistics for \gls{openwbo} might be most positive.
|
|
Through the use of \gls{half-reif}, \gls{openwbo} is able to find and prove the \gls{opt-sol} for 3 more \instances{}.
|
|
It negatively impacts one \instance{}, for which find a \gls{sol} is not found any more.
|
|
That the effect is so positive is surprising since its \gls{rewriting} statistics for \gls{maxsat} showed the least amount of change.
|
|
|
|
% \section{Summary}
|
|
% \label{sec:half-summary}
|