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

Editing with Cait

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-27 20:52:25 +10:00
parent a0b85fda42
commit 3389133fc9
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
3 changed files with 27 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

53
chapters/1_introduction.tex
View File

@ -37,7 +37,7 @@ The \instance{} is transformed into a \gls{slv-mod} through a process called \gl
A commonly used \cml{} is \glsxtrshort{ampl} \autocite{fourer-2003-ampl}. A commonly used \cml{} is \glsxtrshort{ampl} \autocite{fourer-2003-ampl}.
\glsxtrshort{ampl} was originally designed as a common interface between different \gls{mip} \solvers{}. \glsxtrshort{ampl} 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.
Crucially, the same \glsxtrshort{ampl} model can be used between different \solvers{}. The same \glsxtrshort{ampl} model can then be used between different \solvers{}.
\glsxtrshort{ampl} was later extended to include other \solver{} targets, including \gls{cp} and quadratic \solvers{}. \glsxtrshort{ampl} was later extended to include other \solver{} targets, including \gls{cp} and quadratic \solvers{}.
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. 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.
@ -45,7 +45,7 @@ As such, additional types of \constraints{} for these problem classes have been
Let us introduce the \glsxtrshort{ampl} language by modelling the ``open shop'' problem. 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. Each task must be performed by an assigned machine.
A machine can only perform one task at the same time. A machine can only perform one task at any one time.
And, only one task of the same job can be scheduled 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. We assume that each job has a task for every machine.
As an \gls{opt-prb}, our goal is to find a schedule that minimizes 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.
@ -54,7 +54,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 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 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. \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. 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}.
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.
@ -65,7 +65,7 @@ Finally, \lrefrange{line:intro:con:start}{line:intro:con:end} express the \const
The \glsxtrshort{ampl} model provides a clear definition of the problem class, but it can be argued that its meaning is hard to decipher. The \glsxtrshort{ampl} model provides a clear definition of the problem class, but it can be argued that its meaning is hard to decipher.
\glsxtrshort{ampl} does not provide any way to capture common concepts, such as one task preceding another or that two tasks cannot overlap in our example. \glsxtrshort{ampl} does not provide any way to capture common concepts, such as one task preceding another or that two tasks cannot overlap in our example.
Additionally, the process to encode an \instance{} into a \gls{slv-mod} all happens ``behind the scenes''. Moreover, the process to encode an \instance{} into a \gls{slv-mod} all happens ``behind the scenes''.
The \solver{} cannot specify how, for example, an operator is best rewritten. The \solver{} cannot specify how, for example, an operator is best rewritten.
As such, \glsxtrshort{ampl} cannot rewrite all models for all its \solvers{}. As such, \glsxtrshort{ampl} cannot rewrite all models for all its \solvers{}.
For example, since the model in \cref{lst:intro-open-shop} uses the \mzninline{or} operator, it can only be encoded for \solvers{} that support \glsxtrshort{ampl}'s \gls{cp} interface. For example, since the model in \cref{lst:intro-open-shop} uses the \mzninline{or} operator, it can only be encoded for \solvers{} that support \glsxtrshort{ampl}'s \gls{cp} interface.
@ -100,7 +100,7 @@ Instead, it enforces one, test if this works, and it otherwise enforces the othe
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{}.
Additionally, \solvers{} are not always able to verify if a certain set of \constraints{} is consistent. \Solvers{} are also not always able to verify if a certain set of \constraints{} is consistent.
This makes the behaviour of the \gls{clp} program dependent on the \solver{} that is used. This makes the behaviour of the \gls{clp} program dependent on the \solver{} that is used.
As such, a \gls{clp} program is not \solver{}-independent. As such, a \gls{clp} program is not \solver{}-independent.
@ -118,12 +118,11 @@ For example, a user could create the following \minizinc{} function to express t
startA + durA < startB \/ startB + durB < startA; startA + durA < startB \/ startB + durB < startA;
\end{mzn} \end{mzn}
\noindent{}Because functions that return the truth value of an expression are common when constructing \constraints{}, \minizinc{} supports the ``\mzninline{predicate}'' keyword as equivalent to the ``\mzninline{function var bool:}'' syntax. \noindent{}Since functions that return the truth value of an expression are common when constructing \constraints{}, \minizinc{} supports the ``\mzninline{predicate}'' keyword as equivalent to the ``\mzninline{function var bool:}'' syntax.
Fundamentally, in its \gls{rewriting} process \minizinc{} is a functional language. 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{}. It continuously evaluates the calls in a \minizinc{} \instance{} until it reaches \gls{native} \constraints{}.
Like other functional languages, \minizinc{} allows recursion. Like other functional languages, \minizinc{} allows recursion; it can be used as a fully Turing complete programming language.
It can be used as a fully Turing complete programming language.
Using the same mechanism, \minizinc{} defines how an \instance{} is encoded for a \solver{}. Using the same mechanism, \minizinc{} defines how an \instance{} is encoded for a \solver{}.
All functionality in the \minizinc{} language is eventually expressed using function calls. All functionality in the \minizinc{} language is eventually expressed using function calls.
@ -147,7 +146,7 @@ Its use has extended to rewrite for \gls{mip} and \gls{sat} \solvers{}, whose \g
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}.
This is another weakness that has become particularly important, since new optimization methods require the solving of a sequence of closely related \instances{}. 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. 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}. In this thesis we revisit the \gls{rewriting} of functional \cmls{} into \glspl{slv-mod}.
@ -158,7 +157,7 @@ We design and evaluate an architecture for \cmls{} that can accommodate the mode
\minizinc{} is one of the most prominent \cmls{}. \minizinc{} is one of the most prominent \cmls{}.
It is an expressive language that, in addition to user-defined functions, gives modellers access to advanced features, such as many types of \variables{}, \glspl{annotation}, and an extensive standard library of \constraints{}. It is an expressive language that, in addition to user-defined functions, gives modellers access to advanced features, such as many types of \variables{}, \glspl{annotation}, and an extensive standard library of \constraints{}.
All of these can be used with all \solver{} targets. All of these can be used with all \solver{} targets.
Because of the popularity and maturity of the language, there is a large suite of \minizinc{} models available that can be used as benchmarks. As a result of the popularity and maturity of the language, there is a large suite of \minizinc{} models available that can be used as benchmarks.
The language has also been used in multiple studies as a host for meta-optimization techniques \autocite{ingmar-2020-diverse,ek-2020-online}. The language has also been used in multiple studies as a host for meta-optimization techniques \autocite{ingmar-2020-diverse,ek-2020-online}.
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.
@ -184,24 +183,22 @@ In particular:
\item The reasoning about \gls{reif} in \minizinc{} 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{}. 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. 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. 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.
When \minizinc{} is used as part of a meta-optimization 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. When \minizinc{} is used as part of a \gls{meta-optimization} 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 rewritten to a \gls{slv-mod} each time. In the current tool chain, the whole model must be fully rewritten to a \gls{slv-mod} 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 spent \gls{rewriting} the core model over and over again. 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 spent \gls{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. This also prevents the \solver{} from carrying over anything it learnt from one problem to the next.
\end{itemize} \end{itemize}
\section{Research Objective and Contributions} \section{Research Aims 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. 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 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{}}. 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 should allow us to:
@ -226,28 +223,24 @@ Crucially, we ensure that the resulting system is fully incremental, and we expe
Overall, this thesis makes the following contributions. Overall, this thesis makes the following contributions.
\begin{enumerate} \begin{itemize}
\item It presents a formal execution model of rewriting for the \minizinc{} language and extends this model with well-known optimization and simplification techniques. \item It presents a formal execution model of rewriting for the \minizinc{} language and extends this model with well-known optimization and simplification techniques.
This model includes a novel method of tracking of \constraints{} created as part of functional dependencies, ensuring the correct removal of unnecessary \constraints{}.
\item It provides a novel method of tracking of \constraints{} created as part of functional dependencies, ensuring the correct removal of unnecessary \constraints{}. \item It presents an analysis technique to reason about in what (\gls{reified}) form a \constraint{} should be considered.
This analysis allows for the design and implementation of techniques to automatically introduce \gls{half-reified} \constraints{} in \minizinc{}, including a technique to simplify \glspl{slv-mod} by efficiently eliminating \glspl{implication-chain}.
\item It presents an analysis technique to reason about in what (\gls{reified}) form \constraints{} should be considered. \item It proposes two novel methods to reduce the overhead of using \cmls{} in incremental techniques: \gls{rbmo} and the \gls{incremental-rewriting} of changing \instances{} through an incremental interface.
\item It presents a design and implementation of techniques to automatically introduce \gls{half-reif} of \constraints{} in \minizinc{}. \end{itemize}
\item It develops a technique to simplify \glspl{slv-mod} by efficiently eliminating \glspl{implication-chain}.
\item It proposes two novel methods to reduce the overhead of using \cmls{} in incremental techniques: \gls{rbmo} and the \gls{incremental-rewriting} of changing \instances{}.
\end{enumerate}
\section{Organization of the Thesis} \section{Organization of the Thesis}
This thesis is arranged into the following chapters. This thesis is arranged into the following chapters.
Following this introductory chapter, \emph{\cref{ch:background}} gives an overview of the area of \cmls{}. Succeeding this introductory chapter, \emph{\cref{ch:background}} gives an overview of the area of \cmls{}.
First, it introduces the reader to \minizinc{}, how its models are formulated, and how they are translated to \solver{} specifications. 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{}.
This chapter also reviews techniques that are closely related to \cmls{}. This chapter also reviews techniques that are closely related to \cmls{}.
@ -270,7 +263,7 @@ We conclude this chapter by analysing the impact of \gls{half-reif} for differen
\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 the incremental \gls{rewriting}.
Instead, it integrates a 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} for 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.

