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

Grammar check of the introduction

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-24 11:35:43 +10:00
parent f6d869885b
commit b6a54d384b
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
1 changed files with 22 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
chapters/1_introduction.tex
View File

@ -13,7 +13,7 @@ But, although these problems are hard to solve, finding a (good) solution for th
The field of \gls{or} uses advanced computational methods to help make (better) decisions.
Famous classes of decision and \glspl{opt-prb}, such as \gls{sat} \autocite{biere-2021-sat}, \gls{cp} \autocite{rossi-2006-cp} and \gls{mip} \autocite{wolsey-1988-mip}, have been studied extensively.
And, over the years, highly specialised \solvers{} have been created to find \glspl{sol} for these classes of problems.
And, over the years, highly specialized \solvers{} have been created to find \glspl{sol} for these classes of problems.
Nowadays, most decision and \glspl{opt-prb} are solved by encoding them into one of the above-mentioned classes of problems.
Encoding one problem in terms of another is, however, a difficult problem.
@ -43,23 +43,23 @@ Crucially, the same \glsxtrshort{ampl} model can be used between different \solv
As such, additional types of \constraints{} for these problem classes have been added to the language, removing the restriction that \constraints{} must be linear (in-)equations.
Let us introduce the \glsxtrshort{ampl} language by modelling the ``open shop problem''.
In the open shop problem, the goal is to schedule jobs with multiple tasks..
In the open shop problem, the goal is to schedule jobs with multiple tasks.
Each task must be performed by an assigned machine.
A machine can only perform one task at the same time.
And, only one task of the same job can be scheduled at the same time.
We assume that each job has a task for every machine.
As an \gls{opt-prb}, our goal is to find a schedule that minimises the finishing time of the last task.
As an \gls{opt-prb}, our goal is to find a schedule that minimizes the finishing time of the last task.
\Cref{lst:intro-open-shop} shows an \glsxtrshort{ampl} model for the open shop problem.
In order of occurence, \lrefrange{line:intro:param:start}{line:intro:param:end} show the declarations of the \prbpars{}.
In order of occurrence, \lrefrange{line:intro:param:start}{line:intro:param:end} show the declarations of the \prbpars{}.
To create an \instance{} of the problem, the user provides the number of jobs and machines that are considered, and the duration of each task.
\Lrefrange{line:intro:var:start}{line:intro:var:end} show the \variable{} declarations: for each task we decide on its start time.
Additionally, we declare the end time of the last task as a \variable{}, to ease the modelling of the problem.
This \variable{} is made to be our optimisation goal on \lref{line:intro:goal}.
This \variable{} is made to be our optimization goal on \lref{line:intro:goal}.
Finally, \lrefrange{line:intro:con:start}{line:intro:con:end} express the \constraints{} of our problem in terms of equations bound by logic.
\begin{listing}
\pyfile{assets/listing/intro_open_shop.mod}
\amplfile{assets/listing/intro_open_shop.mod}
\caption{\label{lst:intro-open-shop} An \glsxtrshort{ampl} model of the open shop problem}
\end{listing}
@ -142,12 +142,12 @@ predicate bool_or(var bool: x, var bool: y);
\end{mzn}
Although \minizinc{} is based on this powerful paradigm, its success has surfaced certain problems.
The language was originally designed to target \gls{cp} \solvers{}, where the \glspl{slv-mod} typically contain a small number of highly complex \constraints{}.
The language was originally designed to target \gls{cp} \solvers{}, where the \glspl{slv-mod} typically contain a few highly complex \constraints{}.
Its use has extended to rewrite for \gls{mip} and \gls{sat} \solvers{}, whose \glspl{slv-mod} often contain large numbers \variables{} and simple \constraints{}, generated by a complex library of \minizinc{} functions.
For many applications, \minizinc{} now requires a significant, and sometimes prohibitive, amount of time to rewrite \instances{}.
Unlike \gls{clp} \gls{rewriting}, the \minizinc{} \gls{rewriting} process does not consider incremental changes to its \gls{slv-mod}.
This is another weakness that has become particularly important, since new optimisation methods require the solving of a sequence of closely related \instances{}.
This is another weakness that has become particularly important, since new optimization methods require the solving of a sequence of closely related \instances{}.
The overhead of \gls{rewriting} all these \instances{} separately can be substantial.
In this thesis we revisit the \gls{rewriting} of functional \cmls{} into \glspl{slv-mod}.
@ -165,8 +165,8 @@ A \minizinc{} model generally consists of a few loops or \glspl{comprehension};
The existing process for translating \minizinc{} into a \gls{slv-mod} is a somewhat ad-hoc, (mostly) single-pass, recursive unrolling procedure, and many aspects (such as call overloading) are resolved dynamically.
In its original application, this was acceptable: models (both before and after \gls{rewriting}) were small.
Now, the language is also used to target low-level \solvers{}, such as \gls{sat} and \gls{mip}.
For them, the encoding of the same \minizinc{} \instance{} results in a much larger \glspl{slv-mod}.
Additionally, \minizinc{} is used more and more as part of various \gls{meta-optimisation} toolchains.
For them, the encoding of the same \minizinc{} \instance{} results in a much larger \gls{slv-mod}.
Additionally, \minizinc{} is used in progressively more \gls{meta-optimisation} toolchains.
To a great extent, this is testament to the effectiveness of the language.
However, as they have become more common, these extended uses have revealed weaknesses of the existing \minizinc{} tool chain.
In particular:
@ -182,11 +182,11 @@ In particular:
During \gls{rewriting}, functional expressions are replaced with \constraints{}.
But this breaks the functional dependencies: if the original expression later becomes redundant (due to model simplifications), \minizinc{} may fail to detect that the constraint can be removed.
\item The reasoning about \gls{reif} in the \minizinc{} \compiler{} is limited.
\item The reasoning about \gls{reif} in \minizinc{} is limited.
An important decision that is made during \gls{rewriting} is if a \constraint{} can be enforced directly or if it is dependent on other \constraints{}.
In the second case, a \gls{reif} has to be introduced, a often costly form of the \constraint{} that determines whether a \constraint{} holds rather than enforcing the \constraint{} itself.
In the second case, a \gls{reif} has to be introduced, an often costly form of the \constraint{} that determines whether a \constraint{} holds rather than enforcing the \constraint{} itself.
It is possible, however, that further \gls{rewriting} can reveal a \gls{reif} to be unnecessary.
Currently, the \compiler{} cannot reverse any \gls{reif} decisions once they are made.
Currently, the current \minizinc{} implementation cannot reverse any \gls{reif} decisions once they are made.
And, it also does not consider \gls{half-reif}, a cheaper alternative to \gls{reif} that is often applicable.
\item Monolithic \gls{rewriting} is wasteful.
@ -202,13 +202,13 @@ In particular:
\section{Research Objective and Contributions}
Research into \gls{rewriting} of \cmls{}, as well as model transformation more generally, has shown that it is difficult to achieve both high performance and generality.
We address these issues by reconsidering the rewriting process from the ground up to make the transformation efficient while accommodating the optimisation techniques to achieve the expected result.
We address these issues by reconsidering the rewriting process from the ground up to make the transformation efficient while accommodating the optimization techniques to achieve the expected result.
In order to adapt \cmls{} for modern day requirements, this thesis aims to \textbf{design, implement, and evaluate a modern architecture for functional \cmls{}}.
Crucially, this architecture should allow us to:
\begin{itemize}
\item easily integrate a range of well-known and new \textbf{optimisation and simplification} techniques,
\item easily integrate a range of well-known and new \textbf{optimization and simplification} techniques,
\item effectively manage the \gls{slv-mod} and \textbf{detect and eliminate} parts of the model that have become unused,
@ -221,18 +221,18 @@ Crucially, this architecture should allow us to:
In the design of this architecture, we analyse the \gls{rewriting} process from the ground up.
We first determine the foundation for the system: an execution model for the basic \gls{rewriting} system.
To ensure the quality of the produced \glspl{slv-mod}, we extend the system with many well-known simplification techniques.
In addition, we experiment with several new approaches to optimise the resulting \glspl{slv-mod}, including the use of \gls{half-reif}.
In addition, we experiment with several new approaches to optimize the resulting \glspl{slv-mod}, including the use of \gls{half-reif}.
Crucially, we ensure that the resulting system is fully incremental, and we experiment with several \gls{meta-optimisation} applications to evaluate this.
Overall, this thesis makes the following contributions:
Overall, this thesis makes the following contributions.
\begin{enumerate}
\item It presents a formal execution model of rewriting of the \minizinc\ language and extends this model with well-known optimisation and simplification techniques.
\item It presents a formal execution model of rewriting of the \minizinc\ language and extends this model with well-known optimization and simplification techniques.
\item It provides a novel method of tracking of \constraints{} created as part of functional dependencies, ensuring the correct removal of dependencies no longer required.
\item It presents an analysis technique to reason about in what (\gls{reified}) form a \constraints{} should be considered.
\item It presents an analysis technique to reason about in what (\gls{reified}) form \constraints{} should be considered.
\item It presents a design and implementation of techniques to automatically introduce \gls{half-reif} of \constraints{} in \minizinc{}.
@ -242,7 +242,7 @@ Overall, this thesis makes the following contributions:
\end{enumerate}
\section{Organisation of the Thesis}
\section{Organization of the Thesis}
This thesis is arranged into the following chapters.
@ -251,7 +251,7 @@ First, it introduces the reader to \minizinc{}, how its models are formulated, a
Then, we review different solving methods such as \gls{sat}, \gls{mip}, and \gls{cp}.
This is followed by a comparison of \minizinc{} with other \cmls{}.
This chapter also reviews techniques that are closely related to \cmls{}.
We conclude this chapter with a description of the current \minizinc{} compiler and the techniques it uses to simplify the \glspl{slv-mod} it produces.
We conclude this chapter with a description of the current \minizinc{} implementation and the techniques it uses to simplify the \glspl{slv-mod} it produces.
\emph{\Cref{ch:rewriting}} presents a formal execution model for \minizinc{} and the core of our new architecture.
We construct a set of formal rewriting rules for a subset of \minizinc{} called \microzinc{}.
@ -271,7 +271,7 @@ We conclude this chapter by analysing the impact of the usage of \gls{half-reif}
\emph{\Cref{ch:incremental}} focuses on the development of incremental methods for \cmls{}.
We first present a novel technique that eliminates the need for the incremental \gls{rewriting}.
Instead, it integrates a meta-optimisation specification, written in the \minizinc{} language, into the \gls{slv-mod}.
Then, we describe a technique to optimise the \gls{rewriting} process for incremental changes to an \instance{}.
Then, we describe a technique to optimize the \gls{rewriting} process for incremental changes to an \instance{}.
This method ensures that no work is done for parts of the \instance{} that remain unchanged.
We conclude this chapter by testing the performance and computational overhead of these two techniques.