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

Fixes for most things pointed out by Andreas

Browse Source 
Some items left as TODO comments
This commit is contained in:
Jip J. Dekker 2021-07-12 17:07:07 +10:00
parent 8f6d5f1835
commit f81a077d82
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
6 changed files with 326 additions and 258 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
assets/bibliography/references.bib
View File

@ -265,6 +265,21 @@
year = 2020,
}
@article{dantzig-1982-simplex,
author = {George B. Dantzig},
title = {Reminiscences about the origins of linear programming},
journal = {Oper. Res. Lett.},
volume = {1},
number = {2},
pages = {43--48},
year = {1982},
url = {https://doi.org/10.1016/0167-6377(82)90043-8},
doi = {10.1016/0167-6377(82)90043-8},
timestamp = {Sun, 02 Jun 2019 20:50:37 +0200},
biburl = {https://dblp.org/rec/journals/orl/Dantzig82.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@article{davis-1960-dpll,
author = {Davis, Martin and Putnam, Hilary},
title = {A Computing Procedure for Quantification Theory},
@ -547,6 +562,22 @@
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@inproceedings{jaffar-1987-clp,
author = {Joxan Jaffar and Jean{-}Louis Lassez},
title = {Constraint Logic Programming},
booktitle = {Conference Record of the Fourteenth Annual {ACM} Symposium on
Principles of Programming Languages, Munich, Germany, January
21-23, 1987},
pages = {111--119},
publisher = {{ACM} Press},
year = {1987},
url = {https://doi.org/10.1145/41625.41635},
doi = {10.1145/41625.41635},
timestamp = {Tue, 06 Nov 2018 11:07:43 +0100},
biburl = {https://dblp.org/rec/conf/popl/JaffarL87.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@book{jaillet-2021-online,
title = {Online Optimization},
author = {Jaillet, P. and Wagner, M.R.},
@ -588,6 +619,21 @@
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@article{karmarkar-1984-interior-point,
author = {Narendra Karmarkar},
title = {A new polynomial-time algorithm for linear programming},
journal = {Comb.},
volume = {4},
number = {4},
pages = {373--396},
year = {1984},
url = {https://doi.org/10.1007/BF02579150},
doi = {10.1007/BF02579150},
timestamp = {Wed, 22 Jul 2020 22:02:37 +0200},
biburl = {https://dblp.org/rec/journals/combinatorica/Karmarkar84.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@article{kolisch-1997-psplib,
title = {PSPLIB - A project scheduling problem library: OR Software - ORSEP
Operations Research Software Exchange Program},

2
assets/mzn/back_knapsack.mzn
View File

@ -9,7 +9,7 @@ var set of TOYS: selection;@\Vlabel{line:back:knap:sel}@
var int: total_joy = sum(toy in selection)(toy_joy[toy]);@\Vlabel{line:back:knap:tj}@
% Constraints
constraint sum(toy in selection)(toy_space[toy]) < total_space;@\Vlabel{line:back:knap:con}@
constraint sum(toy in selection)(toy_space[toy]) <= total_space;@\Vlabel{line:back:knap:con}@
% Goal
solve maximize total_joy;@\Vlabel{line:back:knap:obj}@

64
assets/shorthands.tex
View File

@ -2,43 +2,43 @@
\renewcommand*{\implies}{\rightarrow}
% Academic writing
\newcommand*{\eg}{e.g.,\xspace{}}
\newcommand*{\ie}{i.e.,\xspace{}}
\newcommand*{\eg}{e.g.,\xspace}
\newcommand*{\ie}{i.e.,\xspace}
% Glossary entries
\newcommand*{\Cmls}{\Glspl{cml}}
\newcommand*{\cmls}{\glspl{cml}}
\newcommand*{\cml}{\gls{cml}}
\newcommand*{\compiler}{\gls{compiler}\xspace{}}
\newcommand*{\constraint}{\gls{constraint}\xspace{}}
\newcommand*{\Constraint}{\Gls{constraint}\xspace{}}
\newcommand*{\constraints}{\glspl{constraint}\xspace{}}
\newcommand*{\Constraints}{\Glspl{constraint}\xspace{}}
\newcommand*{\domain}{\gls{domain}\xspace{}}
\newcommand*{\domains}{\glspl{domain}\xspace{}}
\newcommand*{\flatzinc}{\gls{flatzinc}\xspace{}}
\newcommand*{\interpreter}{\gls{interpreter}\xspace{}}
\newcommand*{\instance}{\gls{instance}\xspace{}}
\newcommand*{\instances}{\glspl{instance}\xspace{}}
\newcommand*{\microzinc}{\gls{microzinc}\xspace{}}
\newcommand*{\minisearch}{\gls{minisearch}\xspace{}}
\newcommand*{\minizinc}{\gls{minizinc}\xspace{}}
\newcommand*{\cmodel}{\gls{model}\xspace{}}
\newcommand*{\cmodels}[0]{\glspl{model}\xspace{}}
\newcommand*{\nanozinc}{\gls{nanozinc}\xspace{}}
\newcommand*{\parameters}{\glspl{parameter}\xspace{}}
\newcommand*{\parameter}{\gls{parameter}\xspace{}}
\newcommand*{\reified}{\gls{reified}\xspace{}}
\newcommand*{\halfreified}{\gls{half-reified}\xspace{}}
\newcommand*{\solvers}{\glspl{solver}\xspace{}}
\newcommand*{\solver}{\gls{solver}\xspace{}}
\newcommand*{\Solvers}{\Glspl{solver}\xspace{}}
\newcommand*{\Solver}{\Gls{solver}\xspace{}}
\newcommand*{\variable}{\gls{variable}\xspace{}}
\newcommand*{\Variable}{\Gls{variable}\xspace{}}
\newcommand*{\variables}{\glspl{variable}\xspace{}}
\newcommand*{\Variables}{\Glspl{variable}\xspace{}}
\newcommand*{\zinc}{\gls{zinc}\xspace{}}
\newcommand*{\compiler}{\gls{compiler}\xspace}
\newcommand*{\constraint}{\gls{constraint}\xspace}
\newcommand*{\Constraint}{\Gls{constraint}\xspace}
\newcommand*{\constraints}{\glspl{constraint}\xspace}
\newcommand*{\Constraints}{\Glspl{constraint}\xspace}
\newcommand*{\domain}{\gls{domain}\xspace}
\newcommand*{\domains}{\glspl{domain}\xspace}
\newcommand*{\flatzinc}{\gls{flatzinc}\xspace}
\newcommand*{\interpreter}{\gls{interpreter}\xspace}
\newcommand*{\instance}{\gls{instance}\xspace}
\newcommand*{\instances}{\glspl{instance}\xspace}
\newcommand*{\microzinc}{\gls{microzinc}\xspace}
\newcommand*{\minisearch}{\gls{minisearch}\xspace}
\newcommand*{\minizinc}{\gls{minizinc}\xspace}
\newcommand*{\cmodel}{\gls{model}\xspace}
\newcommand*{\cmodels}[0]{\glspl{model}\xspace}
\newcommand*{\nanozinc}{\gls{nanozinc}\xspace}
\newcommand*{\parameters}{\glspl{parameter}\xspace}
\newcommand*{\parameter}{\gls{parameter}\xspace}
\newcommand*{\reified}{\gls{reified}\xspace}
\newcommand*{\halfreified}{\gls{half-reified}\xspace}
\newcommand*{\solvers}{\glspl{solver}\xspace}
\newcommand*{\solver}{\gls{solver}\xspace}
\newcommand*{\Solvers}{\Glspl{solver}\xspace}
\newcommand*{\Solver}{\Gls{solver}\xspace}
\newcommand*{\variable}{\gls{variable}\xspace}
\newcommand*{\Variable}{\Gls{variable}\xspace}
\newcommand*{\variables}{\glspl{variable}\xspace}
\newcommand*{\Variables}{\Glspl{variable}\xspace}
\newcommand*{\zinc}{\gls{zinc}\xspace}
% Semantic syntax (rewriting)
\renewcommand{\phi}{\varphi}

10
chapters/1_introduction.tex
View File

@ -24,7 +24,7 @@ For example, \gls{sat} \solvers{} can only reason about Boolean \variables{}, de
Its \constraints{} 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.
There are often many possible correct encodings of a problem, but there can be a significant difference in how quickly the \solver{} will find 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.
The preferred encoding can however differ between \solvers{}.
Two \solvers{} designed to solve the same problem class might perform very differently.
@ -33,7 +33,7 @@ They serve as a level of abstraction between the user 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{}.
A \cmodel{} can generally describe a class of problems through the use of \parameters{}, values assigned by external input.
Once given a complete assignment of the \parameters{}, the \cmodel{} forms an \instance{}.
The language will then create a \gls{slv-mod}, through a process called \gls{rewriting}, and interface with the \solver{} when trying to find an appropriate \gls{sol}.
The language then creates a \gls{slv-mod}, through a process called \gls{rewriting}, and interface with the \solver{} when trying to find an appropriate \gls{sol}.
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{}.
@ -97,7 +97,7 @@ For example, the concepts of one task preceding another and non-overlapping of t
The definition of \mzninline{nonoverlap} require that either task A precedes task B, or vice versa.
However, unlike the \gls{ampl} model, Prolog would not provide this choice to the \solver{}.
Instead, it will enforce one, test if this works, and otherwise enforce the other.
Instead, it enforces one, test if this works, and otherwise enforce the other.
This is a powerful mechanism where any 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{}.
@ -117,7 +117,7 @@ For example, a user could create a \minizinc{} function to express the non-overl
\end{mzn}
Fundamentally, in its \gls{rewriting} process \minizinc{} is a functional language.
It will continuously evaluate 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 computational language.
@ -260,7 +260,7 @@ 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}.
In this chapter, we present an formal analysis technique to reason about \gls{reif}.
This analysis can help us decide whether a \constraint{} will have 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}.
We thus present the first implementation of the usage of automatic \gls{half-reif}.
We conclude this chapter by analysing the impact of the usage of \gls{half-reif} for different types of \solvers{}.

454
chapters/2_background.tex
View File

File diff suppressed because it is too large Load Diff

8
chapters/2_background_preamble.tex
View File

@ -1,5 +1,5 @@
This research presented in this thesis investigates the process of \gls{rewriting} \cmls{} to address both the lack of information about this process and to improve this process to meet its modern day requirements.
This chapter provides the background necessary to understand the usage of \cmls{}:
This chapter provides the required background information to understand \cmls{}:
\begin{itemize}
\item How do you create a \cmodel{}?
@ -9,14 +9,14 @@ This chapter provides the background necessary to understand the usage of \cmls{
In particular, it gives further information about \minizinc{} and discusses the functionality available to create \cmodels{}.
It also provides some insight into \solvers{}, discussing the most important techniques used to solve \instances{} of \cmodels{}.
Additionally, it summarises the functionality of other \cmls{} to serve as a comparison with \minizinc{}
Additionally, it summarises the functionality of other \cmls{} to serve as a comparison with \minizinc{}.
This is followed by a brief overview of other closely related \glspl{trs}.
Finally, the chapter analyses the existing approach to \gls{rewriting} \minizinc{} and discusses its limitations.
The overview of \cmls{} presented in this chapter supports the research and discussion presented in subsequent chapters.
In the remainder of this chapter we will first, in \cref{sec:back-intro} introduce the reader to \cmls{} and their purpose.
In the remainder of this chapter we first, in \cref{sec:back-intro} introduce the reader to \cmls{} and their purpose.
\Cref{sec:back-minizinc} summarised the syntax and functionality of \minizinc{}, the leading \cml{} used within this thesis.
In \cref{sec:back-solving} we discuss how \gls{cp}, \gls{mip}, and \gls{sat} can be used to solve a \gls{slv-mod}.
In \cref{sec:back-solving} we discuss how \gls{cp}, \gls{mip}, and \gls{sat} are used to solve a \gls{slv-mod}.
\Cref{sec:back-other-languages} introduces alternative \cmls{} and compares their functionality to \minizinc{}.
Then, \cref{sec:back-term} survey the closely related technologies in the field of \glspl{trs}.
Finally, \cref{sec:back-mzn-interpreter} explores the process that the current \minizinc{} \interpreter{} uses to translate a \minizinc{} \instance{} into a \gls{slv-mod}.