24 lines
2.6 KiB
TeX
24 lines
2.6 KiB
TeX
\noindent{}Whether a \constraint{} has to be \gls{reified} is a crucial decision made during \gls{rewriting}.
|
|
\minizinc{} allows us to write complex \constraints{} that in the process of \gls{rewriting} result in multiple \constraints{} that reason about each other.
|
|
However, determining whether a \constraint{} holds, \(\texttt{b} \leftrightarrow{} c\), requires significantly more effort from the \solver{} than merely enforcing the constraint \(c\).
|
|
A \gls{reified} \constraint{} results in a larger \gls{decomp} or a more complex \gls{native} \constraint{}.
|
|
It it thus important that \gls{rewriting} avoids the use of \gls{reif}, whenever it is not required.
|
|
|
|
In this chapter we present an extended \gls{reif} analysis to help minimise the required \solver{} effort.
|
|
Not only does it consider if a \constraint{} must be \gls{reified} or not, but it also considers whether it could instead be \gls{half-reified}.
|
|
|
|
The notion of \gls{half-reif} \(\texttt{b} \rightarrow{} c\) for a \constraint{} \(c\) was introduced by \textcite{feydy-2011-half-reif}.
|
|
It is shown \gls{half-reif} can relief some of the problems and expenses of the use of \gls{reif}.
|
|
It is not always possible, however, to use a \gls{half-reif} instead of a \gls{reif}.
|
|
The authors identify the conditions required for its usage and provide an algorithm that rewrites a subset of the \minizinc{} language using the technique.
|
|
Crucially, because of the omission of \gls{let} and multiple occurrences of identifiers, this algorithm does not directly generalise to the full \minizinc{} language.
|
|
This chapter re-evaluates the usage of \gls{half-reif} and extends the \gls{rewriting} process to fully support \gls{half-reif} in \minizinc{}.
|
|
|
|
This chapter is organised as follows.
|
|
In \cref{sec:half-intro,sec:half-propagation} we introduce the core concepts of \gls{half-reif} and \glspl{propagator} for \gls{half-reified} \constraints{}, as discussed by \textcite{feydy-2011-half-reif}.
|
|
An additional benefit of \gls{half-reif} is that its \gls{decomp} can be significantly smaller than the \gls{decomp} of a \gls{reif}.
|
|
\Cref{sec:half-decomposition} shows the benefits of \gls{half-reif} when writing \glspl{decomp} for \gls{mip} and \gls{sat} \solvers{}.
|
|
In \cref{sec:half-context} we introduce our new context analysis algorithm: a way to determine where \gls{half-reif} can be used in \microzinc{}, and by extension \minizinc{}.
|
|
Then, in \cref{sec:half-rewriting}, we elaborate on how the usage of \gls{half-reif} changes the \gls{rewriting} process.
|
|
Finally, the effects of \glspl{propagator} for \gls{half-reified} \constraints{} and the automatic introduction of \gls{half-reif} is analysed in \cref{sec:half-experiments}.
|