Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Work on the Optimisation Phase text

Browse Source
This commit is contained in:
Jip J. Dekker 2021-05-18 20:04:39 +10:00
parent b3a497f71d
commit 1fe8190c14
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
2 changed files with 38 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
assets/glossary.tex
View File

@ -321,6 +321,11 @@
description={},
}
\newglossaryentry{unify}{
name={unify},
description={},
}
\newglossaryentry{variable}{
name={decision variable},
description={},

41
chapters/2_background.tex
View File

@ -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.