diff --git a/assets/glossary.tex b/assets/glossary.tex index d9fd952..ca19f3b 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -321,6 +321,11 @@ description={}, } +\newglossaryentry{unify}{ + name={unify}, + description={}, +} + \newglossaryentry{variable}{ name={decision variable}, description={}, diff --git a/chapters/2_background.tex b/chapters/2_background.tex index ae0497c..2676fe1 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -1568,10 +1568,12 @@ the utmost importance. A \flatzinc\ containing extra \glspl{variable} and \glspl{constraint} that do not add any information to the solving process might exponentially slow down the solving process. Therefore, the \minizinc\ flattening process is extended using many techniques to help improve the quality -of the flattened model. In the remainder of this section we will discuss the -most important techniques utilised in the flattener. +of the flattened model. In \crefrange{subsec:back-cse}{subsec:back-delayed-rew} +we will discuss the most important techniques used to improved the flattening +process. -\paragraph{Common Sub-expression Elimination} +\subsection{Common Sub-expression Elimination}% +\label{subsec:back-cse} Because the evaluation of a \minizinc\ expression cannot have any side-effects, it is possible to reuse the same result for equivalent expressions. This @@ -1670,7 +1672,8 @@ constraint. set \mzninline{b0} to \mzninline{true}. \end{example} -\paragraph{Adjusting domains} +\subsection{Adjusting Domain}% +\label{subsec:back-adjusting-dom} As discussed in \cref{subsec:back-cp}, the \glspl{domain} of \glspl{variable} can sometimes be directly changed because of the addition of a \gls{constraint}. @@ -1718,7 +1721,8 @@ constraints that directly change the domain (\eg\ \mzninline{x in 3..5}). It, however, will not perform more complex \gls{propagation}, like the \gls{propagation} of \glspl{global}. -\paragraph{Constraint Aggregation} +\subsection{Constraint Aggregation}% +\label{subsec:back-aggregation} Complex \minizinc\ expression can sometimes result in the creation of many new variables that represent intermediate results. This is in particular true for @@ -1766,7 +1770,8 @@ expressions to form an aggregated constraint. The flattening process continues by flattening this aggregated constraint, which might still contain unflattened arguments. -\paragraph{Delayed Rewriting} +\subsection{Delayed Rewriting}% +\label{subsec:back-delayed-rew} Adjusting the \glspl{domain} of variables during flattening means that the system becomes non-confluent, and some orders of execution may produce @@ -1818,7 +1823,27 @@ Note that this heuristic does not guarantee that \glspl{variable} have their tightest possible \gls{domain}. One delayed \gls{constraint} can still influence the \glspl{domain} of \glspl{variable} used by other delayed \glspl{constraint}. -\subsection{Optimisation}% +\subsection{FlatZinc Optimisation}% \label{subsec:back-fzn-optimisation} -The optimisation process of the \minizinc\ compiler +After the compiler is done flattening the \minizinc\ instance, it enters the +optimisation phase. This phase occurs at the same stage as the as the solver +input language. Depending on the targeted \gls{solver}, the \minizinc\ flattener +might still understand the meaning of certain constraints. In these cases, +\gls{propagation} methods (as discussed in \cref{subsec:back-cp}) can be used to +eliminate values from variable \glspl{domain} and simplify \glspl{constraint}. + +In the current implementation the main focus of the flattener is to propagate +Boolean constraint. The flattener try and reduce the number of Boolean variables +and try and reduce the number of literals in clauses or logical and constraints. +The additional propagation might fix the reification of a constraint. If this +constraint is not yet rewritten, then the \gls{solver} will know to use a direct +constraint instead of a reified version. + +Even more important than the Boolean constraints, are equality +\glspl{constraint}. The flattening is in the unique position to \gls{unify} +\glspl{variable} when they are found to be equal. Since they both have to take +the same value, only a single \gls{variable} is required in the \flatzinc\ model +to represent them both. Whenever any (recognisable) equality constraint is found +during the optimisation phase, it is removed and the two \glspl{variable} are +unified.