6
chapters/2_background.tex
View File

@ -600,7 +600,7 @@ The most common method in \gls{cp} \solvers{} to keep track of \gls{domain} chan
Every \domain{} change that is made during \gls{propagation}, after the first search decision, is stored in a list. Every \domain{} change that is made during \gls{propagation}, after the first search decision, is stored in a list.
Whenever a new search decision is made, the current position of the list is tagged. Whenever a new search decision is made, the current position of the list is tagged.
If the \solver{} now needs to undo a search decision (i.e., \gls{backtrack}), it reverses all changes until it reaches the change that is tagged with the search decision. If the \solver{} now needs to undo a search decision (i.e., \gls{backtrack}), it reverses all changes until it reaches the change that is tagged with the search decision.
Because all changes before the tagged point on the \gls{trail} were made before the search decision was made, it is guaranteed that these \domain{} changes do not depend on the search decision. Since all changes before the tagged point on the \gls{trail} were made before the search decision was made, it is guaranteed that these \domain{} changes do not depend on the search decision.
Furthermore, because \gls{propagation} is performed to a \gls{fixpoint}, \gls{propagation} is never duplicated. Furthermore, because \gls{propagation} is performed to a \gls{fixpoint}, \gls{propagation} is never duplicated.
The solving method used by \gls{cp} \solvers{} is very flexible. The solving method used by \gls{cp} \solvers{} is very flexible.
@ -946,7 +946,7 @@ When solving a scheduling problem, \gls{opl} makes use of specialized interval \
The job shop problem is similar to the open shop problem discussed in the introduction. The job shop problem is similar to the open shop problem discussed in the introduction.
Like the open shop problem, the goal is to schedule jobs with multiple tasks. Like the open shop problem, the goal is to schedule jobs with multiple tasks.
Each task must be performed by an assigned machine. Each task must be performed by an assigned machine.
A machine can only perform one task at the same time. A machine can only perform one task at any one time.
And, only one task of the same job can be scheduled at the same time. And, only one task of the same job can be scheduled at the same time.
However, in the job shop problem, the tasks within a job also have a specified order. However, in the job shop problem, the tasks within a job also have a specified order.
Abstracting from the \parameter{} declarations, the possible formulation of the \variable{} declarations and \constraints{} for the job shop problem in \gls{opl} is shown in \cref{lst:back-opl-jsp}. Abstracting from the \parameter{} declarations, the possible formulation of the \variable{} declarations and \constraints{} for the job shop problem in \gls{opl} is shown in \cref{lst:back-opl-jsp}.
@ -1055,7 +1055,7 @@ Partitions are defined for finite types: Booleans, enumerated types, or a restri
Most of the problem is modelled on \lref{line:back:essence:var}. Most of the problem is modelled on \lref{line:back:essence:var}.
It declares a \variable{} that is a set of partitions of the golfers. It declares a \variable{} that is a set of partitions of the golfers.
The choice in \variable already contains some implied \constraints{}. The choice in \variable already contains some implied \constraints{}.
Because the \variable{} reasons about partitions of the golfers, a correct \gls{assignment} is already guaranteed to correctly split the golfers into groups. Since the \variable{} reasons about partitions of the golfers, a correct \gls{assignment} is already guaranteed to correctly split the golfers into groups.
The usage of a set of size \texttt{weeks} means that we directly reason about that number of partitions that have to be unique. The usage of a set of size \texttt{weeks} means that we directly reason about that number of partitions that have to be unique.
The type of the \variable{} does, however, not guarantee that two golfers will not meet each other twice. The type of the \variable{} does, however, not guarantee that two golfers will not meet each other twice.

2
chapters/4_half_reif.tex
View File

@ -924,7 +924,7 @@ This ensures that all \variables{} and \constraints{} created for the earlier ve
\end{nzn} \end{nzn}
\end{example} \end{example}
Because the expression itself is changed when a negation is moved inwards, it may not always be clear when the same expression is used in both \posc{} and \negc{} context. Since the expression itself is changed when a negation is moved inwards, it may not always be clear when the same expression is used in both \posc{} and \negc{} context.
This problem is solved by introducing a canonical form for expressions where negations can be pushed inwards. This problem is solved by introducing a canonical form for expressions where negations can be pushed inwards.
In this form the result of \gls{rewriting} an expression and its negation are collected in the same place within the \gls{cse} table. In this form the result of \gls{rewriting} an expression and its negation are collected in the same place within the \gls{cse} table.
If it is found that for an expression that is about to be \gls{half-reified} there already exists a \gls{half-reif} for its negation, then we instead evaluate the expression in \mixc{} context. If it is found that for an expression that is about to be \gls{half-reified} there already exists a \gls{half-reif} for its negation, then we instead evaluate the expression in \mixc{} context.