diff --git a/chapters/2_background.tex b/chapters/2_background.tex index 4f752ae..c760f8b 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -1462,7 +1462,39 @@ Finally, it can also be helpful for \solvers{} as they may need to decide on a r During \gls{rewriting}, the \minizinc{} compiler actively removes values from the \domain{} when it encounters \constraints{} that trivially reduce it. For example, it detects \constraints{} with a single comparison expression between a \variable{} and a \parameter{} (\eg\ \mzninline{x != 5}), \constraints{} with a single comparison between two \variables{} (\eg\ \mzninline{x >= y}), \constraints{} that directly change the domain (\eg\ \mzninline{x in 3..5}). -It, however, does not perform more complex \gls{propagation}, like the \gls{propagation} of \glspl{global}. +It even performs more complex \gls{propagation} for some known \constraints{}. +For example, it will reduce the \domains{} for \mzninline{int_times} and \mzninline{int_div} and we will see in the next subsection how \gls{aggregation} will help simplify certain \constraint{}. + +However, \gls{propagation} is only performed locally, when the \constraint{} is recognised. +During \gls{rewriting}, the \gls{propagation} of one \constraint{}, will not trigger the \gls{propagation} of another. + +Crucially, the \minizinc{} compiler also handles equality \constraints{}. +During the \gls{rewriting} process we are in a unique position to perform effective equality \gls{propagation}. +If the \compiler{} finds that two \variables{} \mzninline{x} and \mzninline{y} are equal, then only a single \variable{} is required in the \gls{slv-mod} to represent them both. +Whenever any equality \constraint{} is found, it is removed and one of the \variables{} is replaced by the other. + +This is often beneficial for the \solver{}, since it reduced the number of \variables{} and some \solver{} are not able to perform this replacement, forcing the propagation of an equality \constraint{}. +Moreover, replacing one variable for another can improve the effectiveness of \gls{cse}. + +\begin{example} + Consider the following \minizinc{} fragment. + + \begin{mzn} + var 1..5: a; + var 1..5: b; + + constraint a = b; + constraint this(a); + constraint this(b); + \end{mzn} + + The equality \constraint{}, replaces the \variable{} \mzninline{b} with the \variable{} \mzninline{a}. + Now the two calls to \mzninline{this} suddenly become equivalent and the second will be found in the \gls{cse} table. +\end{example} + +Note that if the equality \constraint{} in the example would have be found after both calls, then both calls would have already been rewritten. +The \minizinc{} compiler would be unable to revisit the rewriting of second calls after the equality is found. +It is therefore important that equalities are found early in the \gls{rewriting} process. \subsection{Constraint Aggregation}% \label{subsec:back-aggregation} @@ -1549,26 +1581,19 @@ Although the Boolean \gls{avar} can be used in the aggregated \constraints{}, we If the body of the \gls{reif} was defined in terms of Boolean logic, then it would have been aggregated as well. However, since the rewriting of the body was delayed and the \compiler{} does not revisit \gls{aggregation}, this does not happen. -A possible solution to this problem, is for the modeller to activate \minizinc{}'s multi-pass compilation \autocite{leo-2015-multipass}. -When activate it compiles (and propagates) an \instance{} multiple times, remembering information about the earlier iteration. -As such, information normally discovered later in the \gls{rewriting} process, such as the final \domains{} of \variables and whether an expressions must be \gls{reified}, can be used from the start. +This problem can be solved through the use of \minizinc{}'s multi-pass compilation \autocite{leo-2015-multipass}. +It can rewrite (and propagate) an \instance{} multiple times, remembering information about the earlier iteration(s). +As such, information normally discovered later in the \gls{rewriting} process, such as the final \domains{} of \variables{}, whether two \variables{} are equal, and whether an expressions must be \gls{reified}, can be used from the start. \subsection{FlatZinc Optimisation}% \label{subsec:back-fzn-optimisation} After the \compiler{} has finished \gls{rewriting} the \minizinc{} instance, it enters the optimisation phase. -This phase operates at the level of the \gls{slv-mod}, where all \constraints{} are now \gls{native} \constraints{} of the target \solver{}. +The primary role of this phase is to further perform \gls{propagation} until \gls{fixpoint}. +However, this phase operates at the level of the \gls{slv-mod}, where all \constraints{} are now \gls{native} \constraints{} of the target \solver{}. This means that, depending on the target \solver{}, the \compiler{} will not be able to understand the meaning of all \constraints{}. -It only understand the meaning of the standard \flatzinc{} \constraints{}, but not any of the \solver{} specific \gls{native} \constraints{}. -For the standard \flatzinc{} \constraints{}, \gls{propagation} methods, as discussed in \cref{subsec:back-cp}, are used to eliminate values from \domains{} and simplify \constraints{}. +It only understands the meaning of the standard \flatzinc{} \constraints{}, but not any of the \solver{} specific \gls{native} \constraints{}. +For the standard \flatzinc{} \constraints{}, it employs \gls{propagation} methods, as discussed in \cref{subsec:back-cp}, are used to eliminate values from \domains{} and simplify \constraints{}. -In the current implementation the main focus of the \compiler{} is to propagate Boolean \constraints{}. -The \compiler{} tries to reduce the number of Boolean \variables{} and tries to reduce the number of literals in clauses and conjunctions. -The additional \gls{propagation} can fix the result of the \gls{reif} of a \constraint{}. -If the \gls{reif} was a \gls{native} \constraint, then the \solver{} can still use a direct \constraint{} instead of a \gls{reified} version. - -Even more important than the Boolean \constraints{}, are equality \constraints{}. -During the \gls{rewriting} process we are in a unique position to perform effective equality propagation. -If the \compiler{} finds that two \variables{} \mzninline{x} and \mzninline{y} are equal, then only a single \variable{} is required in the \gls{slv-mod} to represent them both. -Whenever any equality \constraint{} is found during the optimisation phase, it is removed and one of the \variables{} is replaced by the other. -Once initialised, it is generally not possible for \solvers{} to perform this replacement internally. +In the current implementation, the \minizinc{} \compiler{} propagate mostly Boolean \constraints{} in this phase. +It tries to reduce the number of Boolean \variables{} and tries to reduce the number of literals in clauses and conjunctions.