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

Start at introduction transition

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-27 21:56:54 +10:00
parent fb24a5dc25
commit 1041eda4c7
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
3 changed files with 43 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

0
assets/img/back_cml_flow.pdf → assets/img/intro_cml_flow.pdf
View File

62
chapters/1_introduction.tex
View File

@ -28,14 +28,50 @@ 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 user and the \solver{}. They serve as a level of abstraction between the modeller and the \solver{}.
Instead of providing a flat list of \variables{} and \constraints{}, the user can create 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{}.
The \instance{} is transformed into a \gls{slv-mod} through a process called \gls{rewriting}. Central to the process of a \cml{}, the \instance{} is transformed, through \gls{rewriting}, into a \gls{slv-mod}, an encoding of the problem that can be used by the \solver{}.
This process is visualized in \cref{fig:intro-cml-flow}.
A commonly used \cml{} is \glsxtrshort{ampl} \autocite{fourer-2003-ampl}. \begin{figure}
\glsxtrshort{ampl} was originally designed as a common interface between different \gls{mip} \solvers{}. \centering
\includegraphics[width=\columnwidth]{assets/img/intro_cml_flow}
\caption{\label{fig:intro-cml-flow}A flow diagram of typical process of a \cml{}.}
\end{figure}
Traditional \cmls{}, such as \glsxtrshort{ampl} \autocite{fourer-2003-ampl}, \gls{essence} \autocite{frisch-2007-essence}, and \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.
This is a stark different to \gls{clp} languages, such Sictus Prolog \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{}.
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{}.
\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{}.
And like a \gls{clp} language, modellers can declare 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.
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.
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{}.
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 weakness 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}.
We design and evaluate an architecture for \cmls{} that can accommodate the modern uses of these languages.
\section{Constraint Modelling}
\glsxtrshort{ampl} is a commonly used \cml{}.
It was originally designed as a common interface between different \gls{mip} \solvers{}.
The language provides a natural way to define numeric \variables{} and express \constraints{} in the form of linear (in-)equations as described by the class of problem. The language provides a natural way to define numeric \variables{} and express \constraints{} in the form of linear (in-)equations as described by the class of problem.
The same \glsxtrshort{ampl} model can then be used between different \solvers{}. The same \glsxtrshort{ampl} model can then be used between different \solvers{}.
@ -52,7 +88,7 @@ As an \gls{opt-prb}, our goal is to find a schedule that minimizes the finishing
\Cref{lst:intro-open-shop} shows an \glsxtrshort{ampl} model for the open shop problem. \Cref{lst:intro-open-shop} shows an \glsxtrshort{ampl} model for the open shop problem.
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 user 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 ease the modelling of the problem.
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}.
@ -108,7 +144,7 @@ As such, a \gls{clp} program is not \solver{}-independent.
Like \glsxtrshort{ampl}, it is a \solver{}-independent \cml{}. Like \glsxtrshort{ampl}, it is a \solver{}-independent \cml{}.
And like \gls{clp} languages, modellers can declare common concepts and control the encoding into the \gls{slv-mod}. And like \gls{clp} languages, modellers can declare common concepts and control the encoding into the \gls{slv-mod}.
The latter is accomplished through the use of function definitions. The latter is accomplished through the use of function definitions.
For example, a user could create the following \minizinc{} function to express the non-overlapping relation. For example, a modeller could create the following \minizinc{} function to express the non-overlapping relation.
\begin{mzn} \begin{mzn}
function var bool: non_overlap( function var bool: non_overlap(
@ -140,18 +176,6 @@ predicate bool_or(var bool: x, var bool: y) =
predicate bool_or(var bool: x, var bool: y); predicate bool_or(var bool: x, var bool: y);
\end{mzn} \end{mzn}
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{}.
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 weakness 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}.
We design and evaluate an architecture for \cmls{} that can accommodate the modern uses of these languages.
\section{The Problems of Rewriting MiniZinc} \section{The Problems of Rewriting MiniZinc}
\minizinc{} is one of the most prominent \cmls{}. \minizinc{} is one of the most prominent \cmls{}.

7
chapters/2_background.tex
View File

@ -34,13 +34,6 @@ In this case the goal is to find a \gls{sol} that satisfies all \constraints{} w
Although a \cmodel{} does not contain any instructions on how to find a suitable \gls{sol}, \instances{} of \cmodels{} can generally be given to a dedicated \solver{}. Although a \cmodel{} does not contain any instructions on how to find a suitable \gls{sol}, \instances{} of \cmodels{} can generally be given to a dedicated \solver{}.
To solve these \instances{}, however, they can go through a \gls{rewriting} process to arrive at a \gls{slv-mod}, input accepted by a \solver{}. To solve these \instances{}, however, they can go through a \gls{rewriting} process to arrive at a \gls{slv-mod}, input accepted by a \solver{}.
The \solver{} then uses a dedicated algorithm that finds a \gls{sol} that fits the requirements of the \instance{}. The \solver{} then uses a dedicated algorithm that finds a \gls{sol} that fits the requirements of the \instance{}.
This process is visualized in \cref{fig:back-cml-flow}.
\begin{figure}
\centering
\includegraphics[width=\columnwidth]{assets/img/back_cml_flow}
\caption{\label{fig:back-cml-flow}A flow diagram of typical process of a \cml{}.}
\end{figure}
\begin{example}% \begin{example}%
\label{ex:back-knapsack} \label{ex:back-knapsack}