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

More work on the background sections

Browse Source
This commit is contained in:
Jip J. Dekker 2021-05-15 17:07:53 +10:00
parent 5f09ec6d02
commit 7c131f7412
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
4 changed files with 275 additions and 103 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

127
assets/bibliography/references.bib
View File

@ -252,6 +252,32 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{fourer-2002-amplcp,
author = {Robert Fourer and David M. Gay},
title = {Extending an Algebraic Modeling Language to Support
Constraint Programming},
journal = {{INFORMS} J. Comput.},
volume = 14,
number = 4,
pages = {322--344},
year = 2002,
url = {https://doi.org/10.1287/ijoc.14.4.322.2825},
doi = {10.1287/ijoc.14.4.322.2825},
timestamp = {Sun, 15 Mar 2020 19:45:41 +0100},
biburl = {https://dblp.org/rec/journals/informs/FourerG02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{fourer-2003-ampl,
title = {AMPL: A Modeling Language for Mathematical Programming},
author = {Fourer, R. and Gay, D.M. and Kernighan, B.W.},
isbn = 9780534388096,
lccn = 00698382,
series = {Scientific Press series},
year = 2003,
publisher = {Thomson/Brooks/Cole}
}
@article{freuder-1997-holygrail,
author = {Eugene C. Freuder},
title = {In Pursuit of the Holy Grail},
@ -267,6 +293,29 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@software{gecode-2021-gecode,
author = {{Gecode Team}},
title = {Gecode: A Generic Constraint Development Environment},
year = 2021,
url = {http://www.gecode.org},
version = {6.3.0},
}
@software{gurobi-2021-gurobi,
author = {{Gurobi Optimization, LLC}},
title = {Gurobi Optimizer Reference Manual},
year = 2021,
url = {http://www.gurobi.com},
}
@software{minizinc-2021-minizinc,
author = {{MiniZinc Team}},
title = {MiniZinc: a free and open-source constraint modeling language},
year = 2021,
url = {http://www.minizinc.org},
version = {2.5.5},
}
@inproceedings{frisch-2007-essence,
author = {Alan M. Frisch and Matthew Grum and Christopher Jefferson
and Bernadette Mart{\'{\i}}nez Hern{\'{a}}ndez and Ian Miguel},
@ -304,27 +353,19 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@software{gecode-2021-gecode,
author = {{Gecode Team}},
title = {Gecode: A Generic Constraint Development Environment},
year = 2021,
url = {http://www.gecode.org},
version = {6.3.0},
}
@software{gurobi-2021-gurobi,
author = {{Gurobi Optimization, LLC}},
title = {Gurobi Optimizer Reference Manual},
year = 2021,
url = {http://www.gurobi.com},
}
@software{minizinc-2021-minizinc,
author = {{MiniZinc Team}},
title = {MiniZinc: a free and open-source constraint modeling language},
year = 2021,
url = {http://www.minizinc.org},
version = {2.5.5},
@article{fruhwirth-1998-chr,
author = {Thom W. Fr{\"{u}}hwirth},
title = {Theory and Practice of Constraint Handling Rules},
journal = {J. Log. Program.},
volume = 37,
number = {1-3},
pages = {95--138},
year = 1998,
url = {https://doi.org/10.1016/S0743-1066(98)10005-5},
doi = {10.1016/S0743-1066(98)10005-5},
timestamp = {Wed, 17 Feb 2021 08:54:37 +0100},
biburl = {https://dblp.org/rec/journals/jlp/Fruhwirth98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{hebrard-2005-diverse,
@ -567,6 +608,17 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@phdthesis{rendl-2010-thesis,
author = {Andrea Rendl},
title = {Effective compilation of constraint models},
school = {University of St Andrews, {UK}},
year = {2010},
url = {http://hdl.handle.net/10023/973},
timestamp = {Thu, 25 Aug 2016 17:20:59 +0200},
biburl = {https://dblp.org/rec/phd/ethos/Rendl10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{nethercote-2007-minizinc,
author = {Nicholas Nethercote and Peter J. Stuckey and Ralph Becket
and Sebastian Brand and Gregory J. Duck and Guido Tack},
@ -617,17 +669,6 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@phdthesis{rendl-2010-thesis,
author = {Andrea Rendl},
title = {Effective compilation of constraint models},
school = {University of St Andrews, {UK}},
year = {2010},
url = {http://hdl.handle.net/10023/973},
timestamp = {Thu, 25 Aug 2016 17:20:59 +0200},
biburl = {https://dblp.org/rec/phd/ethos/Rendl10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{rendl-2009-enhanced-tailoring,
author = {Andrea Rendl and Ian Miguel and Ian P. Gent and Christopher
Jefferson},
@ -810,6 +851,17 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@techreport{gamrath-2020-scip,
author = {Gerald Gamrath and Daniel Anderson and Ksenia Bestuzheva and Wei-Kun Chen and Leon Eifler and Maxime Gasse and Patrick Gemander and Ambros Gleixner and Leona Gottwald and Katrin Halbig and Gregor Hendel and Christopher Hojny and Thorsten Koch and Le Bodic, Pierre and Stephen J. Maher and Frederic Matter and Matthias Miltenberger and Erik M{\"u}hmer and Benjamin M{\"u}ller and Marc E. Pfetsch and Franziska Schl{\"o}sser and Felipe Serrano and Yuji Shinano and Christine Tawfik and Stefan Vigerske and Fabian Wegscheider and Dieter Weninger and Jakob Witzig},
title = {{The SCIP Optimization Suite 7.0}},
type = {ZIB-Report},
institution = {Zuse Institute Berlin},
number = {20-10},
month = {3},
year = {2020},
url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-78023}
}
@book{silvano-1990-knapsack,
author = {Martello, Silvano and Toth, Paolo},
title = {Knapsack Problems: Algorithms and Computer Implementations},
@ -854,17 +906,6 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@techreport{gamrath-2020-scip,
author = {Gerald Gamrath and Daniel Anderson and Ksenia Bestuzheva and Wei-Kun Chen and Leon Eifler and Maxime Gasse and Patrick Gemander and Ambros Gleixner and Leona Gottwald and Katrin Halbig and Gregor Hendel and Christopher Hojny and Thorsten Koch and Le Bodic, Pierre and Stephen J. Maher and Frederic Matter and Matthias Miltenberger and Erik M{\"u}hmer and Benjamin M{\"u}ller and Marc E. Pfetsch and Franziska Schl{\"o}sser and Felipe Serrano and Yuji Shinano and Christine Tawfik and Stefan Vigerske and Fabian Wegscheider and Dieter Weninger and Jakob Witzig},
title = {{The SCIP Optimization Suite 7.0}},
type = {ZIB-Report},
institution = {Zuse Institute Berlin},
number = {20-10},
month = {3},
year = {2020},
url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-78023}
}
@article{stuckey-2014-challenge,
author = {Peter J. Stuckey and Thibaut Feydy and Andreas Schutt and
Guido Tack and Julien Fischer},

6
assets/glossary.tex
View File

@ -69,6 +69,12 @@
description={},
}
\newglossaryentry{constraint-store}{
name={constraint store},
description={},
}
\newglossaryentry{gls-chr}{
name={constraint handling rules},
description={},

2
assets/packages.tex
View File

@ -198,6 +198,6 @@ outputdir=build,
breaklines,
breakindent=4em,
numbers=none,
escapeinside=@@,
% escapeinside=@@,
fontsize=\scriptsize,
]{text}}{\end{minted}}

243
chapters/2_background.tex
View File

@ -587,10 +587,34 @@ expressions in the \gls{solver} model.
There are many prominent techniques to solve a \gls{constraint} model, but none
of them will solve a \minizinc\ model directly. Instead a \minizinc\ model get
translated into \glspl{variable} and \glspl{constraint} of the type that the
solver supports directly. To understand the challenges in the translations a
\minizinc\ model into a solver level \gls{constraint} model, this section will
discuss the different technologies used used by \minizinc\ solver targets: their
input types and the basic method of solving the given problem.
solver supports directly.
\minizinc\ was initially designed as an input language for \gls{cp}
\glspl{solver}. These \glspl{solver} often support many of the high-level
\glspl{constraint} that are written in a \minizinc\ model. For \gls{cp} solvers
the amount of translation required can vary a lot. It depends on which
\glspl{constraint} the targeted \gls{cp} \gls{solver} are directly supported and
which \glspl{constraint} have to be decomposed.
Because \gls{cp} \glspl{solver} work on a similar level as the \minizinc\
language, some of the techniques used in \gls{cp} \glspl{solver} can also be
used during the transformation from \minizinc\ to \flatzinc{}. The usage of
these techniques can often help shrink the \glspl{domain} of \glspl{variable}
and eliminate or simplify \gls{constraint}. \Cref{subsec:back-cp} explains the
general method employed by \gls{cp} \glspl{solver} to solve a \gls{constraint}
model.
Throughout the years \minizinc\ has seen the addition of solvers using other
approaches to finding solutions to \gls{constraint} models. Although these
\glspl{solver} bring new classes of problems that can be solved using
\minizinc{}, they also bring new challenges in to efficiently encode the problem
for these \glspl{solver}. To understand these challenges in the translations a
\minizinc\ model into a solver level \gls{constraint} model, the remainder of
this section will discuss the other dominant technologies used used by
\minizinc\ \gls{solver} targets and their input language.
\subsection{Constraint Programming}%
\label{subsec:back-cp}
\subsection{Boolean Satisfiability}%
\label{subsec:back-sat}
@ -598,9 +622,6 @@ input types and the basic method of solving the given problem.
\subsection{Mathematical Programming}%
\label{subsec:back-mip}
\subsection{Constraint Programming}%
\label{subsec:back-cp}
\subsection{Hybrid Technologies}%
\label{subsec:back-hybrid}
@ -867,51 +888,61 @@ compatible with the targeted solver.
At the heart of the flattening process lies a \gls{trs}. A \gls{trs}
\autocite{baader-1998-term-rewriting} describes a computational model the full
process can be describe as the application of rules \(l \rightarrow r\), that
replace a \gls{term} \(l\) with another \gls{term} \(r\). A \gls{term} is an
expression with nested sub-expressions consisting of \emph{function} and
\emph{constant} symbols. An example of a term is \(F(0 + 1,F(1,0))\), where
\(F\) and \(+\) are function symbols and \(0\) and \(1\) are constant symbols.
In a term rewriting rule, a term can also contain a \emph{term variable} which
captures a term sub-expression. For example, the following \gls{trs} consists of
some (well-known) rules to handle logical and:
process can be describe as the application of rules
\(l \rightarrow r_{1}, \ldots r_{n}\), that replace a \gls{term} \(l\) with one
or more \glspl{term} \(r_{1}, \ldots r_{n}\). A \gls{term} is an expression with
nested sub-expressions consisting of \emph{function} and \emph{constant}
symbols. An example of a term is \(F(0 + 1,F(1,0))\), where \(F\) and \(+\) are
function symbols and \(0\) and \(1\) are constant symbols. In a term rewriting
rule, a term can also contain a \emph{term variable} which captures a term
sub-expression.
\begin{align*}
(r_{1}):\hspace{5pt}& 0 \land x \rightarrow 0 \\
(r_{2}):\hspace{5pt}& 1 \land x \rightarrow x \\
(r_{3}):\hspace{5pt}& x \land y \rightarrow y \land x
\end{align*}
\begin{example}
Consider the following \gls{trs} consists of some (well-known) rules to
rewrite logical and operations:
From these rules it follows that
\begin{align*}
(r_{1}):\hspace{5pt}& 0 \land x \rightarrow 0 \\
(r_{2}):\hspace{5pt}& 1 \land x \rightarrow x \\
(r_{3}):\hspace{5pt}& x \land y \rightarrow y \land x
\end{align*}
\[ 1 \land 1 \land 0 \rightarrow^{r_{1}} 1 \land 0 \rightarrow^{r_{3}} 0 \land 1 \rightarrow^{r_{2}} 0 \]
From these rules it follows that
Notice that there can be a choice between different rules. A \gls{trs} can be
non-deterministic. In the example we could also have applied the \(r_{1}\) twice
and arrived at the same result. Two important properties of \gls{trs} are,
therefore, \gls{termination} and \gls{confluence}. A \gls{trs} is said to be
terminating if, no-matter what order the term rewriting rules are applied, you
always arrive at a \gls{normal-form} (\ie, a term where no more rules apply). A
\gls{trs} is confluent if, no-matter what order the term rewriting rules are
applied, you always arrive at the same \gls{normal-form} (if you arrive at a
\gls{normal-form}).
\[ 1 \land 1 \land 0 \rightarrow^{r_{1}} 1 \land 0 \rightarrow^{r_{3}} 0 \land 1 \rightarrow^{r_{2}} 0 \]
Notice that there can be a choice between different rules. In general, a
\gls{trs} can be non-deterministic. We could also have applied the \(r_{1}\)
twice and arrived at the same result.
\end{example}
Two properties of a \gls{trs} that are often studied are \gls{termination} and
\gls{confluence}. A \gls{trs} is said to be terminating if, no-matter what order
the term rewriting rules are applied, you always arrive at a \gls{normal-form}
(\ie, a term where no more rules apply). A \gls{trs} is confluent if, no-matter
what order the term rewriting rules are applied, you always arrive at the same
\gls{normal-form} (if you arrive at a \gls{normal-form}).
It is trivial to see that our previous example is non-terminating, since you can
repeat rule \(r_{3}\) an infinite amount of times. The system, however, is
confluent as, if it arrives at the same \gls{normal-form}: if the term contains
any \(0\), then the result will be \(0\); otherwise, the result will be \(1\).
In \minizinc\ the flattening process is forced to be confluent. Through the
function definitions in the language and the type system, \minizinc{} ensures
that there is at most one applicable rule for any expression. This means that
given the same \minizinc\ model and solver library, the flattening process will
result in the same solver level constraint model.
These properties are also interesting when in the translation process of a
\minizinc{} instance into \flatzinc{}. The confluence of the translation process
will ensure that the same \flatzinc{} is produced independently of the order in
which the \minizinc\ model is processed. This is a desirable quality as it makes
the behaviour of the translation process more predictable.
The flattening process is, however, not guaranteed to terminate. When using
recursive functions, it is possible to create a \minizinc\ model that never
reaches a flat state. In practice, however, function definitions generally do
not contain any recursive definitions. In the absence of recursive functions the
flattening of a model is guaranteed to terminate.
Many of the techniques used by \glspl{solver} targeted by \minizinc\ are proven
to be complete. Meaning that they are guaranteed to find a (best) solution to
the problem or prove that there is none. For this quality to hold for the
\minizinc\ solving process, it has to be guaranteed that the \minizinc\
translation process terminates (so the solving process can start).
In the remainder of this section we will discuss two types of \glspl{trs} that
are closely related to \cmls\ and their compilation into solver level constraint
models: \glsaccesslong{clp} and \glsaccesslong{chr}.
\subsection{Constraint Logic Programming}%
\label{subsec:back-clp}
@ -919,24 +950,118 @@ flattening of a model is guaranteed to terminate.
\gls{clp} \autocite{marriott-1998-clp} can be seen as a predecessor of \cmls{}
like \minizinc. A constraint logic program describes the process in which a high
level constraint model is eventually rewritten into a solver level constraints
and added to a \gls{solver}. Different from \minizinc{}, the programmer can
define constraints that can be rewritten in multiple ways. When such a
constraint occurs in the constraint model, referred to as the goal, the
constraint logic program will try a different way whenever the problem becomes
unsatisfiable.
and added to a \gls{solver}. Like in \minizinc, can define \gls{constraint}
predicates to use in the definition of the \gls{constraint} model. Different
from \minizinc{}, constraint predicates in \gls{clp} can be rewritten in
multiple ways. The goal of a constraint logic program is to rewrite all
\glspl{constraint} in such a way that the solver level \glspl{constraint} are
all satisfied.
Variables are another notable difference between \cmls\ and \gls{clp}. In
\gls{clp}, like in a conventional \gls{trs}, a variable is merely a name. The
symbol might be replace or equated with a constant symbol, but, different from
\cmls{}, this is not a requirement. A variable can remain a name in the solution
of a constraint logic program. This means that the solution of a constraint
logic program can be a relationship between different variables. In cases where
a instantiated solution is required, a special \mzninline{labeling} constraint
can be used to force a variable to take a constant value. Similarly, there is a
\mzninline{minimize} that can be used to find the optimal value for a variable.
The evaluation of a constraint logic program rewrites the list of constraints,
called the goal, in the order given by the programmer. The rewriting of the
constraint predicates is tried in the order in which the different rewriting
rules for the constraint predicates are defined. The process is completed when
all constraints are rewritten and no inconsistency is detected between the
solver level constraints that are produced. If all the possible ways of
rewriting the program are tried, but all of them prove to be inconsistent, then
the program itself can be said to be unsatisfiable. Even when a correct
rewriting is found, it is possible to continue the process. This ways you can
find all possible correct ways to rewrite the program.
To implement this mechanism there is a tight integration between the solver,
referred to as the constraint store, and constraint logic program. In addition
to just adding constraints, the program can also inspect the status of the
constraint and retract constraints from the constraint store. This allows the
program to detect when the constraint store has become unsatisfiable and then
\gls{backtrack} the constraint store to the last decision (\ie, restore the
constraint store to its state before the last decision was made).
referred to as the \gls{constraint-store}, and the evaluator of the constraint
logic program. In addition to just adding \glspl{constraint}, the program can
also inspect the status of the constraint and retract constraints from the
constraint store. This allows the program to detect when the constraint store
has become inconsistent and then \gls{backtrack} the constraint store to the
last decision (\ie\ restore the \gls{constraint-store} to its state before the
last decision was made) and try the next rewriting rule.
The strength of the \gls{constraint-store} can influence the correctness of a
constraint logic program. Some \glspl{solver} are incomplete; it is unable to
tell if some of its \glspl{constraint} are satisfied or not. This, for example,
happens with \glspl{solver} that work with integer \glspl{domain}. In these
cases the programmer must use the \mzninline{labeling} constraint to force
constant values for the variables. Once the variables have been assigned
constant values, the solver will be able to decide if the constraints are
satisfied.
\subsection{Constraint Handling Rules}%
\label{sub:back-chr}
\gls{chr} are a special kind of \glspl{trs} designed to
When \glspl{constraint} are seen as terms in a \gls{trs}, then it is not just
possible to define rules to rewrite constraints to the level of a \gls{solver}.
It is also possible to define rules to simplify, propagate, and derive new
constraints within the solver. \gls{chr} follow from this idea. \gls{chr} are a
language extension (targeted at \gls{clp}) to allow user-defined constraints
within a \gls{solver}. \Glspl{constraint} defined using \gls{chr} are rewritten
into simpler constraints until they are solved.
Different from \gls{clp}, \gls{chr} allows term rewriting rules that are
multi-headed. This means that, for some rules, multiple terms must match, to
apply the rule.
\begin{example}
Consider the following user-defined constraint for logical implication using
\gls{chr}.
\begin{plain}
reflexivity @ X -> Y <=> X = Y | true
anti-symmetry @ X -> Y, Y -> X <=> X = Y
transitivity @ X -> Y, Y -> Z ==> X -> Z
\end{plain}
These definitions specify how \texttt{->} simplifies and propagates as a
constraint. The rules follow the mathematical concepts of reflexivity,
anti-symmetry, and transitivity.
\begin{itemize}
\item The first rules states that if \texttt{X = Y}, then \texttt{X -> Y} is
logically true. This rule removes the term \texttt{X -> Y}. Since the
constraint is said to be logically true, nothing gets added. \texttt{X
= Y} functions as a guard. This \gls{solver} builtin \gls{constraint}
is required for the rewriting rule to apply.
\item The second rule implements the anti-symmetry of logical implications;
the two implications, \texttt{X -> Y} and \texttt{Y -> X}, are
replaced by a \gls{solver} builtin, \texttt{X = Y}.
\item Finally, the transitivity rule introduces a derived constraint. When
it finds constraints \texttt{X -> Y} and \texttt{Y -> Z}, then it adds
another constraint \texttt{X -> Z}. Different from the other rules, no
constraints are removed.
\end{itemize}
Note that the use of multi-headed rewriting rules is essential to define these
rules.
\end{example}
The rules in a \gls{chr} system can be categorised into three different
categories: simplification, propagation, simpagation. The first two rules in the
previous example are simplification rules: they replace some constraint atoms by
others. The final rule in the example was a propagation rule: based on the
existence of certain constraints, new constraints can be introduced. Simpagation
rules are a combination of both types of rules in the form:
\[ H_{1}, \ldots H_{l} \backslash H_{l+1}, \ldots, H_{n} \texttt{<=>} G_{1}, \ldots{}, G_{m} | B_{1}, \ldots, B_{o} \]
It is possible to rewrite using a simpagation rule when there are terms matching
\(H_{1}, \ldots, H_{n}\) and there are \gls{solver} built-ins
\(G_{1}, \ldots{}, G_{m}\). When the simpagation rule is applied, the terms
\(H_{l+1}, \ldots, H_{n}\) are replaced by the terms \(B_{1}, \ldots, B_{o}\).
The terms \(H_{1}, \ldots H_{l}\) are kept in the system. Since simpagation
rules incorporate both the elements of simplication and propagation rules, it is
possible to formulate all rules as simpagation rules.
\subsection{ACD Term Rewriting}%
\label{subsec:back-acd}
@ -1228,12 +1353,12 @@ system becomes non-confluent, and some orders of execution may produce
well-known method called ``big-M transformation''. The expression
\mzninline{ub(x)} returns a valid upper bound for \mzninline{x}, \ie\ a fixed
value known to be greater than or equal to \mzninline{x}. This could be the
initial upper bound \mzninline{x} was declared with, or the current value in
the corresponding \nanozinc\ \mzninline{mkvar} call. If \mzninline{b} takes
the value 0, the expression \mzninline{ub(x)*(1-b)} is equal to
\mzninline{ub(x)}, and the constraint \mzninline{x <= ub(x)} holds trivially.
If \mzninline{b} takes the value 1, \mzninline{ub(x)*(1-b)} is equal to 0,
enforcing the constraint \mzninline{x <= 0}.
initial upper bound \mzninline{x} was declared with or the current value
adjusted by the \minizinc\ compiler. If \mzninline{b} takes the value 0, the
expression \mzninline{ub(x)*(1-b)} is equal to \mzninline{ub(x)}, and the
constraint \mzninline{x <= ub(x)} holds trivially. If \mzninline{b} takes the
value 1, \mzninline{ub(x)*(1-b)} is equal to 0, enforcing the constraint
\mzninline{x <= 0}.
\end{example}
For \gls{mip} solvers, it is quite important to enforce tight bounds in order to