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

Adjust nanozinc descriptions to match new syntax

Browse Source
This commit is contained in:
Jip J. Dekker 2021-04-07 11:35:27 +10:00
parent eb67f0635d
commit e5e8b9d7ec
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
2 changed files with 67 additions and 73 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
assets/shorthands.tex
View File

@ -1,5 +1,5 @@
\newcommand{\eg}{e.g.,\xspace{}}
\newcommand{\ie}{e.g.,\xspace{}}
\newcommand{\ie}{i.e.,\xspace{}}
\newcommand{\flatzinc}{\gls{flatzinc}\xspace{}}
\newcommand{\microzinc}{\gls{microzinc}\xspace{}}
\newcommand{\minisearch}{\gls{minisearch}\xspace{}}

138
chapters/4_rewriting.tex
View File

@ -196,11 +196,10 @@ The translation from \minizinc\ to \microzinc\ involves the following steps:
\subsection{Partial Evaluation of \glsentrytext{nanozinc}}\label{sub:4-partial}
Each call in a \nanozinc\ program is either a primitive, or it has a
corresponding \microzinc\ definition. The goal of partial evaluation is to
transform the \nanozinc\ program into (essentially) \flatzinc, i.e., a program
where all calls are either solver-level constraint primitives, or defining
variables.
Each call in a \nanozinc\ program is either a call to a solver-level predicate,
or it has a corresponding \microzinc\ function definition. The goal of partial
evaluation is to transform the \nanozinc\ program into (essentially) \flatzinc,
\ie\ a program where all calls are calls to solver-level predicates.
To achieve this, we define the semantics of \microzinc\ as a rewriting system
that produces \nanozinc\ calls. Each non-primitive call in a \nanozinc\ program
@ -254,7 +253,7 @@ list of definitions. Each definition binds a variable to the result of a call or
another variable, and it is associated with a list of identifiers of auxiliary
constraints. The \nanozinc\ model contains a special definition
\mzninline{true}, containing all ``root-context'' constraints of the model,
i.e., those that have to hold globally and are not just used to define an
\ie\ those that have to hold globally and are not just used to define an
auxiliary variable. Only root-context constraints (attached to \mzninline{true})
can effectively constrain the overall problem. Constraints attached to
definitions originate from function calls, and since all functions are
@ -281,17 +280,10 @@ result.
constraint int_gt(z, y);
\end{nzn}
\jip{Adjust text to match the new \nanozinc\ formatting.}
The variables \mzninline{x} and \mzninline{y} result in identifiers bound to
the special built-in \mzninline{mkvar}, which records the variable's domain in
its arguments. Evaluating the call \mzninline{abs(x)} introduces a new
variable \mzninline{z} (with unrestricted domain) and the \mzninline{int_abs}
constraint that is used to define \mzninline{z}, bound to a fresh identifier
\mzninline{b0}. A fresh identifier \mzninline{t} is introduced to capture both
the result \mzninline{z} as well as the list of defining constraints,
\mzninline{[b0]}. The top-level constraint \mzninline{abs(x) > y} is rewritten
into \mzninline{int_gt(t,y)} and bound to fresh identifier \mzninline{b1},
which is added to the root-context definition \mzninline{true}.
Evaluating the call \mzninline{abs(x)} introduces a new variable \mzninline{z}
(with unrestricted domain) and the \mzninline{int_abs} constraint that is used
to define \mzninline{z}. The top-level constraint \mzninline{abs(x) > y} is
rewritten into \mzninline{int_gt(z, y)} and added as a top-level constraint.
\end{example}
\subsection{Rewriting Rules}
@ -311,7 +303,7 @@ suitable alpha renaming.
\begin{figure*}
\centering
\begin{prooftree}
\hypo{\ptinline{F(\(p_1, \ldots{}, p_k\)) = E;} \in{} \Prog{} \text{~where the~} p_i \text{~are fresh}}
\hypo{\texttt{function} ~t\texttt{:}~\ptinline{F(\(p_1, \ldots{}, p_k\)) = E;} \in{} \Prog{} \text{~where the~} p_i \text{~are fresh}}
\infer[no rule]1{\Sem{E}{\Prog, \Env_{[p_i \mapsto a_i, \forall{} 1 \leq{} i \leq{} k]}} \Rightarrow \tuple{v, \Env'}}
\infer1[(Call)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{v, \Env'_{[a_i \mapsto p_i, \forall{} 1 \leq{} i \leq{} k]}}}
\end{prooftree} \\
@ -322,7 +314,7 @@ suitable alpha renaming.
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog}
\hypo{\texttt{predicate}~\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog}
\infer1[(CallPredicate)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_0} \Rightarrow
\tuple{\texttt{constraint~} \text{F}(v_1, \ldots, v_k), \Env_k}}
\end{prooftree}
@ -541,8 +533,8 @@ prepended by \texttt{└── }).
(we will come back to this in \cref{sec:4-cse}). Following the rewriting
rules, the generated \nanozinc\ code will look very similar to the code
generated in \cref{ex:4-absnzn}, but with an additional \mzninline{bool_or}
constraint for the disjunction, which uses the variable \mzninline{b1} that
was introduced for \mzninline{abs(x) > y}:
constraint for the disjunction, which uses a variable \mzninline{b} that will
be introduced for \mzninline{abs(x) > y}:
\begin{nzn}
var true: c;
@ -550,24 +542,26 @@ prepended by \texttt{└── }).
var -10..10: y;
var int: z;
└── constraint int_abs(x, z);
var bool: b1;
└── constraint int_gt(z, y);
constraint bool_or(b1, c);
var bool: b;
└── constraint int_gt_reif(z, y, b);
constraint bool_or(b, c);
\end{nzn}
Since \mzninline{c} is bound to \mzninline{true}, the disjunction
\mzninline{b2} trivially holds, independent of the value of \mzninline{b1}.
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.
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
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.
If the system now simplifies the constraint \mzninline{b2} to \mzninline{true},
the identifier \mzninline{b1} will become unused, since it was only
referenced from the \mzninline{bool_or} call. Removing \mzninline{b1} leads
to \mzninline{t} not being used by any constraint, so its definition can be
removed. This in turn means that \mzninline{b0} is not referenced anywhere
and can be removed, and then \mzninline{z}. The resulting \nanozinc\ program
If the system now simplifies the constraint \mzninline{bool_or(b, c)} to
\mzninline{true}, the identifier \mzninline{b} will become unused outside of
its auxiliary definitions, since it was only referenced from the
\mzninline{bool_or} call. Removing \mzninline{b} leads will also its defining
constraint, \mzninline{int_gt_reif}, being removed. This in turn means that
\mzninline{z} is not referenced anywhere outside its auxiliary definitions and
can be removed together with its definition. The resulting \nanozinc\ program
is much more compact:
\begin{nzn}
@ -580,35 +574,35 @@ prepended by \texttt{└── }).
other parts of the model not shown here and therefore not removed.
\end{example}
\jip{adjust text to match the new \nanozinc\ syntax}
Note how \mzninline{t} acts as a unique name for the result of the let
expression (and thus the function call) --- we could not simply have used
\mzninline{z}, because then \mzninline{b0} would have kept \mzninline{z} alive.
Note how how counting usage of variables outside its auxiliary definitions
allows us to remove the \mzninline{z} variable --- we could not simply have
counted the usage of \mzninline{z} in all constraints since the constraint used
to define it, \mzninline{int_abs(x, z)}, would have kept it alive.
It is worth noting the difference between the constraints \mzninline{b0} and
\mzninline{b1} in this example: \mzninline{b0} is referenced from the auxiliary
constraint list of another variable. This means that it is a constraint that
defines the value of a variable, and it can be enforced globally (it must hold,
under all circumstances). On the other hand, \mzninline{b1} is referenced as an
argument to the \mzninline{bool_or} call. This means that the constraint does
not have to hold globally --- rather, we require the variable \mzninline{b1} to
reflect whether the constraint holds or not, so that the \mzninline{bool_or}
can implement the disjunction. These types of constraints are typically called
\emph{reified} in constraint modelling. So \nanozinc\ uses the same syntax for
reified and globally true constraints, allocating an identifier (such as
\mzninline{b0} or \mzninline{b1}) for any constraint. Whether the constraint is
reified or not depends on where that identifier appears.
It is important to notice the difference between constraints that appear at the
top level and constraints that appear as part of the auxiliary definitions of a
variable. Top-level constraint help define the problem, they are globally
enforced and cannot be removed from the problem unless it can be proved that its
relationship is already enforced. Constraint in auxiliary definitions, on the
other hand, are used to define a variable. Auxiliary definitions generally occur
from a functional relationship, like \mzninline{abs(x)} in the example, or from
the reflection if a constraint holds or not, like \mzninline{abs(x) > y} when
used in the disjunction with \mzninline{c}. These types of reflection
constraints are typically called \glspl{reification}. In this thesis we will
follow the same naming standard as \minizinc\ where a \gls{reification} of a
constraint has the same name as the original constraint with \texttt{\_reif}
appended.
\begin{example}
The importance of the use of auxiliary definitions when removing dead
variables and constraints is demonstrated in the following example:
\begin{mzn}
int n;
int: n;
var int: x;
function var int: f(var int: x, int: i) = let {
var int: y;
constraint y = int_minus(x, i);
constraint y = x div i;
} in y;
constraint [f(x,i) | i in 1..n][1] == 10;
\end{mzn}
@ -616,22 +610,22 @@ reified or not depends on where that identifier appears.
The rewriting of this instance will initially create the \mzninline{n}
elements for the array comprehension. Each element is evaluated as a new
variable \mzninline{y} and a constraint to ensure that \mzninline{y} is the
subtraction of \mzninline{x} and \mzninline{i}. Although \mzninline{n}
variables are created, only the first variable is constrained to be 10. All
other variables can thus be removed and the model will stay equisatisfiable.
division of \mzninline{x} and \mzninline{i}. Although \mzninline{n} variables
are created, only the first variable is constrained to be 10. All other
variables can thus be removed and the model will stay equisatisfiable.
In the \nanozinc\ version of this model, each of the subtraction constraints
will be added to the list of auxiliary constraints of its corresponding
In the \nanozinc\ version of this model, each of the division constraints will
be added to the list of auxiliary constraints of its corresponding
\mzninline{y} variable. When, after evaluating the array access, all of those
variables except the first are detected to be unused, their removal triggers
the removal of the subtraction constraints.
For this example the current \minizinc\ compiler, version 2.3.2, will produce
For this example the current \minizinc\ compiler, version 2.5.5, will produce
a \flatzinc\ program that contains the variable \mzninline{x}, \mzninline{n-1}
variables \mzninline{y}, and \mzninline{n} constraints for the subtraction.
variables \mzninline{y}, and \mzninline{n} constraints for the division.
The first \mzninline{y} variable is directly replaced with the constant 10.
Using the \nanozinc\ system, only 1 variable, \mzninline{x}, and 1 constraint,
\mzninline{10 = int_minus(x,1);} is produced.
\mzninline{constraint int_minus(x,1,10);} is produced.
\end{example}
\paragraph{Implementation} The removal of unused identifiers is taken care of
@ -737,7 +731,7 @@ Rewriting a function call that has a \microzinc\ definition and rewriting a
constraint due to propagation are very similar. The interpreter therefore simply
interleaves both forms of rewriting. Efficient constraint propagation engines
``wake up'' a constraint only when one of its variables has received an update
(i.e., when its domain has been shrunk). To enable this, the interpreter needs
(\ie\ when its domain has been shrunk). To enable this, the interpreter needs
to keep a data structure linking variables to the constraints where they appear
(in addition to the reverse links from calls to the variables in their
arguments). These links do not take part in the reference counting.
@ -746,14 +740,14 @@ arguments). These links do not take part in the reference counting.
Adding constraint propagation and simplification into the rewriting system means
that the system becomes non-confluent, and some orders of execution may produce
``better'', i.e., more compact or more efficient, \nanozinc.
``better'', \ie\ more compact or more efficient, \nanozinc.
\begin{example}
The following example is similar to code found in the \minizinc\ libraries of
MIP solvers.
\begin{mzn}
predicate lq_zero_if_b(var int: x, var bool: b) =
function var int: lq_zero_if_b(var int: x, var bool: b) =
x <= ub(x)*(1-b);
\end{mzn}
@ -890,7 +884,7 @@ and the evaluation will proceed as normal with the root context constraint.
Consider the fragment:
\begin{mzn}
predicate p(var int: x, var int: y) = q(x) /\ r(y);
function var bool: p(var int: x, var int: y) = q(x) /\ r(y);
constraint b0 <-> q(x);
constraint b1 <-> t(x,y);
constraint b1 <-> p(x,y);
@ -900,14 +894,14 @@ and the evaluation will proceed as normal with the root context constraint.
\mzninline{q(x)} for the original call. Suppose processing the second
constraint we discover \mzninline{t(x,y)} is \mzninline{true}, setting
\mzninline{b1}. When we process \mzninline{q(x)} in the call
\mzninline{t(x,y)} we find it is the root context. So CSE needs to set
\mzninline{t(x,y)} we find it is the root context. So CSE needs to set
\mzninline{b0} to \mzninline{true}.
\end{example}
\minizinc\ distinguishes not only between root and reified contexts, but in
addition recognises constraints in \emph{positive} contexts, also known as
\emph{half-reified} \autocite{feydy-2011-half-reif}. We omit the details here
for brevity, but the CSE approach generalises to this extension.
\emph{half-reified} \autocite{feydy-2011-half-reif}. A full explanation and
discussion of half-reification can be found in \cref{ch:half_reif}.
\section{Experiments}\label{sec:4-experiments}
@ -932,9 +926,9 @@ gains that are possible thanks to the new architecture.
As a first experiment, we selected 20 models from the annual \minizinc\
challenge and compiled 5 instances of each model to \flatzinc, using the current
\minizinc\ release version 2.4.3 and the new prototype system. In both cases we
use the standard \minizinc\ library of global constraints (i.e., we decompose
use the standard \minizinc\ library of global constraints (\ie\ we decompose
those constraints rather than using solver built-ins, in order to stress-test
the flattening). We measured pure flattening time, i.e., without time required
the flattening). We measured pure flattening time, \ie\ without time required
to parse and typecheck in version 2.4.3, and without time required for
compilation to \microzinc\ in the new system (compilation is usually very fast).
Times are averages of 10 runs.\footnote{All models obtained from