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

Small fixes

Browse Source
This commit is contained in:
Jip J. Dekker 2021-05-21 14:47:36 +10:00
parent 372c1557aa
commit 3469458307
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
2 changed files with 28 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.chktexrc
View File

@ -2,3 +2,4 @@
VerbEnvir { pgfpicture tikzpicture mzn nzn plain grammar proof }
MathCmd { \hypo }
WipeArg { \mzninline:{} \nzninline:{} \Sem:{} \texttt:{} }
CmdLine { -n21 }

53
chapters/3_rewriting.tex
View File

@ -155,8 +155,9 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
\mzninline{int_plus(x,y)}. As mentioned above, more complex rules for
rewriting conditionals with variables, such as \mzninline{if x then A
else B endif} and \mzninline{A[x]} where \mzninline{x} is a variable,
are also replaced by function calls (\eg\ \mzninline{if_then_else([x,
true], [A, B])} and \mzninline{element(a, x)} respectively).
are also replaced by function calls (\eg\
\mzninline{if_then_else([x, true], [A, B])} and
\mzninline{element(a, x)} respectively).
\item Replace optional variables into non-optional forms. As shown by Mears et
al., optional variable types can be represented using a variable of the
@ -432,7 +433,7 @@ suitable alpha renaming.
The rules in \cref{fig:4-rewrite-to-nzn-calls} handle function calls. The first
rule (Call) evaluates a function call expression in the context of a \microzinc\
program \(\Prog\) and \nanozinc\ program \(\Env\). The rule evaluates the
program \(\Prog{}\) and \nanozinc\ program \(\Env{}\). The rule evaluates the
function body \(\ptinline{E}\) where the formal parameters \(p_{i}\) are
substituted by the call arguments \(a_{i}\).\footnote{We use
\(E_{[a \mapsto b]}\) as a notation for the expression \(E\) where \(a\) is
@ -656,8 +657,8 @@ prepended by \texttt{↳}).
Evaluating \mzninline{constraint c} will result in the domain of \mzninline{c}
to be bound to \mzninline{true}, the disjunction then trivially holds,
independent of the value of \mzninline{b}. The constraint \mzninline{abs(x) >
y} is therefore not required. However, the rewriting has to choose a
independent of the value of \mzninline{b}. The constraint
\mzninline{abs(x) > y} is therefore not required. However, the rewriting has to choose a
particular order in which arguments are evaluated, so it is always possible
that it already evaluated the left-hand side before ``noticing'' that the
disjunction is true.
@ -895,7 +896,7 @@ for MIP\@.
\subsection{Common Sub-expression Elimination}\label{sec:4-cse}
\jip{Adjust with the background section. Just needs to talk about microzinc optimisation.}
\jip{Adjust with the background section. Just needs to talk about \microzinc{} optimisation.}
The simplifications introduced above remove definitions from the model when we
can detect that they are no longer needed. In some cases, it is even possible to
@ -958,27 +959,27 @@ combine both approaches. The static approach can be further improved by
\emph{inlining} function calls, since that may expose more calls as being
syntactically equal.
\jip{TODO: \gls{cse} will be discussed in the background. How can we make this
\jip{TODO:\ \gls{cse} will be discussed in the background. How can we make this
more specific to how it works in \nanozinc{}.}
\paragraph{Reification}
\jip{Adjust with information in the background section. Is there anything specific to the microzinc/nanozinc system?}
\jip{Adjust with information in the background section. Is there anything specific to the \microzinc{}/\nanozinc{} system?}
Many constraint modelling languages, including \minizinc{}, not only enable
constraints to be globally enforced, but typically also support constraints to
be \emph{reified} into a Boolean variable. Reification means that a variable
\mzninline{b} is constrained to be true if and only if a corresponding
constraint \mzninline{c(...)} holds. We have already seen reification in
\cref{ex:4-absreif}: the truth of constraint \mzninline{abs(x) > y} was bound to
a Boolean variable \mzninline{b1}, which was then used in a disjunction. We say
that the same constraint can be used in \emph{root context} as well as in a
\emph{reified context}. In \minizinc{}, almost all constraints can be used in both
contexts. However, reified constraints are often defined in the library in terms
of complicated decompositions into simpler constraints, or require specialised
algorithms in the target solvers. In either case, it can be very beneficial for
the efficiency of the generated \nanozinc\ program if we can detect that a
reified constraint is in fact not required.
\constraints{} to be globally enforced, but typically also support
\constraints{} to be \emph{reified} into a Boolean variable. Reification means
that a variable \mzninline{b} is constrained to be true if and only if a
corresponding constraint \mzninline{c(...)} holds. We have already seen
reification in \cref{ex:4-absreif}: the truth of constraint \mzninline{abs(x) >
y} was bound to a Boolean variable \mzninline{b1}, which was then used in a
disjunction. We say that the same constraint can be used in \emph{root context}
as well as in a \emph{reified context}. In \minizinc{}, almost all constraints
can be used in both contexts. However, reified constraints are often defined in
the library in terms of complicated decompositions into simpler constraints, or
require specialised algorithms in the target solvers. In either case, it can be
very beneficial for the efficiency of the generated \nanozinc\ program if we can
detect that a reified constraint is in fact not required.
If a constraint is present in the root context, it means that it must hold
globally. If the same constraint is used in a reified context, it can therefore
@ -1018,7 +1019,7 @@ addition recognises constraints in \emph{positive} contexts, also known as
\emph{half-reified} \autocite{feydy-2011-half-reif}. A full explanation and
discussion of half-reification can be found in \cref{ch:half_reif}.
\jip{TODO: Reification should also be discussed in the background. How can we
\jip{TODO:\ Reification should also be discussed in the background. How can we
make this more specific to how it works in \nanozinc{}.}
\subsection{Constraint Aggregation}%
@ -1044,8 +1045,8 @@ operators. For example the evaluation of the linear constraint \mzninline{x +
These \nanozinc\ definitions are correct, but, at least for \gls{mip} solvers,
the existence of the intermediate variables is likely to have a negative impact
on the \gls{solver}'s performance. These \glspl{solver} would likely perform
better had they received the linear constraint \mzninline{int_lin_le([1,2,-1],
[x,y,z], 0)} directly. Since many solvers support linear constraints, it is
better had they received the linear constraint
\mzninline{int_lin_le([1,2,-1], [x,y,z], 0)} directly. Since many solvers support linear constraints, it is
often an additional burden to have intermediate values that have to be given a
value in the solution.
@ -1067,7 +1068,7 @@ visit the functional definitions and combine their constraints. The top-level
intermediate variables become unused, they will be removed using the normal
mechanisms.
\jip{TODO: Aggregation is also part of the background. How can we make this more
\jip{TODO:\ Aggregation is also part of the background. How can we make this more
specific to how it works in \nanozinc{}.}
\section{Experiments}\label{sec:4-experiments}
@ -1142,7 +1143,7 @@ unoptimised prototype to a mature piece of software.
\pgfplotstableread[
col sep=comma,
]{assets/table/rew_functional.csv}\rewFuncData
]{assets/table/rew_functional.csv}\rewFuncData{}
\begin{tikzpicture}
\begin{axis}[
xbar,