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

Notes from Peter

Browse Source
This commit is contained in:
Jip J. Dekker 2021-06-25 14:33:03 +10:00
parent 63dd1bed74
commit cb82213d85
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
2 changed files with 36 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

64
chapters/3_rewriting.tex
View File

@ -92,7 +92,7 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
In contrast to \minizinc{}, the evaluation of \microzinc\ will implement strict semantics for partial expressions, whereas \minizinc\ uses relational semantics.
Stuckey and Tack have extensively examined these problems and describe how to transform any partial function into a total function.
\autocite*{stuckey-2013-functions}.
A general approach for describing the partially in \microzinc\ functions is to make the function return both a boolean variable that indicates the totality of the input variables and the resulting value of the function that is adjusted that is adjusted to return a predefined value when it would normally be undefined.
A general approach for describing the partially in \microzinc\ functions is to make the function return both a Boolean variable that indicates the totality with regards to the input variables and the resulting value of the function that is adjusted to return a predefined value when it would normally be undefined.
For example, The function
\begin{mzn}
@ -105,15 +105,21 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
\begin{mzn}
function tuple(var int, var bool): element_safe(array of int: a, var int: x) =
let {
var bool: total = x in index_set(x);
var index_set(a): xs;
constraint total -> x = xs; % Give xs the value of x when result is total
var res = element(a, xs); % Use of element that is guaranteed to be total
set of int: idx = index_set(x)
var bool: total = x in idx;
var idx: xs;
int: m = min(idx);
% Give xs the value of x when result is total
constraint total -> xs = x;
% Otherwise, give xs the value m instead.
constraint not total -> xs = m;
% element constraint that is guaranteed to be total
var res = element(a, xs);
tuple(var int, var bool): ret = (res, total);
} in ret;
\end{mzn}
Similar to the replacement of optional values, all usage of the \mzninline{element} function are replaced by \mzninline{element_safe} and the usage of its result should be guarded by the returned totality variable in the surrounding boolean context.
Similar to the replacement of optional values, all usage of the \mzninline{element} function are replaced by \mzninline{element_safe} and the usage of its result should be guarded by the returned totality variable in the surrounding Boolean context.
This means that, for example, the expression \mzninline{element(e, v) = 5 \/ b} would be transformed into:
\begin{mzn}
@ -134,9 +140,9 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
function f_int(int: x) = /* original body */;
function f_varint(varint: x) =
if is_fixed(x) then
f_int(x)
f_int(x)
else
/* original body */;
/* original body */;
endif;
\end{mzn}
@ -840,27 +846,27 @@ These are very encouraging results, given that we are comparing a largely unopti
\end{figure}
\section{Summary}%
\label{sec:rew-summary}
% \section{Summary}%
% \label{sec:rew-summary}
In this chapter, we introduced a systematic view of the execution of \minizinc{}, revisiting the rewriting from high-level \minizinc\ to solver-level \flatzinc{}.
We first introduced the intermediate languages \microzinc{} and \nanozinc{} and explained how \minizinc\ can be transformed into a set of \microzinc\ definitions and a \nanozinc\ program.
We then, crucially, discussed how to partially evaluate a \nanozinc\ program using \microzinc\ definitions and present formal definitions of the rewriting rules applied during partial evaluation.
% In this chapter, we introduced a systematic view of the execution of \minizinc{}, revisiting the rewriting from high-level \minizinc\ to solver-level \flatzinc{}.
% We first introduced the intermediate languages \microzinc{} and \nanozinc{} and explained how \minizinc\ can be transformed into a set of \microzinc\ definitions and a \nanozinc\ program.
% We then, crucially, discussed how to partially evaluate a \nanozinc\ program using \microzinc\ definitions and present formal definitions of the rewriting rules applied during partial evaluation.
Continuously applying these rules would result in a correct solver-level model, but it is unlikely to be the best model for the solver.
We, therefore, discuss multiple techniques to improve the solver-level constraint model during the partial evaluation of \nanozinc{}.
First, we introduce a novel technique to eliminate all unused variables and constraints: we track all constraints that are introduced only to define a variable.
This means we can keep an accurate count of when a variable becomes unused by counting only the references to a variable in constraints that do not help define it.
Then, we discuss the use of \gls{propagation} during the partial evaluation of the \nanozinc\ program.
This technique can help shrink the domains of the decision variable or even combine variables known to be equal.
When a redefinition of a constraint requires the introspection into the current domain of a variable, it is often important to have the tightest possible domain.
Hence, we discuss how in choosing the next \nanozinc\ constraint to rewrite, the interpreter can sometimes delay the rewriting of certain constraints to ensure the most amount of information is available.
\Gls{cse}, our next optimisation technique, ensures that we do not create or evaluate the same constraint or function twice and reuse variables where possible.
Finally, the last optimisation technique we discuss is the use of constraint \gls{aggregation}.
The use of \gls{aggregation} ensures that individual functional constraints can be collected and combined into an aggregated form.
This allows us to avoid the existence of intermediate variables in some cases.
This optimisation is very important for \gls{mip} solvers.
% Continuously applying these rules would result in a correct solver-level model, but it is unlikely to be the best model for the solver.
% We, therefore, discuss multiple techniques to improve the solver-level constraint model during the partial evaluation of \nanozinc{}.
% First, we introduce a novel technique to eliminate all unused variables and constraints: we track all constraints that are introduced only to define a variable.
% This means we can keep an accurate count of when a variable becomes unused by counting only the references to a variable in constraints that do not help define it.
% Then, we discuss the use of \gls{propagation} during the partial evaluation of the \nanozinc\ program.
% This technique can help shrink the domains of the decision variable or even combine variables known to be equal.
% When a redefinition of a constraint requires the introspection into the current domain of a variable, it is often important to have the tightest possible domain.
% Hence, we discuss how in choosing the next \nanozinc\ constraint to rewrite, the interpreter can sometimes delay the rewriting of certain constraints to ensure the most amount of information is available.
% \Gls{cse}, our next optimisation technique, ensures that we do not create or evaluate the same constraint or function twice and reuse variables where possible.
% Finally, the last optimisation technique we discuss is the use of constraint \gls{aggregation}.
% The use of \gls{aggregation} ensures that individual functional constraints can be collected and combined into an aggregated form.
% This allows us to avoid the existence of intermediate variables in some cases.
% This optimisation is very important for \gls{mip} solvers.
Finally, we test the described system using an experimental implementation.
We compare this experimental implementation against the current \minizinc\ interpreter, version 2.5.3, and look at both runtime and its memory usage.
Although the experimental implementation there are instances where the experimental implementation uses more memory than the current \minizinc\ interpreter, it clearly outperforms the current \minizinc\ interpreter in terms of time.
% Finally, we test the described system using an experimental implementation.
% We compare this experimental implementation against the current \minizinc\ interpreter, version 2.5.3, and look at both runtime and its memory usage.
% Although the experimental implementation there are instances where the experimental implementation uses more memory than the current \minizinc\ interpreter, it clearly outperforms the current \minizinc\ interpreter in terms of time.

3
chapters/3_rewriting_preamble.tex
View File

@ -48,8 +48,7 @@ This chapter is organised as follows. \Cref{sec:4-micronano} introduces the
propose that enables more efficient flattening. \Cref{sec:4-simplification}
describes how we can perform various processing and simplification steps on this
representation, and in \cref{sec:4-experiments} we report on the experimental
results of the prototype implementation. Finally, \Cref{sec:4-conclusion}
presents our conclusions.
results of the prototype implementation.
\begin{figure}
\centering