25 lines
2.7 KiB
TeX
25 lines
2.7 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, using a \gls{reif} \(b \leftrightarrow{} c\), that determines whether a \constraint{} \(c\) holds, can slow the \solver{} down.
|
|
Even in \gls{cp} \solvers{}, not many \glspl{reif} are \gls{native} to the \solvers{}, and the \glspl{propagator}, for the ones that are, are often weak.
|
|
Generally, the \glspl{decomp} of \gls{reified} \constraint{} also result numerous \gls{native} \constraints{} and \variables{}.
|
|
It is 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 minimize 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} \(b \rightarrow{} c\) for a \constraint{} \(c\) was introduced by \textcite{feydy-2011-half-reif}.
|
|
It is shown \gls{half-reif} can mitigate some 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 generalize to the full \minizinc{} language.
|
|
This chapter re-evaluates \gls{half-reif} and extends the \gls{rewriting} process to fully support \gls{half-reif} in \minizinc{}.
|
|
|
|
This chapter is organized 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 using \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}.
|