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

Final (non-essence) feedback from Guido

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-23 11:47:47 +10:00
parent 2c3bd8bef9
commit a267db1e81
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
1 changed files with 42 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

59
chapters/2_background.tex
View File

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