206 lines
14 KiB
TeX
206 lines
14 KiB
TeX
%************************************************
|
||
\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
|
||
|
||
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.
|
||
|
||
\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
|
||
\end{itemize}
|
||
}
|
||
|
||
\section{Motivation}
|
||
|
||
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:
|
||
|
||
\begin{itemize}
|
||
|
||
\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.
|
||
As the model transformations implemented in \minizinc\ become more sophisticated, these performance problems are simply magnified.
|
||
|
||
\item The generated models often contain unnecessary constraints.
|
||
During the transformation, 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 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.
|
||
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.
|
||
|
||
\end{itemize}
|
||
|
||
\jip{
|
||
\begin{itemize}
|
||
\item Known (self - current literature)
|
||
\item Problem statement specific - scope of your study
|
||
\end{itemize}
|
||
}
|
||
|
||
|
||
\section{Aims /RQs /ROs}
|
||
|
||
In this thesis, we revisit the rewriting of high-level \cmls\ into solver-level constraint models and describe an architecture that allows us to:
|
||
|
||
\begin{itemize}
|
||
|
||
\item easily integrate a range of \textbf{optimisation and simplification} techniques,
|
||
|
||
\item effectively \textbf{detect and eliminate dead code} introduced by functional definitions, and
|
||
|
||
\item support \textbf{incremental flattening and solving}, and better integration with solvers providing native incremental features.
|
||
|
||
\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.
|
||
|
||
\begin{center}
|
||
\textbf{Question 1: Can we formulate a formal execution model for the
|
||
\minizinc\ language?}
|
||
\end{center}
|
||
|
||
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{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}
|
||
|
||
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.
|
||
|
||
\begin{center}
|
||
\textbf{Question 3: How can we efficiently re-solve a high-level constraint
|
||
model with slight changes?}
|
||
\end{center}
|
||
|
||
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.
|
||
|
||
\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}
|
||
|
||
|
||
\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{}.
|
||
|
||
\emph{\Cref{ch:rewriting}}
|
||
|
||
\emph{\Cref{ch:half-reif}}
|
||
|
||
\emph{\Cref{ch:incremental}}
|
||
|
||
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??)}
|