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

Style changes for captions

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-25 16:57:58 +10:00
parent c53d492e11
commit 9ad2019622
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
7 changed files with 82 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
assets/glossary.tex
View File

@ -238,7 +238,7 @@
}
\newglossaryentry{flatzinc}{
name={Flat\-Zinc},{}
name={Flat\-Zinc},
description={A subset of \gls{minizinc} chosen to represent \glspl{slv-mod}. It is the standard format in which \gls{minizinc} communicates with its \glspl{solver}},
}

2
chapters/1_introduction.tex
View File

@ -60,7 +60,7 @@ Finally, \lrefrange{line:intro:con:start}{line:intro:con:end} express the \const
\begin{listing}
\amplfile{assets/listing/intro_open_shop.mod}
\caption{\label{lst:intro-open-shop} An \glsxtrshort{ampl} model of the open shop problem}
\caption{\label{lst:intro-open-shop} An \glsxtrshort{ampl} model of the open shop problem.}
\end{listing}
The \glsxtrshort{ampl} model provides a clear definition of the problem class, but it can be argued that its meaning is hard to decipher.

7
chapters/2_background.tex
View File

@ -102,7 +102,7 @@ Its expressive language and extensive library of \glspl{global} allow users to e
\begin{listing}
\mznfile{assets/listing/back_knapsack.mzn}
\caption{\label{lst:back-mzn-knapsack} A \minizinc{} model describing a 0-1 knapsack problem}
\caption{\label{lst:back-mzn-knapsack} A \minizinc{} model describing a 0-1 knapsack problem.}
\end{listing}
Note that, although more textual and explicit, the \minizinc{} model definition is very similar to our earlier mathematical definition.
@ -906,7 +906,7 @@ Different types of \solvers{} can also have access to different types of \constr
\begin{listing}
\mznfile{assets/listing/back_tsp.mzn}
\caption{\label{lst:back-mzn-tsp} An \minizinc{} model describing the \gls{tsp}}
\caption{\label{lst:back-mzn-tsp} An \minizinc{} model describing the \gls{tsp}.}
\end{listing}
A \minizinc{} model for the same problem is shown in \cref{lst:back-mzn-tsp}.
@ -1276,8 +1276,7 @@ For instance, this replaces enumerated types by normal integers.
\begin{figure}
\centering
\includegraphics[width=\linewidth]{assets/img/back_compilation_structure}
\caption{\label{fig:back-mzn-comp} The compilation structure of the \minizinc\
compiler.}
\caption{\label{fig:back-mzn-comp} The compilation structure of the \minizinc \compiler{}.}
\end{figure}
The middle-end contains the most important two processes: \gls{rewriting} and optimization.

15
chapters/3_rewriting.tex
View File

