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

Revert index to a glossary

Browse Source
This commit is contained in:
Jip J. Dekker 2021-06-28 13:16:42 +10:00
parent e05140062f
commit 4c276cdfa6
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
5 changed files with 170 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

160
assets/glossary.tex
View File

@ -71,12 +71,17 @@
\newglossaryentry{constraint}{
name={constraint},
description={},
description={A formalised rule of a problem. Constraints are generally expressed in term of Boolean logic},
}
\newglossaryentry{constraint-modelling}{
name={constraint modelling},
description={},
\newglossaryentry{cml}{
name={constraint modelling language},
description={
A constraint modelling language is a computer language used to define \glspl{model}.
Low-level constraint modelling languages allow modellers to define \glspl{model} in terms of \gls{native} \glspl{constraint} and \gls{variable} types.
To create a \gls{slv-mod} the language merely assigns the \glspl{parameter}, (almost) no \gls{rewriting} is required.
In contrast, high-level constraint modelling languages provide \glspl{global}, allowing modellers to reason at a level different from the targeted \gls{solver}
},
}
\newglossaryentry{constraint-store}{
@ -124,6 +129,29 @@
description={},
}
\newglossaryentry{cvar}{
name={control variable},
description={
A control variable is a special form of an \gls{ivar} where the \gls{variable} represent the result of a \gls{reification}
},
}
\newglossaryentry{dec-prb}{
name={decision problem},
description={
A problem which can be defined as making a set of decisions under a certain set of rules.
Decisions problems can be formalised as \glspl{model}.
},
}
\newglossaryentry{decomp}{
name={decomposition},
description={
A decomposition formulates a \gls{constraint} in terms of other \glspl{constraint} in order to reach \gls{native} \glspl{constraint}.
Note that the new \glspl{constraint} might represent the same decisions using a different \glspl{variable}, possibly of different types
},
}
\newglossaryentry{del-rew}{
name={delayed rewriting},
description={},
@ -131,7 +159,7 @@
\newglossaryentry{domain}{
name={domain},
description={},
description={A domain is a set of value that a \gls{variable} can take without violating any \glspl{constraint} in the problem},
}
\newglossaryentry{domain-con}{
@ -144,8 +172,18 @@
description={},
}
\newglossaryentry{eqsat}{
name={equisatisfiable},
description={Two \glspl{model} are equisatisfiable when a bijective function can be defined to map the \glspl{sol} of one \gls{model} onto the \glspl{sol} of the other.},
}
\newglossaryentry{fixed}{
name={fixed},
description={A \gls{variable} is said to be fixed when there is only a single possible value that it can take},
}
\newglossaryentry{fixpoint}{
name={fixpoint},
name={fix-point},
description={},
}
@ -176,7 +214,13 @@
\newglossaryentry{global}{
name={global constraint},
description={},
description={
A global constraint is a common \gls{constraint} pattern.
These patterns can generally span any number of \glspl{variable}.
For example, the well-known global constraint \( \textsc{All\_Different}(\ldots) \) requires all its arguments to take a different value.
Global constraints are usually not \gls{native} to a \gls{solver}.
Instead, the \gls{rewriting} process can enforce the global constraint using a \gls{decomp}
},
}
\newglossaryentry{gurobi}{
@ -194,11 +238,24 @@
description={},
}
\newglossaryentry{ivar}{
name={introduced variable},
description={
An introduced variable is a \gls{variable} that was created in the reformulation of a \gls{decomp}.
New \gls{variable} are introduced either to redefine an existing \gls{variable} using a different type or to connect newly introduced \glspl{constraint}
},
}
\newglossaryentry{interval}{
name={interval},
description={},
}
\newglossaryentry{instance}{
name={instance},
description={A \gls{model} with assignments for all its \glspl{parameter}},
}
\newglossaryentry{knapsack}{
name={knapsack problem},
description={},
@ -235,6 +292,16 @@
description={},
}
\newglossaryentry{model}{
name={constraint model},
description={
A constraint model is a formalisation of a \gls{dec-prb} or an \gls{opt-prb}.
It is defined in terms of formalised decision, \glspl{variable} of different kinds (\eg{} Boolean, integers, or even sets), and \glspl{constraint}, Boolean logic formulas which are forced to hold in any \gls{sol}, and, in case of an \gls{opt-prb}, an \gls{objective}.
Any external data required to formulate the \glspl{constraint} is said to be the \glspl{parameter}.
The combination of a constraint model and assignments for its \glspl{parameter} is said to be an \gls{instance} of the constraint model.
},
}
\newglossaryentry{minizinc}{
name={Mini\-Zinc},
description={},
@ -250,6 +317,11 @@
description={},
}
\newglossaryentry{native}{
name={native},
description={\glspl{constraint} and \gls{variable} types are said to be native to a \gls{solver} when they can be directly used as input for the \gls{solver}},
}
\newglossaryentry{nanozinc}{
name={Nano\-Zinc},
description={},
@ -261,8 +333,8 @@
}
\newglossaryentry{objective}{
name={objective},
description={},
name={objective function},
description={An objective function is a function defined over the \glspl{variable} of a \gls{model} to assign a numeric value to the quality of the \gls{sol}.},
}
\newglossaryentry{operator}{
@ -275,11 +347,26 @@
description={},
}
\newglossaryentry{opt-prb}{
name={optimisation problem},
description={
A decision problem with an additional \gls{objective}.
It can, likewise, be formalised as a \gls{model}.
If the problem has multiple \glspl{sol}, then this function can be used to asses the quality on the \gls{sol}.
For such a problem, an \gls{opt-sol} is a \gls{sol} with the highest quality
},
}
\newglossaryentry{optional}{
name={optional},
description={},
}
\newglossaryentry{opt-sol}{
name={optimal solution},
description={An \gls{sol} in an \gls{opt-prb} for which it has been proven that no other \gls{sol} exist of higher quality},
}
\newglossaryentry{restart}{
name={restart},
description={},
@ -295,14 +382,27 @@
description={},
}
\newglossaryentry{sol}{
name={solution},
description={A solution is an assignment for all \glspl{variable} in an \gls{instance} such that no \gls{constraint} is violated},
}
\newglossaryentry{solver}{
name={solver},
description={},
description={
A solver is a computer program that is designed to solve certain types of \gls{dec-prb} and/or \gls{opt-prb}.
Given a \gls{slv-mod}, in a specified format, a solver will (eventually) produce a \gls{sol} for it.
When solving a \gls{opt-prb}, solvers often produce intermediate \glspl{sol} before producing the \gls{opt-sol}
},
}
\newglossaryentry{parameter}{
name={problem parameter},
description={},
description={
A problem parameter is immutable data used to define one or more \glspl{constraint}.
Parameters are part of the external input for a \gls{model}.
The combination of a \gls{model} and assignment for all its problem parameters is referred to as an \gls{instance} of a \gls{model}
},
}
\newglossaryentry{propagation}{
@ -322,7 +422,31 @@
\newglossaryentry{reification}{
name={reification},
description={},
description={A reification is a special form of a \gls{constraint} where, instead of the \gls{constraint} being enforced in the \glspl{sol}, it enforces that a \gls{cvar} represents whether the \gls{constraint} holds or not},
}
\newglossaryentry{rewriting}{
name={rewriting},
description={
The process of transforming a \gls{model} \gls{instance} into an \gls{eqsat} \gls{slv-mod} is referred to as rewriting.
This happens primarily through the application of \glspl{decomp}
},
}
\newglossaryentry{satisfied}{
name={satisfied},
description={
A \gls{constraint} is said to be satisfied when its logical expression is proven to hold.
Furthermore, a \gls{dec-prb} is said to be satisfied when all its \glspl{constraint} are satisfied
},
}
\newglossaryentry{slv-mod}{
name={solver model},
description={
A solver model is a \gls{instance} of a \gls{model} where all \glspl{constraint} and \gls{variable} types are \gls{native} for the targeted \gls{solver}.
\glspl{instance} of \glspl{model} containing non-native \glspl{constraint} and/or \gls{variable} types can be transformed into solver models through the process of \gls{rewriting}
},
}
\newglossaryentry{scip}{
@ -355,9 +479,19 @@
description={},
}
\newglossaryentry{unsat}{
name={unsatisfiable},
description={A problem is unsatisfiable when there exists no possible for the problem},
}
\newglossaryentry{variable}{
name={decision variable},
description={},
description={
A formalised decision that is yet to be made.
When searching for a \gls{sol} a decision variable is said to have a certain \gls{domain}, which contains the values that the decision variable might still take.
If at any point the \gls{domain} is reduced to a single value, then the decision variable is said to be \gls{fixed}.
If, however, a decision variable has an empty \gls{domain}, then there is no value it can take that is consistent with the \glspl{constraint}
},
}
\newglossaryentry{zinc}{

6
assets/shorthands.tex
View File

@ -6,9 +6,9 @@
\newcommand{\ie}{i.e.,\xspace{}}
% Glossary entries
\newcommand{\Cmls}{\Gls{constraint-modelling} languages\xspace{}}
\newcommand{\cmls}{\gls{constraint-modelling} languages\xspace{}}
\newcommand{\cml}{\gls{constraint-modelling} language\xspace{}}
\newcommand{\Cmls}{\Glspl{cml}}
\newcommand{\cmls}{\glspl{cml}}
\newcommand{\cml}{\gls{cml}}
\newcommand{\constraints}{\glspl{constraint}\xspace{}}
\newcommand{\constraint}{\gls{constraint}\xspace{}}
\newcommand{\flatzinc}{\gls{flatzinc}\xspace{}}

39
chapters/2_background_preamble.tex
View File

@ -1,32 +1,15 @@
\noindent{}A goal shared between all programming languages is to provide a certain level
of abstraction: an assembly language allows you to abstract from the binary
instructions and memory positions; Low-level imperial languages, like FORTRAN,
were the first to allow you to abstract from the processor architecture of the
target machine; and nowadays writing a program requires little knowledge of the
actual workings of the hardware on which the program is executed.
\noindent{}A goal shared between all programming languages is to provide a certain level of abstraction: an assembly language allows you to abstract from the binary instructions and memory positions; Low-level imperial languages, like FORTRAN, were the first to allow you to abstract from the processor architecture of the target machine; and nowadays writing a program requires little knowledge of the actual workings of the hardware on which the program is executed.
Freuder states that the ``Holy Grail'' of programming languages would be where
the user merely states the problem, and the computer solves it and that
\gls{constraint-modelling} is one of the biggest steps towards this goal to
this day \autocite*{freuder-1997-holygrail}. Different from imperative (and
even other declarative) languages, in a \cml{} the modeller does not describe
how to solve the problem, but rather provides the problem requirements. You
could say that a constraint model actually describes the solution to the
problem.
Freuder states that the ``Holy Grail'' of programming languages would be where the user merely states the problem, and the computer solves it and that constraint modelling is one of the biggest steps towards this goal to this day \autocite*{freuder-1997-holygrail}.
Different from imperative (and even other declarative) languages, in a \cml{} the modeller does not describe how to solve the problem, but rather provides the problem requirements.
You could say that a constraint model actually describes the solution to the problem.
In a constraint model, instead of specifying the manner in which we can find
the solution, we give a concise description of the problem. We describe what we
already know, the \parameters{}, what we wish to know, the \variables{}, and
the relationships that should exist between them, the \constraints{}.
In a constraint model, instead of specifying the manner in which we can find the solution, we give a concise description of the problem.
We describe what we already know, the \parameters{}, what we wish to know, the \variables{}, and the relationships that should exist between them, the \constraints{}.
This type of combinatorial problem is typically called a \gls{csp}. The goal of
a \gls{csp} is to find values for the \variables{} that satisfy the
\constraints{} or prove that no such assignment exists. Many \cmls\ also
support the modelling of \gls{cop}, where a \gls{csp} is augmented with a
\gls{objective} \(z\). In this case the goal is to find a solution that
satisfies all \constraints{} while minimising (or maximising) \(z\).
This type of combinatorial problem is typically called a \gls{csp}.
The goal of a \gls{csp} is to find values for the \variables{} that satisfy the \constraints{} or prove that no such assignment exists.
Many \cmls\ also support the modelling of \gls{cop}, where a \gls{csp} is augmented with a \gls{objective} \(z\).
In this case the goal is to find a solution that satisfies all \constraints{} while minimising (or maximising) \(z\).
Although a constraint model does not contain any instructions on how to find a
suitable solution, these models can generally be given to a dedicated solving
program, or \solver{} for short, that can find a solution that fits the
requirements of the model.
Although a constraint model does not contain any instructions on how to find a suitable solution, these models can generally be given to a dedicated solving program, or \solver{} for short, that can find a solution that fits the requirements of the model.

8
chapters/5_incremental_preamble.tex
View File

@ -24,9 +24,9 @@ Examples of these methods are:
All of these examples have in common that a problem instance is solved, new constraints are added, the resulting instance is solved again, and constraints may be removed again.
The usage of these methods is not new to \gls{constraint-modelling}, and they have proven to be very useful \autocite{schrijvers-2013-combinators, rendl-2015-minisearch, schiendorfer-2018-minibrass, ek-2020-online, ingmar-2020-diverse}.
In its most basic form, a simple scripting language is sufficient to implement these methods, by repeatedly calling on the \gls{constraint-modelling} infrastructure to compile and solve the adjusted constraint models.
While improvements of the compilation of constraint models, such as the ones discussed in previous chapters, can increase the performance of these approaches, the overhead of re-compiling an almost identical model may still prove prohibitive, warranting direct support from the \gls{constraint-modelling} infrastructure.
The usage of these methods is not new to constraint modelling, and they have proven to be very useful \autocite{schrijvers-2013-combinators, rendl-2015-minisearch, schiendorfer-2018-minibrass, ek-2020-online, ingmar-2020-diverse}.
In its most basic form, a simple scripting language is sufficient to implement these methods, by repeatedly calling on the constraint modelling infrastructure to compile and solve the adjusted constraint models.
While improvements of the compilation of constraint models, such as the ones discussed in previous chapters, can increase the performance of these approaches, the overhead of re-compiling an almost identical model may still prove prohibitive, warranting direct support from the constraint modelling infrastructure.
In this chapter we introduce two methods to provide this support:
\begin{itemize}
@ -40,6 +40,6 @@ In this chapter we introduce two methods to provide this support:
The rest of the chapter is organised as follows.
\Cref{sec:6-modelling} discusses the declarative modelling of restart-based \gls{meta-search} algorithms that can be modelled directly in a \cml{}.
\Cref{sec:6-solver-extension} introduces the method to compile these \gls{meta-search} specifications into efficient solver-level specifications that only require a small extension of existing \glspl{solver}.
\Cref{sec:6-incremental-compilation} introduces the alternative method that extends the \gls{constraint-modelling} infrastructure with an interface to add and remove constraints from an existing model while avoiding recompilation.
\Cref{sec:6-incremental-compilation} introduces the alternative method that extends the constraint modelling infrastructure with an interface to add and remove constraints from an existing model while avoiding recompilation.
\Cref{sec:inc-experiments} reports on the experimental results of both approaches.

6
dekker_thesis.tex
View File

@ -115,9 +115,13 @@ Some ideas and figures included in this thesis have previously appeared in the f
\backmatter{}
\printbibliography{}
% -- Acronyms
\printglossary[nonumberlist,type=\acronymtype]{}
% -- Glossary
\renewcommand{\glsnamefont}[1]{\titlecap{#1}}
\printglossary[style=bookindex,title=Index]{}
\defglsentryfmt[main]{\textit{\glsgenentryfmt}}
\printglossary[style=altlistgroup]{}
\cleardoublepage
\pdfbookmark{\contentsname}{Contents}