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

Guido's abstract / intro notes

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-28 13:53:53 +10:00
parent fe0234b009
commit 4562bb685d
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
2 changed files with 28 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
chapters/0_abstract.tex
View File

@ -2,7 +2,7 @@
\chapter{Abstract}\label{ch:abstract} \chapter{Abstract}\label{ch:abstract}
%************************************************ %************************************************
\vspace{-8em} \vspace{-5em}
\noindent{}\Cmls{} are a prominent way to model and solve real world problems. \noindent{}\Cmls{} are a prominent way to model and solve real world problems.
They are used in areas such as scheduling, supply chain management, and transportation, among many others. They are used in areas such as scheduling, supply chain management, and transportation, among many others.
@ -27,8 +27,8 @@ The architecture is extended using a range of well-known simplification techniqu
In addition, we incorporate new analysis techniques to avoid the use of \glspl{reif} or replace them with \glspl{half-reif}, where possible. In addition, we incorporate new analysis techniques to avoid the use of \glspl{reif} or replace them with \glspl{half-reif}, where possible.
The architecture is designed to incorporate incremental \constraint{} modelling in two ways. The architecture is designed to incorporate incremental \constraint{} modelling in two ways.
Primarily, the \gls{rewriting} process is fully incremental: changes made to the \instance{} through a provided interface require minimal addition \gls{rewriting} effort. Primarily, the \gls{rewriting} process is fully incremental: changes made to the \instance{} through a provided interface require minimal additional \gls{rewriting} effort.
Moreover, we introduce \gls{rbmo}, a way to specify \gls{meta-optimization} algorithms directly in \minizinc{}. Moreover, we introduce \gls{rbmo}, a way to specify \gls{meta-optimization} algorithms directly in \minizinc{}.
These specifications are executed by a normal \minizinc{} \solver{}, requiring only a slight extension of its capabilities. These specifications are executed directly by a \minizinc{} \solver{}, using a simple extension.
Together, the functionality of this architecture helps to make \cmls{} a more powerful and attractive approach to solve real world problems. Together, the functionality of this architecture helps to make constraint modelling a more powerful and attractive approach to solve real world problems.

48
chapters/1_introduction.tex
View File