@ -32,7 +32,7 @@ The process can even be made incremental: in \cref{ch:incremental} we discuss ho
\begin{figure}
\centering
\includegraphics[width=\linewidth]{assets/img/rew_compilation_structure}
\caption{\label{fig:rew-comp} The proposed process for the compilation of \minizinc{} instances.}
\caption{\label{fig:rew-comp} The proposed process for the compilation of \minizinc{} instances.}
\end{figure}
The process of the new architecture is shown in \cref{fig:rew-comp}.
@ -339,8 +339,7 @@ Although pure \microzinc{} behaves the same under any call evaluation strategy,
\infer1[(CallNative)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{}
\tuple{\ensuremath{\texttt{constraint}~\ptinline{F}(a_1, \ldots, a_k), \Env}}}
\end{prooftree}
\caption{\label{fig:rew-rewrite-to-nzn-calls} Rewriting rules for partial evaluation
of \microzinc{} calls to \nanozinc{}.}
\caption{\label{fig:rew-rewrite-to-nzn-calls} Rewriting rules for partial evaluation of \microzinc{} calls to \nanozinc{}.}
\end{figure*}
The rules in \cref{fig:rew-rewrite-to-nzn-calls} handle function calls.
@ -393,8 +392,7 @@ Since these are directly supported by the \solver{}, they simply need to be tran
\infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env', \Ctx} \Rightarrow{} \tuple{x, \Env''}}
\infer1[(ItemTupD)]{\Sem{\(\left(t_{1}\texttt{:}~x_{1}, \ldots, t_{k}\texttt{:}~x_{k}\right) = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env''}}
\end{prooftree}
\caption{\label{fig:rew-rewrite-to-nzn-let} Rewriting rules for partial evaluation
of \microzinc{} \glspl{let} to \nanozinc{}.}
\caption{\label{fig:rew-rewrite-to-nzn-let} Rewriting rules for partial evaluation of \microzinc{} \glspl{let} to \nanozinc{}.}
\end{figure*}
The rules in \cref{fig:rew-rewrite-to-nzn-let} consider \glspl{let}.
@ -453,8 +451,7 @@ We use the notation \(x_{\langle{}i\rangle}\) to mark the \(i^{\text{th}}\) memb
\infer1[(ListG)]{\Sem{\([E~|~ x \mbox{~in~} \mathit{PE}, \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env} \Rightarrow{}
\tuple{\mbox{concat} [ A_v~|~v \in{} S ], \Env{} \cup{} \bigcup{}_{v \in{} S} \Env{}_{v}}}
\end{prooftree}
\caption{\label{fig:rew-rewrite-to-nzn-other} Rewriting rules for partial evaluation
of other \microzinc{} expressions to \nanozinc{}.}
\caption{\label{fig:rew-rewrite-to-nzn-other} Rewriting rules for partial evaluation of other \microzinc{} expressions to \nanozinc{}.}
\end{figure*}
Finally, the rules in \cref{fig:rew-rewrite-to-nzn-other} handle the evaluation of \variables{}, constants, \glspl{conditional} and \glspl{comprehension}.
@ -821,9 +818,7 @@ These are very encouraging results, given that we are comparing a largely unopti
\includegraphics[width=\columnwidth]{assets/img/rew_compare_memory}
\caption{\label{sfig:rew-comparemem}Maximum resident set size (kbytes)}
\end{subfigure}
\caption{\label{fig:4-runtime}Performance on \gls{rewriting} MiniZinc Challenge
\instances{}. \minizinc{} 2.5.5 (x-axis) vs new architecture (y-axis), log-log
plot. Dots below the line indicate the new system is better.}
\caption{\label{fig:4-runtime}Performance on \gls{rewriting} \minizinc{} Challenge \instances{}. \minizinc{} 2.5.5 (x-axis) vs our prototype (y-axis), log-log plot. Dots below the line indicate the new system is better.}
\end{figure}
Our second experiment considers three well-known computational recursive functions: Ackermann, Fibonacci, and Takeuchi.

62
chapters/4_half_reif.tex
View File

@ -434,7 +434,7 @@ The behaviour of these transformations is shown in \cref{fig:half-ctx-trans}.
\hypo{\ctxeval{\texttt{[}e_{1}, \ldots, e_{n}\texttt{]}}{ctx}}
\infer1[(Arr)]{\ctxeval{e_{1}}{ctx}, \ldots, \ctxeval{e_{n}}{ctx}}
\end{prooftree}
\caption{\label{fig:half-analysis-expr} Context inference rules for \microzinc\ expressions.}
\caption{\label{fig:half-analysis-expr} Context inference rules for \microzinc{} expressions.}
\end{figure*}
\Cref{fig:half-analysis-expr} shows the inference rules for all \microzinc{} expressions, apart from \glspl{let}.
@ -494,7 +494,7 @@ However, we currently do not provide such analysis and annotate functions by han
\Return{\tuple{\mixc, \ldots, \mixc}}
}
}
\caption{\label{alg:arg-ctx} Definition of the ``argCtx'' function for \minizinc\ operators.}
\caption{\label{alg:arg-ctx} Definition of the ``argCtx'' function for \minizinc{} operators.}
\end{algorithm}
The context in which the result of a call expression is used must also be considered.
@ -568,7 +568,7 @@ If such an expression is evaluated in the context \(ctx\), then its members can
\hypo{\ctxitem{\epsilon{}}}
\infer1[(Item0)]{}
\end{prooftree}
\caption{\label{fig:half-analysis-it} Context inference rules for \microzinc\ let-expressions.}
\caption{\label{fig:half-analysis-it} Context inference rules for \microzinc{} let-expressions.}
\end{figure*}
\Cref{fig:half-analysis-it} shows the inference rules for \glspl{let} and their inner items.
@ -814,7 +814,7 @@ The goal of the algorithm is now to identify and remove vertices that are not ma
}
}
\(G' \longleftarrow \tuple{V', E'}\)\;
\caption{\label{alg:half-compression} implication \gls{chain-compression} algorithm}
\caption{\label{alg:half-compression} implication \gls{chain-compression} algorithm.}
\end{algorithm}
The algorithm can be further improved by considering implied conjunctions.
@ -872,6 +872,60 @@ All usages of the previously recorded \gls{cvar} are replaced by the new result.
The dependency tracking, through the use of \constraints{} attached to \variables{}, ensures that all defining \constraints{} are removed from the model.
This ensures that all \variables{} and \constraints{} created for the earlier version are correctly removed.
\begin{example}
Consider, for example, the following \minizinc{} fragment, which uses the linearization of \mzninline{int_le}.
\begin{mzn}
predicate int_le_imp(var int: x, int: y, var bool: b) =
x <= ub(x) - (ub(x) - y) * b;
predicate int_le_reif(var int: x, int: y, var bool: b) =
x <= ub(x) - (ub(x) - y) * b /\ x >= (y + 1) - (y + 1) * b;
var 1..10: i;
constraint j \/ int_le(i, 4);
constraint k xor int_le(i, 4);
\end{mzn}
In this fragment the call \mzninline{int_le(i, 4)} occurs both in \posc{} and \mixc{} context.
Although, in this case, the \compiler{} is able to hoist the expression to share it between the two \constraint{}, as discussed in \cref{sec:rew-cse}, the same expressions might result from function \gls{rewriting} were this is not possible.
After \gls{rewriting} the first \constraint{}, the \nanozinc{} program would contain the following definitions.
\begin{nzn}
var bool: b1;
↳ constraint int_lin_le([1, 6], [i, b1], 10);
constraint bool_clause([j, b1], []);
\end{nzn}
In this program \mzninline{b1} is the \gls{cvar} of the \gls{half-reif} of the \mzninline{int_le(i, 4)} call.
The \gls{cvar} is added to the \gls{cse} table as the result of the call.
However, since the second call is in \mixc{} context, it cannot use the \gls{half-reif}, and must create the \gls{reif} instead.
This results in the following \nanozinc{} program.
\begin{nzn}
var bool: b1;
↳ constraint int_lin_le([1, 6], [i, b1], 10);
constraint bool_clause([j, b1], []);
var bool: b2;
↳ constraint int_lin_le([1, 6], [i, b2], 10);
↳ constraint int_lin_le([-1, -5], [i, b2], -5);
constraint bool_not(k, b2);
\end{nzn}
Now when \mzninline{b2} is added to the \gls{cse} table as the \gls{cvar} of the \gls{reif} of the \mzninline{int_le(i, 4)} call, it notices that there is already a result in table for the same call in a weaker context.
As such, it replaces all occurrences of the \gls{cvar} of the \gls{half-reif}, found in the table, with the \gls{cvar} of the \gls{reif}.
Once all usage of the \gls{cvar} have been removed, it and its dependent \constraints{} are removed, resulting in the following \nanozinc{} program.
\begin{nzn}
constraint bool_clause([j, b2], []);
var bool: b2;
↳ constraint int_lin_le([1, 6], [i, b2], 10);
↳ constraint int_lin_le([-1, -5], [i, b2], -5);
constraint bool_not(k, b2);
\end{nzn}
\end{example}
Because the expression itself is changed when a negation is moved inwards, it may not always be clear when the same expression is used in both \posc{} and \negc{} context.
This problem is solved by introducing a canonical form for expressions where negations can be pushed inwards.
In this form the result of \gls{rewriting} an expression and its negation are collected in the same place within the \gls{cse} table.

29
chapters/5_incremental.tex
View File

@ -36,12 +36,12 @@ For example, \mzninline{uniform_neighbourhood(x, 0.2)} would result in each vari
\begin{listing}
\mznfile{assets/listing/inc_lns_minisearch_pred.mzn}
\caption{\label{lst:inc-lns-minisearch-pred} A simple random \gls{lns} predicate implemented in \minisearch{}}
\caption{\label{lst:inc-lns-minisearch-pred} A simple random \gls{lns} predicate implemented in \minisearch{}.}
\end{listing}
\begin{listing}
\mznfile{assets/listing/inc_lns_minisearch.mzn}
\caption{\label{lst:inc-lns-minisearch} A simple \gls{lns} \gls{meta-optimization} implemented in \minisearch{}}
\caption{\label{lst:inc-lns-minisearch} A simple \gls{lns} \gls{meta-optimization} implemented in \minisearch{}.}
\end{listing}
The second part of a \minisearch{} \gls{meta-optimization} is the \gls{meta-optimization} algorithm itself.
@ -97,8 +97,7 @@ Finally, the \mzninline{restart_limit} stops the search after a fixed number of
\begin{listing}
\mznfile{assets/listing/inc_restart_ann.mzn}
\caption{\label{lst:inc-restart-ann} New annotations to control the restarting
behaviour}
\caption{\label{lst:inc-restart-ann} New annotations to control the restarting behaviour.}
\end{listing}
\subsection{Advanced Meta-Optimisation Algorithms}
@ -136,7 +135,7 @@ Like \mzninline{sol}, it has versions for all basic \variable{} types.
\begin{listing}
\mznfile{assets/listing/inc_state_access.mzn}
\caption{\label{lst:inc-state-access} Functions for accessing previous \solver{} states}
\caption{\label{lst:inc-state-access} Functions for accessing previous \solver{} states.}
\end{listing}
In order to be able to initialize the \variables{} used for state access, we interpret \mzninline{on_restart} also before initial search using the same semantics.
@ -166,7 +165,7 @@ Therefore, users have to define their overall strategy in a new predicate.
\begin{listing}
\mznfile{assets/listing/inc_basic_complete.mzn}
\caption{\label{lst:inc-basic-complete} Complete \gls{lns} example}
\caption{\label{lst:inc-basic-complete} A complete \gls{lns} example.}
\end{listing}
We can also define round-robin and adaptive strategies using these primitives.
@ -178,8 +177,7 @@ This will activate a different \gls{neighbourhood} for each subsequent \gls{rest
\begin{listing}
\mznfile{assets/listing/inc_round_robin.mzn}
\caption{\label{lst:inc-round-robin} A predicate providing the round-robin
meta-heuristic}
\caption{\label{lst:inc-round-robin} A predicate providing the round-robin meta-heuristic.}
\end{listing}
%\paragraph{Adaptive \gls{lns}}
@ -189,7 +187,7 @@ For adaptive \gls{lns}, a simple strategy is to change the size of the \gls{neig
\begin{listing}
\mznfile{assets/listing/inc_adaptive.mzn}
\caption{\label{lst:inc-adaptive} A simple adaptive neighbourhood}
\caption{\label{lst:inc-adaptive} A simple adaptive neighbourhood.}
\end{listing}
\subsection{Optimization strategies}
@ -314,7 +312,7 @@ It simply replaces the functional form by a predicate \mzninline{status} (declar
\begin{listing}
\mznfile{assets/listing/inc_status.mzn}
\caption{\label{lst:inc-status} MiniZinc definition of the \mzninline{status} function}
\caption{\label{lst:inc-status} MiniZinc definition of the \mzninline{status} function.}
\end{listing}
\paragraph{\mzninline{sol} and \mzninline{last_val}}
@ -329,8 +327,7 @@ We use the current \domain{} of the \variable{}, \mzninline{dom(x)}, as the \dom
\begin{listing}
\mznfile{assets/listing/inc_sol_function.mzn}
\caption{\label{lst:inc-int-sol} MiniZinc definition of the \mzninline{sol}
function for integer variables}
\caption{\label{lst:inc-int-sol} MiniZinc definition of the \mzninline{sol} function for integer \variables{}.}
\end{listing}
The compilation of \mzninline{last_val} is similar to that for \mzninline{sol}.
@ -345,8 +342,7 @@ As such, it can be used in combination with other functions, such as \mzninline{
\begin{listing}
\mznfile{assets/listing/inc_uniform_slv.mzn}
\caption{\label{lst:inc-int-rnd} MiniZinc definition of the
\mzninline{uniform_nbh} function for floats}
\caption{\label{lst:inc-int-rnd} MiniZinc definition of the floating point \mzninline{uniform_nbh} function.}
\end{listing}
\paragraph{\mzninline{complete}}
@ -418,7 +414,7 @@ Note that the \flatzinc{} \gls{slv-mod} shown here has been simplified for prese
\begin{listing}
\mznfile{assets/listing/inc_basic_complete_transformed.mzn}
\caption{\label{lst:inc-flat-pred} \flatzinc{} that results from compiling \\
\caption{\label{lst:inc-flat-pred} The \flatzinc{} \gls{slv-mod} that results from \gls{rewriting} \\
\mzninline{basic_lns(uniformNeighbourhood(x,0.2))}.}
\end{listing}
@ -636,8 +632,7 @@ These orders can then be freely reassigned to any other slab.
\begin{listing}
\mznfile{assets/listing/inc_steelmillslab_neighbourhood.mzn}
\caption{\label{lst:inc-free-bin}Steel mill slab: \gls{neighbourhood} that frees
all orders assigned to a selected slab.}
\caption{\label{lst:inc-free-bin}Steel mill slab: \gls{neighbourhood} that frees all orders assigned to a selected slab.}
\end{listing}

4
chapters/A2_benchmark.tex
View File

@ -277,7 +277,7 @@ The data and original model are available at:
\begin{listing}
\mznfile{assets/listing/prize.mzn}
\caption{\label{lst:bench-prize} A \minizinc{} model for the Prize Collecting Path problem}
\caption{\label{lst:bench-prize} A \minizinc{} model for the Prize Collecting Path problem.}
\end{listing}
\paragraph{QCP-Max} This problem was introduced in by \textcite{feydy-2011-half-reif} in the original paper on \gls{half-reif}.
@ -292,6 +292,6 @@ The data and original model are available at:
\begin{listing}
\mznfile{assets/listing/qcp_max.mzn}
\caption{\label{lst:bench-qcpmax} A \minizinc{} model for the QCP-Max problem}
\caption{\label{lst:bench-qcpmax} A \minizinc{} model for the QCP-Max problem.}
\end{listing}