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

Fix some final formatting issues

Browse Source
This commit is contained in:
Jip J. Dekker 2021-11-08 13:03:08 +11:00
parent 6d4481b843
commit b36d49292b
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
8 changed files with 46 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
assets/listing/back_queens.mzn Normal file
View File

@ -0,0 +1,8 @@
int: n;
set of int: ROW = 1..n;
set of int: COL = 1..n;
array [COL] of var ROW: q;
constraint all_different(q);
constraint all_different([q[i] + i | i in COL]);
constraint all_different([q[i] - i | i in COL]);

5
assets/listing/half_impli.mzn
View File

@ -1,5 +0,0 @@
predicate impli(
var bool: x ::promise_ctx_antitone,
var bool: y ::promise_ctx_monotone
) =
not x \/ y;

2
assets/packages.tex
View File

@ -116,7 +116,7 @@
cachedir=listings,
outputdir=latex.out,
]{minted}
\usemintedstyle{borland}
\usemintedstyle{tango}
\usepackage[many]{tcolorbox}
\newtcolorbox{listingbox}[1][]{

8
assets/table/half_mznc.tex
View File

@ -2,16 +2,16 @@
\toprule
\multicolumn{2}{c}{Solver} & \multicolumn{2}{c}{Unsatisfiable} & \multicolumn{2}{c}{Optimal Solution} & Satisfied & Unk. & Err. \\
\midrule
\gls{gecode} & (Full) & 1 & (573.39s) & 49 & (218.12s) & 80 & 70 & 0 \\
\gls{gecode} & (Half) & 1 & (574.69s) & 48 & (201.29s) & 81 & 70 & 0 \\
\gls{gecode} & (Full) & 1 & (573.39s) & 49 & (218.12s) & 80 & 70 & 0 \\
\midrule
\gls{cplex} & (Full) & 2 & (5.35s) & 76 & (141.45s) & 63 & 48 & 11 \\
\gls{cplex} & (Half) & 1 & (3.24s) & 81 & (178.08s) & 60 & 45 & 13 \\
\gls{cplex} & (Full) & 2 & (5.35s) & 76 & (141.45s) & 63 & 48 & 11 \\
\midrule
\gls{cbc} & (Full) & 2 & (11.94s) & 41 & (131.76s) & 131 & 16 & 10 \\
\gls{cbc} & (Half) & 2 & (7.01s) & 35 & (135.93s) & 135 & 17 & 11 \\
\gls{cbc} & (Full) & 2 & (11.94s) & 41 & (131.76s) & 131 & 16 & 10 \\
\midrule
OpenWBO & (Full) & 16 & (20.44s) & 48 & (156.01s) & 51 & 32 & 53 \\
OpenWBO & (Half) & 16 & (19.61s) & 51 & (187.73s) & 47 & 33 & 53 \\
OpenWBO & (Full) & 16 & (20.44s) & 48 & (156.01s) & 51 & 32 & 53 \\
\bottomrule
\end{tabular}

20
chapters/2_background.tex
View File

@ -231,8 +231,8 @@ A function is declared using the syntax \mzninline{function @\(T\)@: @\(I\)@(@\(
\begin{itemize}
\item \(T\) is the type of its result;
\item \(I\) is its identifier;
\item \(P\) is a list types and identifiers for its arguments;
\item and \(E\) is the body of the function, an expression that can use the arguments \(P\).
\item \(P\) is a list types and identifiers for its arguments; and
\item \(E\) is the body of the function, an expression that can use the arguments \(P\).
\end{itemize}
\noindent{}\Gls{rewriting} replaces a call to a function by its body instantiated with the arguments given in the call.
@ -608,18 +608,12 @@ They allow modellers to always use \glspl{global} and depending on the \solver{}
As an example of the \gls{propagation} mechanism, let us consider the N-Queens problem.
Given a chessboard of size \(n \times n\), find a placement for \(n\) queen chess pieces such that the queens cannot attack each other.
This means we can only place one queen per row, one queen per column, and one queen per diagonal.
The problem can be modelled in \minizinc{} as follows.
A \minizinc{} model for this problem is shown in \cref{lst:back-queens-mzn}.
\begin{mzn}
int: n;
set of int: ROW = 1..n;
set of int: COL = 1..n;
array [COL] of var ROW: q;
constraint all_different(q);
constraint all_different([q[i] + i | i in COL]);
constraint all_different([q[i] - i | i in COL]);
\end{mzn}
\begin{listing}
\mznfile{assets/listing/back_queens.mzn}
\caption{\label{lst:back-queens-mzn}A \minizinc{} model for the N-Queens problem.}
\end{listing}
The \variables{} in the \gls{array} \mzninline{q} decide for each column in which row the queen is placed.
This restricts every column to only have a single queen.

13
chapters/3_rewriting.tex
View File

@ -674,7 +674,6 @@ For example, a \cmodel{} targeted at a \gls{mip} \solver{} is rewritten into Boo
The \nanozinc{} program can then be fully simplified by \gls{propagation}, before the Boolean and reified \constraints{} are rewritten into \gls{native} linear \constraints{} suitable for \gls{mip}.
\begin{example}
Let us revisit the example from \cref{subsec:back-delayed-rew}.
The following \minizinc{} fragment calls a predicate that uses the ``Big M method''.
@ -706,7 +705,6 @@ The \nanozinc{} program can then be fully simplified by \gls{propagation}, befor
\end{nzn}
Because the evaluation of \mzninline{lq_zero_if_b} is delayed until after the domain changes of \mzninline{x} it can instead produce \mzninline{int_lin_le([1, 100], [x,b], 100)}.
\end{example}
\subsection{Common Sub-expression Elimination}%
@ -857,13 +855,13 @@ Times are averages of 1000 runs.
The results of the experiment are shown in \cref{fig:rew-interpreter-comp}.
For all experiments there is a clear ordering in the results:
\begin{itemize}
\item OCaml is the clear winner,
\item our prototype finishes in second place,
\item Python is a close third,
\item and finally \minizinc{} 2.5.5.
\item OCaml is the clear winner, always at least five times faster than its closest competitor;
\item our prototype finishes in second place;
\item Python is a close third, with only a significant difference compared to our prototype on the Ackermann bencmark; and
\item \minizinc{} 2.5.5 always finishes last out of the four interpreters with significant overhead over all other competitors.
\end{itemize}
Our prototype performs well in this test.
It clearly outperforms \minizinc{} 2.5.5 with about 10 times speed-up, and it slightly outperforms Python, an optimized \interpreter{} for a general programming language.
It clearly outperforms \minizinc{} 2.5.5 with about ten times speed-up, and it slightly outperforms Python, an optimized \interpreter{} for a general programming language.
It is clear though that OCaml, a language that is dedicated to these types of programs, still outperforms our prototype.
We are convinced, however, that we can get closer to its performance given the right improvements in our prototype.
@ -874,6 +872,7 @@ We are convinced, however, that we can get closer to its performance given the r
on recursive functions: Takeuchi, Fibonacci, and Ackermann.}
\end{figure}
\pagebreak{}
\section{Summary}%
\label{sec:rew-summary}

32
chapters/4_half_reif.tex
View File

@ -13,9 +13,9 @@
\label{sec:half-intro}
The complex expression language used in \cmls{}, such as \minizinc{}, often requires the use of \gls{reif} in order to arrive at a \gls{slv-mod}.
If the Boolean expression \mzninline{pred(...)} is seen in a non-\rootc{} context, then a new Boolean \variable{} \mzninline{b} is introduced to replace the expression.
If the Boolean expression \mzninline{pred(@...@)} is seen in a non-\rootc{} context, then a new Boolean \variable{} \mzninline{b} is introduced to replace the expression.
We call \mzninline{b} the \gls{cvar} of the expression.
The \gls{rewriting} process then enforces a \constraint{} \mzninline{pred_reif(...,b)}, which binds the \variable{} to be the truth-value of the expression (i.e., \mzninline{b <-> pred(...)}).
The \gls{rewriting} process then enforces a \constraint{} \mzninline{pred_reif(@...@,b)}, which binds the \variable{} to be the truth-value of the expression (i.e., \mzninline{b <-> pred(@...@)}).
\textcite{feydy-2011-half-reif} show that although using \gls{reif} in the \gls{rewriting} process is well-understood, it suffers from certain weaknesses.
@ -25,7 +25,7 @@ The \gls{rewriting} process then enforces a \constraint{} \mzninline{pred_reif(.
\end{itemize}
As an alternative, the authors introduce \gls{half-reif}.
It follows from the idea that in many cases it is \gls{eqsat} to use the logical implication of an expression, \mzninline{b -> pred(...)}, instead of the logical equivalence, \mzninline{b <-> pred(...)}.
It follows from the idea that in many cases it is \gls{eqsat} to use the logical implication of an expression, \mzninline{b -> pred(@...@)}, instead of the logical equivalence, \mzninline{b <-> pred(@...@)}.
\Gls{rewriting} with \gls{half-reif} is an approach that improves upon these weaknesses of \gls{rewriting} with ``full'' \gls{reif}.
\begin{itemize}
@ -43,6 +43,7 @@ Therefore, it can be used in these cases as it is guaranteed that if \(e\) repre
Note that when the right-hand side of an implication \(b \implies{} e\) is \true{}, it also does not influence the left-hand side.
A possible downside of \gls{half-reif} is thus that its \gls{cvar} might need to be assigned by a \gls{search-decision}.
\pagebreak{}
\begin{example}
\label{ex:hr-disjunction}
@ -240,10 +241,10 @@ This can be advantageous, but has a corresponding disadvantage.
When a \gls{cvar} is \gls{fixed}, it can allow the simplification of the \glspl{propagator} that use them, and hence make \gls{propagation} faster.
When a full \gls{reif} is required, we can still use \gls{half-reified} \glspl{propagator} to implement it.
A full \gls{reif} \mzninline{x <-> pred(...)} can be propagated using its \gls{half-reified} \gls{propagator}, \mzninline{x -> pred(...)}, the \gls{half-reified} \gls{propagator} of its negation, \mzninline{y -> not pred(...)}, and the \constraint{} \mzninline{x <-> not y}.
A full \gls{reif} \mzninline{x <-> pred(@...@)} can be propagated using its \gls{half-reified} \gls{propagator}, \mzninline{x -> pred(@...@)}, the \gls{half-reified} \gls{propagator} of its negation, \mzninline{y -> not pred(@...@)}, and the \constraint{} \mzninline{x <-> not y}.
This does not lose \gls{propagation} strength.
For Booleans appearing in \posc{} context we can make the \gls{propagator} of the negated \gls{half-reif} run at the lowest priority, since it will never detect if the state is \gls{unsat}.
Similarly, in \negc{} context we can make the \gls{propagator} \mzninline{b -> pred(...)} run at the lowest priority.
Similarly, in \negc{} context we can make the \gls{propagator} \mzninline{b -> pred(@...@)} run at the lowest priority.
This means that the \glspl{cvar} are still \gls{fixed} at the same time, but there is less overhead.
In \cref{sec:half-experiments} we assess \glspl{propagator} implementations for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element} based on these principles.
@ -454,14 +455,17 @@ It may be possible to infer these \glspl{annotation} from the function body.
However, we currently do not provide such analysis and annotate functions by hand.
\begin{example}
Consider the user-defined \minizinc{} implementation of a logical implication in \cref{lst:half-impli}.
Consider the following user-defined \minizinc{} implementation of a logical implication.
\begin{mzn}
predicate impli(
var bool: x ::promise_ctx_antitone,
var bool: y ::promise_ctx_monotone
) =
not x \/ y;
\end{mzn}
The \glspl{annotation} placed on the argument of the \mzninline{impli} function will apply the same context transformations as the \mzninline{->} \gls{operator} shown in \cref{alg:arg-ctx}.
In terms of context analysis, this function now is equivalent to the \minizinc{} \gls{operator}.
\end{example}
\begin{listing}
\mznfile{assets/listing/half_impli.mzn}
\caption{\label{lst:half-impli} A user-defined predicate of a logical implication using \glspl{annotation} to define the context usage of its arguments.}
\end{listing}
\begin{algorithm}
\KwIn{A \minizinc{} \gls{operator} \(op\) and calling context \(ctx\)}
@ -472,16 +476,16 @@ However, we currently do not provide such analysis and annotate functions by han
\Case{\mzninline{ not }}{
\Return{\tuple{\changeneg{}ctx}}
}
\Case{\mzninline{ \/ }, \mzninline{+ }}{
\Case{\mzninline{ \/}, \mzninline{+ }}{
\Return{\tuple{\changepos{}ctx, \changepos{}ctx}}
}
\Case{\mzninline{ -> }, \mzninline{< }, \mzninline{<= }}{
\Case{\mzninline{ ->}, \mzninline{<}, \mzninline{<= }}{
\Return{\tuple{\changeneg{}ctx, \changepos{}ctx}}
}
\Case{\mzninline{ > }, \mzninline{>= }, \mzninline{- }}{
\Case{\mzninline{ >}, \mzninline{>=}, \mzninline{- }}{
\Return{\tuple{\changepos{}ctx, \changeneg{}ctx}}
}
\Case{\mzninline{ <-> }, \mzninline{= }, \mzninline{xor }, \mzninline{* }}{
\Case{\mzninline{ <->}, \mzninline{=}, \mzninline{xor}, \mzninline{* }}{
\Return{\tuple{\mixc, \mixc}}
}
\Case{\mzninline{ /\ }}{

3
chapters/5_incremental.tex
View File

@ -261,7 +261,7 @@ This will activate a different \gls{neighbourhood} for each subsequent \gls{rest
\end{listing}
For adaptive \gls{lns}, a simple strategy is to change the size of the \gls{neighbourhood} depending on whether the previous size was successful or not.
\Cref{lst:inc-adaptive} shows an adaptive version of the \mzninline{uniform_neighbourhood} that increases the number of free \variables{} when the previous \gls{restart} failed, and decreases it when it succeeded, within the range \([0.6,0.95]\).
\Cref{lst:inc-adaptive} shows an adaptive version of the \mzninline{uniform_neighbourhood} that increases the number of free \variables{} when the previous \gls{restart} failed, and decreases it when it succeeded, within the range \mzninline{0.6..0.95}.
\begin{listing}[p]
\mznfile{assets/listing/inc_adaptive.mzn}
@ -829,6 +829,7 @@ It is surprising to see that the application of 1000 \glspl{neighbourhood} using
The solving times are similar between all methods and once again, we do not see any real advantage of the use of the incremental \solver{} \glsxtrshort{api}.
The advantage in solve time using \gls{rbmo} is more pronounced here, but it is hard to draw conclusions since the \glspl{neighbourhood} of this method are not exactly the same.
\pagebreak{}
\section{Summary}
This chapter presented two novel methods that strive towards eliminating the overhead of \cmls{} for the use of \gls{meta-optimization}.