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

Add first real version of the introduction

Browse Source
This commit is contained in:
Jip J. Dekker 2021-06-19 17:11:53 +10:00
parent e3dcae4d29
commit 15b1a63e77
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
3 changed files with 121 additions and 145 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
assets/acronyms.tex
View File

@ -36,6 +36,8 @@
\newacronym{np}{NP}{Nondeterministic Polynomial-time}
\newacronym{or}{OR}{Operational Research}
\newacronym[see={[Glossary:]{gls-opl}}]{opl}{OPL\glsadd{gls-opl}}{The Optimisation Programming Language}
\newacronym{ram}{RAM}{Random Access Memory}

1
assets/shorthands.tex
View File

@ -6,6 +6,7 @@
\newcommand{\ie}{i.e.,\xspace{}}
% Glossary entries
\newcommand{\Cmls}{\Gls{constraint-modelling} languages\xspace{}}
\newcommand{\cmls}{\gls{constraint-modelling} languages\xspace{}}
\newcommand{\cml}{\gls{constraint-modelling} language\xspace{}}
\newcommand{\constraints}{\glspl{constraint}\xspace{}}

263
chapters/1_introduction.tex
View File

@ -2,62 +2,69 @@
\chapter{Introduction}\label{ch:introduction}
%************************************************
\noindent{}Operation decision problems are some of the hardest computational problems. Even with the fastest computer it requires
\noindent{}Every day we face a abundance of decisions. Although many
\noindent{} Many problems can be described as making a number of decisions according to a set of rules, or \constraints{}.
These \emph{decision problems} are some of the hardest computational problems.
Even with the fastest computer there is no simple way to, for example, decide on the schedule for a country's train system or the stand-by locations for the ambulances in the region.
These kinds of problems get even more complex when we consider \emph{optimisation problems}: if there are multiple solution, one might be preferred over the other.
But, although these problems might be hard to solve, finding a (good) solution for these problems is essential in many walks of life.
I can first talk about \emph{decision problems}, which are complex.
We can think about making a national train schedule or deciding which delivery truck delivers which package.
These problem are complex as their decisions are highly interconnected.
They get harder when we consider that one solution might be reasons to prefer one solution over another.
\emph{Optimisation problems} extends decision problems with an objective function to be maximised or minimised.
The field of \gls{or} uses advanced computational methods to help make (better) decisions.
And, although some problems require the creation of specialised algorithms, more often than not problems are solved by reducing them to another problem.
There are famous problems, like \gls{sat} \autocite{biere-2021-sat} and \gls{mip} \autocite{wolsey-1988-mip}, for which over the years highly specialised \solvers{} have been created to find solutions.
Because of universality of these problems and the effectiveness of their \solvers{}, formulating a new problem in terms of on of these famous problems is often the best way to find a solution.
This reformulation process presents various challenges:
\emph{Operational Research} is the field of study that concerns itself with solving these kinds of problems using computational \jip{models}.
\gls{sat} proves if a logical formula is unsatisfiable, or gives a valid assignment.
For a set of linear equations, \gls{mip} can find an solution that op
There are techniques such as \gls{sat}, which solves a set of Boolean and \gls{mip}. In ea
\jip{Traditionally ...}
The process of solving the problem can be said to consists of three stages.
First, the operational expert to understand the problem itself and create a formal specification, or \emph{model} of the problem.
This is generally referred to as modelling the problem.
The model is then translated into a solver-level \emph{program}.
The solver then solves the program.
\jip{Yeah nah!}
So what is the model exactly?
That depends.
There is a trade-off between the level at which you model, and the level at which you solve.
\gls{sat} and \gls{mip} solvers operate at a low level and
We introduce \minizinc{}, a high-l
High-level \cmls{}, like \minizinc{}, were originally designed as a convenient input language for \gls{cp} solvers \autocite{marriott-1998-clp}.
A user would write a model consisting of a few loops or comprehensions; given a data file for the parameters, this would be rewritten into a relatively small set of constraints which would be fed whole into the solver.
The existing process for translating \minizinc\ into solver-specific constraints 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 translation) were small, translation was fast, and the expected results of translation were obvious.
The current architecture is illustrated in \Cref{sfig:4-oldarch}.
But over time, the uses of high-level \cmls{} have expanded greatly from this original vision.
It is now used to generate input for wildly different solver technologies: not just \gls{cp}, but also \gls{mip} \autocite{wolsey-1988-mip}, \gls{sat} \autocite{davis-1962-dpll} and \gls{cbls} \autocite{bjordal-2015-fzn2oscarcbls} solvers.
Crucially, the same constraint model can be used with any of these solvers, which is achieved through the use of solver-specific libraries of constraint definitions.
In \minizinc{}, these solver libraries are written in the same language.
As such, \minizinc\ turned out to be much more expressive than expected, so more and more preprocessing and model transformation has been added to both the core \minizinc\ library, and users' models.
And in addition to one-shot solving, \minizinc\ is frequently used as the basis of a larger meta-optimisation tool chain: programmatically generating a model, solving it, then using the results to generate another slightly different model.
\jip{Overview preamble}
\jip{
\begin{itemize}
\item Topic and significance
\item Broad known (current literature) and problem - broad
\item Major aim of the thesis
\item The problem likely reasons at a different level than the targeted \solver{}.
For example, expressing the rules of a train schedule in term of Boolean logic (for a \gls{sat} \solver{}) is a complicated process.
\item There are many possible formulations of the problem, but there is a significant difference in how quickly in how quickly it can be solved.
\item All \solvers{} are different. Even when two \solvers{} are designed to solve the same problem set, they might perform substantially better when specific formulations are used or support slight extensions of the original problem set.
\end{itemize}
}
\section{Motivation}
\Cmls{}, like \gls{ampl} \autocite{fourer-2003-ampl}, \gls{opl} \autocite{van-hentenryck-1999-opl}, \minizinc{} \autocite{nethercote-2007-minizinc}, and \gls{essence} \autocite{frisch-2007-essence}, have been designed to tackle these problems.
They define a common language that can be used between different \solvers{}.
So instead of defining the problem for a \solver{}, the user creates formalises the problem in the \cml{}, creating a \emph{model} of the problem.
The language is then tasked with creating an optimised formulation for the targeted \solver{}.
Some of these language even allow the modeller to use common patterns, \glspl{global}, that are not directly supported by the solver.
These \emph{High-level} languages will then \emph{decompose} these \glspl{global} into an efficient structure for the targeted solver.
The usage of \cmls{}, especially high-level languages, can simplify the process and reduce the amount of expert knowledge that is required about the \solver{}.
The problem, however, is that high-level \cmls{} were originally designed to target \gls{cp} problems.
Extraordinarily, instances of \gls{cp} problems can directly include many of the \glspl{global} available in the language.
This meant that only little effort was required to rewrite a model for the targeted solver.
But over time these languages have expanded greatly from this original vision.
They are now used to generate input for wildly different solver technologies: not just \gls{cp}, but also \gls{mip} and \gls{sat}.
Crucially, for these \solver{} types the same \glspl{global} have to be replaced by much bigger structures in the problem specification.
This means more and more processing and model transformation has been required to rewrite models into a specification for the targeted \solver{}.
Furthermore, new meta-optimisation techniques are becoming increasingly prominent.
Instead of creating a single model that describes the full problem, these techniques programmatically generate a model, solve it, and then using the results generate another slightly different model.
This results in the rewriting of an abundance of related models in quick succession As such, the rewriting process has become an obstacle for both sizable models and models that require incremental changes.
In this thesis we revisit the rewriting of high-level \cmls\ into \solver{}-level problem specifications.
It is our aim to design and test an architecture for \cmls{} that can accommodate the modern uses of these languages.
\section{MiniZinc}
One of the most prominent high-level \cmls{} is \minizinc{}.
In this thesis, we choose \minizinc{} as the primary \cml{} for several reasons.
First, the \minizinc{} language is one of the most extensive \cmls{}.
It contains features such as annotations and user-defined functions, not found in other \cmls{}.
This means that, despite the usage of \minizinc{}, the methods explored in this thesis would still be applicable to other \cmls{}.
Second, because of the popularity and maturity of the language, there is a large suite of models available that can be used as benchmarks.
Third, the language has been used in multiple studies as a host for meta-optimisation techniques \autocite{ingmar-2020-diverse,ek-2020-online}.
Finally, many of the researchers involved in the design and implementation of \minizinc{} have settled at Monash University.
People with the expertise to answer complex questions about the language were therefore close at hand.
Once designed as a standard for different \gls{cp} solvers, \minizinc{} exhibits many of the earlier described problems.
A \minizinc{} model generally consists of a few loops or comprehensions; for a \gls{cp} solver, this would be rewritten into a relatively small set of constraints which would be fed whole into the solver.
The existing process for translating \minizinc{} into solver-specific constraints 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 translation) were small.
Now, the language is also used to target \solvers{} for low-level problems, such as \gls{sat} and \gls{mip}, and is used as part of various 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:
@ -66,7 +73,7 @@ In particular:
\item The \minizinc\ compiler is inefficient.
It does a surprisingly large amount of work for each expression (especially resolving sub-typing and overloading), which may be repeated many times --- for example, inside the body of a comprehension.
And as models generated for other solver technologies (particularly \gls{mip}) can be quite large, the resulting flattening procedure can be intolerably slow.
And as models generated for other solver technologies can be quite large, the resulting flattening procedure can be intolerably slow.
As the model transformations implemented in \minizinc\ become more sophisticated, these performance problems are simply magnified.
\item The generated models often contain unnecessary constraints.
@ -74,132 +81,98 @@ In particular:
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 Monolithic flattening is wasteful.
When \minizinc\ is used for multi-shot solving, there is typically a large base model common to all sub-problems, and a small set of constraints which are added or removed in each iteration.
But with the existing \minizinc\ architecture, the whole model must be re-flattened each time.
When \minizinc\ is used as part of a meta-optimisation toolchain, there is typically a large base model common to all sub-problems, and a small set of constraints which are added or removed in each iteration.
But with the existing \minizinc\ architecture, the whole model must be rewritten each time.
Many use cases involve generating a base model, then repeatedly adding or removing a few constraints before re-solving.
In the current tool chain, the whole model must be fully re-flattened each time.
Not only does this repeat all the work done to flatten the base model, This means a large (sometimes dominant) portion of runtime is simply flattening the core model over and over again.
But it also prevents \emph{the solver} from carrying over anything it learnt from one problem to the next, closely related, problem.
In the current tool chain, the whole model must be fully rewritten to a \solver{} specification each time.
Not only does this repeat all the work done to rewrite the base model, This means a large (sometimes dominant) portion of runtime is simply rewriting the core model over and over again.
But it also prevents the \solver{} from carrying over anything it learnt from one problem to the next, closely related, problem.
\end{itemize}
\jip{
\begin{itemize}
\item Known (self - current literature)
\item Problem statement specific - scope of your study
\end{itemize}
}
In addition, Feydy et al.\ once argued for the usage of \gls{half-reif} in \gls{cp} solvers and \cmls{} \autocite*{feydy-2011-half-reif}.
Where a \gls{reification} is a technique to reason about the truth-value of a \constraint{}, as an improvement \gls{half-reif} reasons only about the logical implication of this value.
The authors even show how, for a subset of \minizinc{}, \gls{half-reif} could automatically be introduced as an alternative to \gls{reification}.
Although it is shown that \gls{half-reif} can lead to significant improvements, automatically introducing \gls{half-reif} was never used in rewriting \minizinc{} models.
In part, because the method presented for the subset of \minizinc{} did not extend to the full language.
\section{Research Objective and Contributions}
\section{Aims /RQs /ROs}
Research on the rewriting of \cmls{} has long focused on the improvement of the \solver{} specification.
For each of these improvements it can be shown that they are highly effective when used.
It is well-known that the optimisation of the \solver{} specification can lead to profound reductions in solving time.
But while each optimisation might only trigger in a fraction of models, in implementation eagerly searching for applicable optimisations can take a significant amount of time.
% All things considered, these individual
In this thesis, we revisit the rewriting of high-level \cmls\ into solver-level constraint models and describe an architecture that allows us to:
We address these issues by instead of considering optimisations individually, reconsider the rewriting process overall.
In order to adapt high-level \cmls{} for its modern day requirements, this thesis aims to \textbf{design, implement, and evaluate a modern architecture for high-level \cmls{}}.
Crucially, this architecture should allow us to:
\begin{itemize}
\item easily integrate a range of \textbf{optimisation and simplification} techniques,
\item easily integrate a range of well-known and new \textbf{optimisation and simplification} techniques,
\item effectively \textbf{detect and eliminate dead code} introduced by functional definitions, and
\item effectively manage the \solver{} specification and \textbf{detect and eliminate} parts of models that have become unused, and
\item support \textbf{incremental flattening and solving}, and better integration with solvers providing native incremental features.
\item support \textbf{incremental usage} of the \cml{} infrastructure.
\end{itemize}
The goal of my research is to design a compiler architecture for high-level constraint modelling languages that improves on the capabilities of these languages for modern applications of these languages.
In particular, I have investigated the architecture of compilers for constraints modelling languages and how they can incorporate various optimisations and simplifications, how the generation of solver-level constraint models, like MIP and SAT, can be sped up without compromising the quality of the model, and how we can minimize the work required in the generation of solver-level constraint models when incrementally making changes to the high-level constraint model.
In my candidature I have therefore answered the following research questions.
In the design of this architecture, we start analysing the rewriting process from the ground up.
We first determine the foundation for the system: an execution model for the basic rewriting system.
To ensure the quality of the produced \solver{} specifications, we extend the system with many well-known optimisation techniques.
In addition, we experiment with several new approaches to optimise the resulting \solver{} specification, including the use of \gls{half-reif}.
Crucially, we ensure that the system is integrates well within meta-optimisation toolchains and experiment with several meta-optimisation applications.
\begin{center}
\textbf{Question 1: Can we formulate a formal execution model for the
\minizinc\ language?}
\end{center}
Overall, this thesis makes the following contributions:
I have developed a formal execution model for the \minizinc\ language.
This execution model allows us to describe exactly what a compiler or interpreter of the \minizinc\ language has to do to arrive at a valid set of solver-level constraints.
The use of the formal model offers insight into both the generation process and the opportunities for simplifications and optimisations.
Using this formal model I was able to produce a prototype \minizinc\ tool chain that significantly improved the generation time of solver-level constraint models while maintaining the same quality.
Additionally, the new tool chain is able to simplify certain patterns of constraints that the current \minizinc\ tool chain is unable to simplify.
Although this execution model has been developed for \minizinc\ in particular, the execution model can be applied to other constraint modelling languages with relative ease as their features can likely be expressed in terms of features in the \minizinc\ language.
\begin{enumerate}
\begin{center}
\textbf{Question 2: How can we design and implement a procedure that
correctly introduces half-reified constraints during the compilation of
constraint modelling languages?}
\end{center}
\item It presents a formal execution model of rewriting of the \minizinc\ language and extends this model with well-known optimisation and simplification techniques.
The ideas behind half-reification~\cite{feydy-2011-half-reif}, where the implication of a constraint is used instead of the truth value (i.e., reification) of a constraint, is almost 10 years old.
There was, however, no concrete procedure for the automatic generation of half-reified constraints instead of fully reified constraint when they are equivalent to the use.
During my candidature I have designed and implemented this procedure and it has been included in both the current version of the \minizinc\ compiler and our prototype tool chain.
As an additional optimisation, I have developed an algorithm to find and eliminate chains of implications, which are often introduced when using half-reified constraints.
Initial results show significant translation improvements when using MIP solvers and CP solvers with dedicated half-reified propagators.
\item It provides a novel method of tracking of \constraints{} created as part of functional dependencies, ensuring it can be correctly removed when it is no longer required.
\begin{center}
\textbf{Question 3: How can we efficiently re-solve a high-level constraint
model with slight changes?}
\end{center}
\item It presents a design and implementation of techniques to automatically introduce \gls{half-reif} of constraints in \minizinc{}.
Within the new prototype tool chain for \minizinc\ we have designed a new scheme to efficiently allow users to apply changes to their high-level constraint models.
In this scheme the state of the constraint model can be thought of as a stack data structure.
Additional constraints and variables can be added to the ``end'' of the model and the user is able to remove the last added variable or constraint, but the user can never remove constraint and variables from the ``beginning'' or ``middle'' of the model.
This allows us to trace (and undo) any side effects that occurred during the generation process.
For some solvers, these stack-like changes can be directly reflected in the solver without the need to re-initialise the solver.
I have therefore defined several levels of incremental protocols for solver interfaces, depending on whether the solver allows for any changes to its internal model, and if so, which kind of changes are allowed.
My experiments show that applying meta-search algorithms using this mechanism is a massive improvement over previous approaches, which would run the full \minizinc\ to solver translation and reinitialize the solver for every change.
\item It develops a technique to simplify problem specifications by efficiently eliminating implication chains.
\begin{center}
\textbf{Question 4: Can meta-searches be compiled into a solver-level
constraint model with minimal changes to the solver?}
\end{center}
I found that in some cases even the minimal interaction with a solver to apply a meta-search incurs a significant overhead.
In addition, I found that using minimal additions to the solver we could apply the same meta-search using its internal search algorithms.
Hence, I have defined a set of intrinsics that allows users to define a meta-search from within a constraint modelling language.
These intrinsic features are translated to a minimal set of features that have to be implemented within the solver.
I show that this search language is expressive enough to implement search algorithms like \textit{branch-and-bound}, \textit{lexicographic search}, and \textit{large neighbourhood search}.
Experiments show that this approach eliminates the significant overhead of recompilation and that there is a benefit of using meta-searches, like large neighbourhood search, for some constraint models.
\jip{
\begin{itemize}
\item (description and Method?? )
\end{itemize}
}
\section{Contributions}
\jip{overview (details in the conclusion)(publications?)}
As the importance of computers continues to grow in this age of automation, so does the importance of operational research and optimisation.
Constraint modelling languages are one of the techniques that make optimisation accessible to beginning practitioners, but even optimisation experts often use these languages as they allow them to create prototypes quickly and model complex problems with ease.
It is therefore a very worthwhile pursuit to contribute to the field of optimisation and constraint modelling languages.
During my candidature I have made the following contributions the field of optimisation and constraint modelling languages:
\begin{itemize}
\item A formal execution model of the \minizinc\ language.
\item A design for a compiler architecture for constraint modelling languages that is designed for the modern uses of high-level constraint languages, including the low-level solver targets and the incremental adjustments of models.
\item The design and implementation of automatic half-reification of constraints within compilers for constraint modelling languages.
\item An efficient algorithm to eliminate implication chains within constraint models.
\item Designs of solver instructing protocols for different levels of incremental changes to the problem definition.
\item Prototype implementation for all above mentioned designs for the \minizinc\ tool chain.
\end{itemize}
\item It proposes two methods novel methods to reduce the required overhead of use \cmls in meta-optimisation techniques: \emph{restart-based} meta-search and the \emph{incremental} rewriting of changing models.
\end{enumerate}
\section{Organisation of the Thesis}
This thesis is partitioned into the following chapters.
Following this introductory chapter, \emph{\cref{ch:background}} presents the background information \ldots{}.
Following this introductory chapter, \emph{\cref{ch:background}} reviews relevant information in the area of \cmls{}.
First, it introduces the reader to \minizinc{}, how its models are formulated, and how they are translated to \solver{} specifications.
Then, we review different solving methods method 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 \solver{} specifications it produces.
\emph{\Cref{ch:rewriting}}
\emph{\Cref{ch:rewriting}} presents a formal execution model for \minizinc{} and the core of our new architecture.
We introduce \microzinc{}, a minimal language to which \minizinc{} can be reduced.
We use this language to construct formal rewriting rules.
The product of applying these rules is in terms of \nanozinc{}, an abstract \solver{} specification language.
Crucially, we show how \nanozinc{} tracks the \constraints{} that define the variable such that functional definitions can correctly be removed.
This chapter also integrates well-known techniques used to simplify the \solver{} specification into the architecture.
We compare the performance of an implementation of the presented architecture against the existing \minizinc{} infrastructure.
\emph{\Cref{ch:half-reif}}
\emph{\Cref{ch:half-reif}} continues on the path of creating better \solver{} specifications.
In this chapter, we present the first implementation of the usage of automatic \gls{half-reif}.
We consider the effects of using \gls{half-reif} both inside a \gls{cp} solver and as part of a decomposition.
We then describe a new analysis to determine when \gls{half-reif} can be used.
This extends an earlier approach that does not extend to the full \minizinc{} language.
We also comment on the influence that \gls{half-reif} has on other techniques used in the rewriting process.
We conclude this chapter by analysing performance changes incurred by the usage of this technique on both small and large scale.
\emph{\Cref{ch:incremental}}
\emph{\Cref{ch:incremental}} focuses on the use of meta-optimisation methods.
We introduce two methods that can be employed to describe and employ these technique.
We first present a novel technique that considers a meta-search specification in a \minizinc{} and compiles it into the \solver{} specification.
Then, we describe a method to optimise the rewriting process for incremental changes to a model.
This method ensures that no work is done for parts of the model that remain unchanged.
We conclude this chapter by testing the performance and computational overhead of these two techniques.
Finally, \emph{\Cref{ch:conclusions}} is the concluding chapter of the thesis.
It reiterates the discoveries and contributions of this research to theory and practice, comments on the scope and limitations of the presented system, and presents further avenues for research in this area.
\jip{ Chapter overview – including main focus, (and method??)}