@ -4,7 +4,7 @@
\noindent{}A \gls{dec-prb} is any problem that requires us to make decisions according to a set of rules. \noindent{}A \gls{dec-prb} is any problem that requires us to make decisions according to a set of rules.
Many important and difficult problems in the real world are \glspl{dec-prb}. Many important and difficult problems in the real world are \glspl{dec-prb}.
We can think, for instance, about the decision on the country's rail timetable or the stand-by locations for ambulances in the region. We can think, for instance, about the decisions on the country's rail timetable or the stand-by locations for ambulances in the region.
Formally, we define a \gls{dec-prb} as a set of \variables{} subject to a set of logical \constraints{}. Formally, we define a \gls{dec-prb} as a set of \variables{} subject to a set of logical \constraints{}.
A \gls{sol} to such a problem is the \gls{assignment} of all \variables{} to values that abide by the logic of the \constraints{}. A \gls{sol} to such a problem is the \gls{assignment} of all \variables{} to values that abide by the logic of the \constraints{}.
These problems are also highly computationally complex: even with the fastest computers, finding a solution can take a long time. These problems are also highly computationally complex: even with the fastest computers, finding a solution can take a long time.
@ -16,20 +16,19 @@ Famous classes of decision and \glspl{opt-prb}, such as \gls{sat} \autocite{bier
And, over the years, highly specialized \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. 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. Encoding one problem in terms of another is, however, a difficult task.
The problem classes can be restrictive: the input to the \solver{}, the \gls{slv-mod}, can only contain \gls{native} \variables{} and \constraints{}, meaning those that are directly supported by the \solver{}. The problem classes can be restrictive: the input to the \solver{}, the \gls{slv-mod}, can only contain \gls{native} \variables{} and \constraints{}, meaning those that are directly supported by the \solver{}.
Furthermore, \constraints{} can only refer to \variables{}, they cannot be (directly) dependent on other \constraints{}. Furthermore, \constraints{} can only refer to \variables{}, they cannot be (directly) dependent on other \constraints{}.
For example, \gls{sat} \solvers{} can only reason about Boolean \variables{}, deciding if something is true or false. For example, \gls{sat} \solvers{} can only reason about Boolean \variables{}, deciding if something is true or false.
\Constraints{} for \gls{sat} \solvers{} have to be in the form of disjunctions of Boolean \variables{}, or their negations. \Constraints{} for \gls{sat} \solvers{} have to be in the form of disjunctions of Boolean \variables{}, or their negations.
But, not only does the encoding have to be correct, the encoding also has to be performant. But, not only does the encoding have to be correct, the encoding also has to be performant.
There are often many possible correct encodings of a problem, but there can be a significant difference in how quickly the \solver{} finds a \gls{sol} for them. There are often many possible correct encodings of a problem, but there can be a significant difference in how quickly the \solver{} finds a \gls{sol} for them and the preferred encoding can differ between \solvers{}.
The preferred encoding can however differ between \solvers{}.
Two \solvers{} designed to solve the same problem class can perform very differently. Two \solvers{} designed to solve the same problem class can perform very differently.
\Cmls{} have been designed to tackle these issues. \Cmls{} have been designed to tackle these issues.
They serve as a level of abstraction between the modeller and the \solver{}. They serve as a level of abstraction between the modeller and the \solver{}.
The typical process of a \cml{} is visualized in \cref{fig:intro-cml-flow}. The typical process of using a \cml{} is visualized in \cref{fig:intro-cml-flow}.
Instead of providing a flat list of \variables{} and \constraints{}, a modeller creates a \cmodel{} using the more natural syntax of the \cml{}. Instead of providing a flat list of \variables{} and \constraints{}, a modeller creates a \cmodel{} using the more natural syntax of the \cml{}.
A \cmodel{} can generally describe a class of problems through the use of \prbpars{}: values assigned by external input. A \cmodel{} can generally describe a class of problems through the use of \prbpars{}: values assigned by external input.
Once given a complete \gls{assignment} of the \prbpars{}, the \cmodel{} forms an \instance{}. Once given a complete \gls{assignment} of the \prbpars{}, the \cmodel{} forms an \instance{}.
@ -42,23 +41,23 @@ The \gls{rewriting} process of a \cml{} transforms a \cmodel{} into a \gls{slv-m
\end{figure} \end{figure}
Traditional \cmls{}, such as \emph{\glsxtrshort{ampl}} \autocite{fourer-2003-ampl}, \gls{essence} \autocite{frisch-2007-essence}, and \emph{\glsxtrshort{opl}} \autocite{van-hentenryck-1999-opl}, offer the modeller an expressive language that can be used to target a great variety of \solvers{}. Traditional \cmls{}, such as \emph{\glsxtrshort{ampl}} \autocite{fourer-2003-ampl}, \gls{essence} \autocite{frisch-2007-essence}, and \emph{\glsxtrshort{opl}} \autocite{van-hentenryck-1999-opl}, offer the modeller an expressive language that can be used to target a great variety of \solvers{}.
However, these language lack a certain level of flexibility: the modeller is unable to capture common concepts used throughout a \cmodel{}, and the \solver{} cannot influence their way in which the problem is encoded. However, these languages lack a certain level of flexibility: the modeller is unable to capture common concepts used throughout a \cmodel{}, and the \solver{} cannot influence their way in which the problem is encoded.
This is a stark difference to \gls{clp} languages, such as \gls{sicstus} \autocite{carlsson-1997-sicstus}, which are said to be the precursors to \cmls{}. This is a stark difference to \gls{clp} languages, such as \gls{sicstus} \autocite{carlsson-1997-sicstus}, which are said to be the precursors to \cmls{}.
In these languages, the modeller is encouraged to create high-level concepts and declare the way in which they are rewritten into \gls{native} \constraints{}. In these languages, the modeller is encouraged to express high-level concepts by defining custom predicates and functions and declare the way in which they are rewritten into \gls{native} \constraints{}.
The downside of \gls{clp} languages is that, because of its search mechanism, the \solver{} is tightly integrated within the \gls{rewriting}. The downside of \gls{clp} languages is that, because of its search mechanism, the \solver{} is tightly integrated within the \gls{rewriting}.
These languages thus lack the \solver{}-independence of \cmls{}. These languages thus lack the \solver{}-independence of \cmls{}.
\minizinc{} \autocite{nethercote-2007-minizinc} is a functional \cml{} that operates on a level in between these two types of languages. \minizinc{} \autocite{nethercote-2007-minizinc} is a functional \cml{} that operates on a level in between these two types of languages.
Like a traditional \cml{}, it is a \solver{}-independent \cml{}. Like a traditional \cml{}, it is \solver{}-independent.
Like a \gls{clp} language, modellers can declare and reuse common concepts and control the encoding into the \gls{slv-mod} through the use of function definitions. Like a \gls{clp} language, modellers can declare and reuse common concepts and control the encoding into the \gls{slv-mod} through the use of function definitions.
Fundamentally, in its \gls{rewriting} process \minizinc{} is a functional language. Fundamentally, in its \gls{rewriting} process \minizinc{} is a functional programming language.
It continuously evaluates the calls in a \minizinc{} \instance{} until it reaches \gls{native} \constraints{}. It continuously evaluates the calls in a \minizinc{} \instance{} until it reaches \gls{native} \constraints{}.
Like other functional languages, \minizinc{} allows recursion; it can be used as a fully Turing complete programming language. Like other functional languages, \minizinc{} allows recursion; it can be used as a fully Turing complete programming language.
Although \minizinc{} is based on this powerful paradigm, its success has made certain problems apparent. Although \minizinc{} is based on this powerful paradigm, its success has made certain problems apparent.
The language was originally designed to target \gls{cp} \solvers{}, where the \glspl{slv-mod} typically contain a few highly complex \constraints{}. The language was originally designed to target \gls{cp} \solvers{}, where the \glspl{slv-mod} typically contain only 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. Its use has however, over time, extended to rewrite for \gls{mip} and \gls{sat} \solvers{}, whose \glspl{slv-mod} often contain numerous \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{}. 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}. Unlike \gls{clp} \gls{rewriting}, the \minizinc{} \gls{rewriting} process does not consider incremental changes to its \gls{slv-mod}.
@ -68,7 +67,7 @@ The overhead of \gls{rewriting} all these \instances{} separately can be substan
In this thesis we revisit the \gls{rewriting} of functional \cmls{} into \glspl{slv-mod}. In this thesis we revisit the \gls{rewriting} of functional \cmls{} into \glspl{slv-mod}.
We design and evaluate an architecture for \cmls{} that can accommodate the modern uses of these languages. We design and evaluate an architecture for \cmls{} that can accommodate the modern uses of these languages.
\section{Constraint Modelling Varieties} \section{Different Ways of Modelling with Constraints}
Let us now study the different ways of constraint modelling in more detail, starting with one of the most commonly used \cmls{}: \glsxtrshort{ampl}. Let us now study the different ways of constraint modelling in more detail, starting with one of the most commonly used \cmls{}: \glsxtrshort{ampl}.
@ -91,7 +90,7 @@ As an \gls{opt-prb}, our goal is to find a schedule that minimizes the finishing
In order of occurrence, \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 modeller provides the number of jobs and machines that are considered, and the duration of each task. To create an \instance{} of the problem, the modeller 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. \Lrefrange{line:intro:var:start}{line:intro:var:end} show the \variable{} declarations: for each task we decide on its start time.
We also declare the end time of the last task as a \variable{}, to ease the modelling of the problem. We also declare the end time of the last task as a \variable{}, to make it easier to model the \gls{objective}.
This \variable{} is made to be our optimization 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. Finally, \lrefrange{line:intro:con:start}{line:intro:con:end} express the \constraints{} of our problem in terms of equations bound by logic.
@ -133,7 +132,7 @@ For example, the concepts of one task preceding another and non-overlapping of t
The definition of \texttt{non\_overlap} requires that either task A precedes task B, or vice versa. The definition of \texttt{non\_overlap} requires that either task A precedes task B, or vice versa.
However, unlike the \glsxtrshort{ampl} model, Prolog would not provide this choice to the \solver{}. However, unlike the \glsxtrshort{ampl} model, Prolog would not provide this choice to the \solver{}.
Instead, it enforces one, test if this works, and it otherwise enforces the other. Instead, it enforces one, tests if this works, and it otherwise enforces the other.
This is a powerful mechanism where choices are made in the \gls{rewriting} process, and not in the \solver{}. This is a powerful mechanism where choices are made in the \gls{rewriting} process, and not in the \solver{}.
The problem with the mechanism is that it requires a highly incremental interface with the \solver{} that can incrementally post and retract \constraints{}. The problem with the mechanism is that it requires a highly incremental interface with the \solver{} that can incrementally post and retract \constraints{}.
@ -161,14 +160,15 @@ For example, a modeller could create the following \minizinc{} function to expre
\minizinc{} also determines how an \instance{} is encoded for a \solver{} through function definitions. \minizinc{} also determines how an \instance{} is encoded for a \solver{} through function definitions.
All functionality in the \minizinc{} language is eventually expressed using function calls. All functionality in the \minizinc{} language is eventually expressed using function calls.
The \solver{}, then, has the decision to choose if this call is a \gls{native} \constraint{}, or how this call is rewritten. The \solver{}, then, has the decision to choose if this call is a \gls{native} \constraint{}, or how this call is rewritten.
For example, the logical \mzninline{or}-operator, which was only supported for \gls{cp} \solvers{} in \glsxtrshort{ampl}, could be defined for \gls{mip} solvers in \minizinc{} using the following definition. Each \solver{} supplies its own library of \minizinc{} function definitions for common \constraints{}.
For example, the logical \mzninline{or}-operator, which was only supported for \gls{cp} \solvers{} in \glsxtrshort{ampl}, could be defined in the \minizinc{} library for a \gls{mip} \solver{} using the following definition.
\begin{mzn} \begin{mzn}
predicate bool_or(var bool: x, var bool: y) = predicate bool_or(var bool: x, var bool: y) =
x + y >= 1; x + y >= 1;
\end{mzn} \end{mzn}
\noindent{}Whereas the following definition would mark it as a \gls{native} \constraint{} for a \gls{cp} \solver{}, by not defining a body. \noindent{}Whereas, the \minizinc{} library of a \gls{cp} \solver{} could include the following definition to mark it as a \gls{native} \constraint{}, by not defining a body.
\begin{mzn} \begin{mzn}
predicate bool_or(var bool: x, var bool: y); predicate bool_or(var bool: x, var bool: y);
@ -177,7 +177,7 @@ For example, the logical \mzninline{or}-operator, which was only supported for \
The functional paradigm employed by \minizinc{} has shown itself to be powerful and flexible for the modeller and \solver{} The functional paradigm employed by \minizinc{} has shown itself to be powerful and flexible for the modeller and \solver{}
However, the performance of the functional evaluation of the language can be a limiting factor. However, the performance of the functional evaluation of the language can be a limiting factor.
\section{The Problems of Rewriting MiniZinc} \section{Why Rewriting MiniZinc is Difficult}
A \minizinc{} model generally consists of a few loops or \glspl{comprehension}; for a \gls{cp} solver, this would be rewritten into a relatively small set of \constraints{} which would be fed whole into the solver. A \minizinc{} model generally consists of a few loops or \glspl{comprehension}; 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 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. 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.
@ -204,7 +204,7 @@ In particular:
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{}. 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: an 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. It is possible, however, that further \gls{rewriting} can reveal a \gls{reif} to be unnecessary.
Currently, the current \minizinc{} implementation cannot reverse any \gls{reif} decisions once they are made. 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. 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. \item Monolithic \gls{rewriting} is wasteful.
@ -218,9 +218,9 @@ In particular:
\section{Research Aims and Contributions} \section{Research Aims and Contributions}
Research into \gls{rewriting} of \cmls{}, as well as model transformation in general, has shown that it is difficult to achieve both high performance and generality. Research into \gls{rewriting} of \cmls{}, as well as model transformation in general, 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 optimization 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 required to produce high-quality \gls{slv-mod}.
In order to adapt \cmls{} for modern day requirements, this thesis aims to \textbf{design, implement, and evaluate a modern architecture for functional \cmls{}}. 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: Crucially, this architecture will allow us to:
\begin{itemize} \begin{itemize}
@ -258,7 +258,7 @@ Overall, this thesis makes the following contributions.
This thesis is arranged into the following chapters. This thesis is arranged into the following chapters.
Succeeding this introductory chapter, \emph{\cref{ch:background}} gives an overview of the area of \cmls{}. \emph{\Cref{ch:background}} gives an overview of the area of \cmls{}.
It introduces the reader to \minizinc{}, how its models are formulated and how they are translated to \glspl{slv-mod}. It introduces the reader to \minizinc{}, how its models are formulated and how they are translated to \glspl{slv-mod}.
Then, we review different solving methods such as \gls{sat}, \gls{mip}, and \gls{cp}. 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 is followed by a comparison of \minizinc{} with other \cmls{}.
@ -276,15 +276,15 @@ We compare the performance of an implementation of the presented architecture ag
\emph{\Cref{ch:half-reif}} continues on the path of improving \glspl{slv-mod}. \emph{\Cref{ch:half-reif}} continues on the path of improving \glspl{slv-mod}.
In this chapter, we present a formal analysis technique to reason about \gls{reif}. In this chapter, we present a formal analysis technique to reason about \gls{reif}.
This analysis can help us decide whether a \constraint{} has to be reified. This analysis can help us decide whether a \constraint{} has to be reified.
In addition, the analysis allows us to determine whether we use \gls{half-reif}. In addition, the analysis allows us to determine whether to use \gls{half-reif}.
We thus present the first implementation of automatic \gls{half-reif}. We thus present the first implementation of automatic \gls{half-reif}.
We conclude this chapter by analysing the impact of \gls{half-reif} for different types of \solvers{}. We conclude this chapter by analysing the impact of \gls{half-reif} for different types of \solvers{}.
\emph{\Cref{ch:incremental}} focuses on the development of incremental methods for \cmls{}. \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}. We first present a novel technique that eliminates the need for incremental \gls{rewriting}.
Instead, it integrates a \gls{meta-optimization} specification, written in the \minizinc{} language, into the \gls{slv-mod}. Instead, it integrates a \gls{meta-optimization} specification, written in the \minizinc{} language, into the \gls{slv-mod}.
Then, we describe a technique to optimize 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 prevents the repeated \gls{rewriting} for parts of the \instance{} that remain unchanged. This method prevents the repeated \gls{rewriting} of parts of the \instance{} that remain unchanged.
We conclude this chapter by testing the performance and computational overhead of these two techniques. 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. Finally, \emph{\Cref{ch:conclusions}} is the concluding chapter of the thesis.