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

Incorporate Peter's feedback

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-26 11:44:31 +10:00
parent 87c059609a
commit b94eb66e12
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
10 changed files with 117 additions and 109 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
assets/acronyms.tex
View File

@ -4,7 +4,7 @@
\newacronym[see={[Glossary:]{gls-ast}}]{ast}{AST\glsadd{gls-ast}}{Abstract Syntax Tree} \newacronym[see={[Glossary:]{gls-ast}}]{ast}{AST\glsadd{gls-ast}}{Abstract Syntax Tree}
\newacronym[see={[Glossary:]{gls-cbc}}]{cbc}{CBC}{COIN-OR Branch-and-Cut} \newacronym[see={[Glossary:]{gls-cbc}}]{cbc}{CBC\glsadd{gls-cbc}}{COIN-OR Branch-and-Cut}
\newacronym[see={[Glossary:]{gls-cbls}}]{cbls}{CBLS\glsadd{gls-cbls}}{Constraint-Based Local Search} \newacronym[see={[Glossary:]{gls-cbls}}]{cbls}{CBLS\glsadd{gls-cbls}}{Constraint-Based Local Search}

44
assets/bibliography/references.bib
View File

@ -230,6 +230,17 @@
version = {0.10.3}, version = {0.10.3},
} }
@phdthesis{chu-2011-chuffed,
author = {Geoffrey Chu},
title = {Improving Combinatorial Optimization},
school = {University of Melbourne, Australia},
year = {2011},
url = {http://hdl.handle.net/11343/36679},
timestamp = {Thu, 28 Nov 2019 09:33:38 +0100},
biburl = {https://dblp.org/rec/phd/basesearch/Chu11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@inproceedings{choi-2006-fin-cons, @inproceedings{choi-2006-fin-cons,
author = {Chiu Wo Choi and Warwick Harvey and J. H. M. Lee and Peter J. author = {Chiu Wo Choi and Warwick Harvey and J. H. M. Lee and Peter J.
Stuckey}, Stuckey},
@ -518,14 +529,6 @@
doi = {10.1016/S0743-1066(98)10005-5}, doi = {10.1016/S0743-1066(98)10005-5},
} }
@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},
}
@article{gebser-2012-clasp, @article{gebser-2012-clasp,
author = {Martin Gebser and Benjamin Kaufmann and Torsten Schaub}, author = {Martin Gebser and Benjamin Kaufmann and Torsten Schaub},
title = {Conflict-driven answer set solving: From theory to practice}, title = {Conflict-driven answer set solving: From theory to practice},
@ -723,14 +726,16 @@
year = {2020}, year = {2020},
} }
@inbook{lodi-2013-variability, @incollection{lodi-2013-variability,
author = {Andrea Lodi and Andrea Tramontani}, author = {Andrea Lodi and Andrea Tramontani},
title = {Performance Variability in Mixed-Integer Programming}, title = {Performance Variability in Mixed-Integer Programming},
booktitle = {Theory Driven by Influential Applications}, booktitle = {Theory Driven by Influential Applications},
chapter = {Chapter 1}, series = {INFORMS TutORials in Operations Research},
chapter = 1,
year = 2013, year = 2013,
pages = {1-12}, pages = {1-12},
doi = {10.1287/educ.2013.0112}, doi = {10.1287/educ.2013.0112},
isbn = {978-0-9843378-4-2},
URL = {https://pubsonline.informs.org/doi/abs/10.1287/educ.2013.0112}, URL = {https://pubsonline.informs.org/doi/abs/10.1287/educ.2013.0112},
eprint = {https://pubsonline.informs.org/doi/pdf/10.1287/educ.2013.0112}, eprint = {https://pubsonline.informs.org/doi/pdf/10.1287/educ.2013.0112},
} }
@ -1108,6 +1113,13 @@
doi = {10.1145/1452044.1452046}, doi = {10.1145/1452044.1452046},
} }
@manual{schulte-2019-gecode,
author = {Christian Schulte and Guido Tack and Mikael Z. Lagerkvist},
title = {Modeling and Programming with Gecode},
year = 2019,
url = {https://www.gecode.org/doc/6.2.0/MPG.pdf},
}
@inproceedings{schutt-2009-cumulative, @inproceedings{schutt-2009-cumulative,
author = {Andreas Schutt and Thibaut Feydy and Peter J. Stuckey and Mark author = {Andreas Schutt and Thibaut Feydy and Peter J. Stuckey and Mark
Wallace}, Wallace},
@ -1268,12 +1280,14 @@
publisher = {Taylor \& Francis}, publisher = {Taylor \& Francis},
} }
@article{warren-1983-wam, @techreport{warren-1983-wam,
title = {An abstract Prolog instruction set}, author = {Warren, David H. D.},
author = {Warren, David HD}, title = {An Abstract Prolog Instruction Set},
journal = {Technical note 309}, institution = {AI Center, SRI International},
month = 10,
number = 309,
year = 1983, year = 1983,
publisher = {SRI International}, KEYWORDS = {Prolog},
} }
@book{wolsey-1988-mip, @book{wolsey-1988-mip,

12
assets/glossary.tex
View File

@ -104,7 +104,7 @@
\newglossaryentry{chuffed}{ \newglossaryentry{chuffed}{
name={Chuffed}, name={Chuffed},
description={A well-known open source \gls{lcg} \gls{solver} \autocite{chuffed-2021-chuffed}.}, description={A well-known open source \gls{lcg} \gls{solver} \autocite{chuffed-2021-chuffed,chu-2011-chuffed}.},
} }
\newglossaryentry{comprehension}{ \newglossaryentry{comprehension}{
@ -244,7 +244,7 @@
\newglossaryentry{gecode}{ \newglossaryentry{gecode}{
name={Gecode}, name={Gecode},
description={A well-known open source \gls{cp} \gls{solver} \autocite{gecode-2021-gecode}.}, description={A well-known open source \gls{cp} \gls{solver} \autocite{schulte-2019-gecode}.},
} }
\newglossaryentry{generator}{ \newglossaryentry{generator}{
@ -307,7 +307,7 @@
} }
\newglossaryentry{kleene-sem}{ \newglossaryentry{kleene-sem}{
name={Kleene semantic}, name={Kleene semantics},
description={ description={
A semantic model for treating undefined behaviour in \glspl{cml}. A semantic model for treating undefined behaviour in \glspl{cml}.
Under Kleene semantics an occurrence of undefined behaviour will only cause its surrounding expression to be undefined when its value is required to compute its result. Under Kleene semantics an occurrence of undefined behaviour will only cause its surrounding expression to be undefined when its value is required to compute its result.
@ -510,7 +510,7 @@
} }
\newglossaryentry{strict-sem}{ \newglossaryentry{strict-sem}{
name={strict semantic}, name={strict semantics},
description={ description={
A semantic model for treating undefined behaviour in \glspl{cml}. A semantic model for treating undefined behaviour in \glspl{cml}.
Under strict semantics any occurrence of undefined behaviour will cause the result of the \gls{instance} to be undefined. Under strict semantics any occurrence of undefined behaviour will cause the result of the \gls{instance} to be undefined.
@ -567,10 +567,10 @@
} }
\newglossaryentry{rel-sem}{ \newglossaryentry{rel-sem}{
name={relational semantic}, name={relational semantics},
description={ description={
A semantic model for treating undefined behaviour in \glspl{cml}. A semantic model for treating undefined behaviour in \glspl{cml}.
Under relational semantics an occurrence of undefined behaviour will cause its closest surrounding Boolean expression to be \mzninline{false}. Under relational semantics an occurrence of undefined behaviour will cause its closest surrounding Boolean expression to be false.
} }
} }

12
chapters/1_introduction.tex
View File

@ -32,7 +32,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{}. 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 \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 class \gls{rewriting}. The \instance{} is transformed into a \gls{slv-mod} through a process called \gls{rewriting}.
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{}.
@ -74,7 +74,7 @@ Although they do support the rewriting of models between different problem class
They do not provide any way to capture common concepts. They do not provide any way to capture common concepts.
And, apart from changing the implementation of \glsxtrshort{opl} or \gls{essence}, the \solver{} is unable to influence their preferred encoding. And, apart from changing the implementation of \glsxtrshort{opl} or \gls{essence}, the \solver{} is unable to influence their preferred encoding.
\gls{clp}, as used in the Prolog language, offers a very different mechanism to create a \cmodel{}. \gls{clp}, as used for example in the Sictus Prolog language \autocite{carlsson-1997-sicstus}, offers a very different mechanism to create a \cmodel{}.
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{}. 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{}.
For example, the concepts of one task preceding another and non-overlapping of tasks could be defined in Prolog as: For example, the concepts of one task preceding another and non-overlapping of tasks could be defined in Prolog as:
@ -98,7 +98,7 @@ The definition of \mzninline{nonoverlap} requires that either task A precedes ta
However, unlike the \glsxtrshort{ampl} model, Prolog would not provide this choice to the \solver{}. However, unlike the \glsxtrshort{ampl} model, Prolog would not provide this choice to the \solver{}.
Instead, it enforces one, test if this works, and it otherwise enforces the other. Instead, it enforces one, test if this works, and it otherwise enforces the other.
This is a powerful mechanism where any 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. Additionally, \solvers{} are 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.
@ -141,7 +141,7 @@ 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 surfaced certain problems. 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{}. 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. 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{}. For many applications, \minizinc{} now requires a significant, and sometimes prohibitive, amount of time to rewrite \instances{}.
@ -228,9 +228,9 @@ Overall, this thesis makes the following contributions.
\begin{enumerate} \begin{enumerate}
\item It presents a formal execution model of rewriting of 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.
\item It provides a novel method of tracking of \constraints{} created as part of functional dependencies, ensuring the correct removal of unused dependencies. \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 \constraints{} should be considered. \item It presents an analysis technique to reason about in what (\gls{reified}) form \constraints{} should be considered.

78
chapters/2_background.tex
View File

@ -47,7 +47,7 @@ This process is visualized in \cref{fig:back-cml-flow}.
As an example, let us consider the following scenario: Packing for a weekend trip, I have to decide which toys to bring for my dog, Audrey. As an example, let us consider the following scenario: Packing for a weekend trip, I have to decide which toys to bring for my dog, Audrey.
We only have a small amount of space left in the car, so we cannot bring all the toys. We only have a small amount of space left in the car, so we cannot bring all the toys.
Since Audrey enjoys playing with some toys more than others, we try and pick the toys that bring Audrey the most amount of joy, but still fit in the car. Since Audrey enjoys playing with some toys more than others, we try to pick the toys that bring Audrey the most amount of joy, but still fit in the car.
The following set of equations describes this ``knapsack'' problem as an \gls{opt-prb}: The following set of equations describes this ``knapsack'' problem as an \gls{opt-prb}:
\begin{equation*} \begin{equation*}
@ -322,7 +322,7 @@ If the arguments to a function consist of only \parameters{}, then the result of
However, \gls{rewriting} functions with \variable{} as arguments results in a new \variable{} that is constrained to the result of the function. However, \gls{rewriting} functions with \variable{} as arguments results in a new \variable{} that is constrained to the result of the function.
\paragraph{Conditional Expression} The choice between different expressions is often expressed using a \gls{conditional} expression, also known as an ``if-then-else'' expression. \paragraph{Conditional Expression} The choice between different expressions is often expressed using a \gls{conditional} expression, also known as an ``if-then-else'' expression.
It can, for example, force that the absolute value of \mzninline{a} is bigger than \mzninline{b} using the \constraint{} as follows. It can, for example, force that the absolute value of \mzninline{a} is larger than \mzninline{b} using the \constraint{} as follows.
\begin{mzn} \begin{mzn}
constraint if a >= 0 then a > b else b < a endif; constraint if a >= 0 then a > b else b < a endif;
@ -358,7 +358,7 @@ The generation of new \gls{array} structures allows modellers adjust, combine, f
\begin{description} \begin{description}
\item[\(G\)] The \gls{generator} expression which assigns the values of collections to identifiers, \item[\(G\)] The \gls{generator} expression which assigns the values of collections to identifiers,
\item[\(F\)] an optional filtering condition, which has to evaluate to \mzninline{true} for the iteration to be included in the \gls{array}, \item[\(F\)] an optional filtering condition, which has to evaluate to true for the iteration to be included in the \gls{array},
\item[\(E\)] and the expression that is evaluated for each iteration when the filtering condition succeeds. \item[\(E\)] and the expression that is evaluated for each iteration when the filtering condition succeeds.
\end{description} \end{description}
@ -419,7 +419,7 @@ Any item or expression can be annotated.
An annotation is indicated by the \mzninline{::} \gls{operator} followed by an identifier or function call. An annotation is indicated by the \mzninline{::} \gls{operator} followed by an identifier or function call.
The same syntax can be repeated to place multiple \glspl{annotation} on the same item or expression. The same syntax can be repeated to place multiple \glspl{annotation} on the same item or expression.
A common use of \glspl{annotation} in \minizinc{} is to provide a search heuristic. A common use of \glspl{annotation} in \minizinc{} is to provide a \gls{search-heuristic}.
Through the use of an \gls{annotation} on the solving goal item, the modeller can express an order in which they think values should be tried for an arrangement of \variables{} in the model. Through the use of an \gls{annotation} on the solving goal item, the modeller can express an order in which they think values should be tried for an arrangement of \variables{} in the model.
\subsection{Reification}% \subsection{Reification}%
@ -444,7 +444,7 @@ The \gls{reif} of a \constraint{} \(c\) creates a Boolean \gls{avar} \mzninline{
This means that for each \mzninline{i}, a \gls{cvar} \mzninline{b_i} is added, together with a constraint that makes \mzninline{b_i} true if-and-only-if \mzninline{x[i] mod 2 = 0}. This means that for each \mzninline{i}, a \gls{cvar} \mzninline{b_i} is added, together with a constraint that makes \mzninline{b_i} true if-and-only-if \mzninline{x[i] mod 2 = 0}.
We can then add up the values of all these \mzninline{b_i}, as required by the maximization. We can then add up the values of all these \mzninline{b_i}, as required by the maximization.
Since the elements have a domain from 1 to 15 and are constrained to take different values, not all elements of \mzninline{x} can take even values. Since the elements have a domain from 1 to 15 and are constrained to take different values, not all elements of \mzninline{x} can take even values.
Instead, the solver is tasked to maximize the number of reified variables it sets to \mzninline{true}. Instead, the \solver{} is tasked to maximize the number of reified variables it sets to true.
\end{example} \end{example}
When an expression occurs in a position where it can be directly enforced, we say it occurs in \rootc{} context. When an expression occurs in a position where it can be directly enforced, we say it occurs in \rootc{} context.
@ -457,7 +457,7 @@ In \minizinc{}, almost all expressions can be used in both \rootc{} and non-\roo
In this subsection we discuss the handling of \gls{partial} functions in \cmls{} as studied by \textcite{frisch-2009-undefinedness}. In this subsection we discuss the handling of \gls{partial} functions in \cmls{} as studied by \textcite{frisch-2009-undefinedness}.
When a function has a well-defined result for all its possible inputs it is said to be total. When a function has a well-defined result for all its possible inputs it is said to be total.
Some expression in \cmls{}, however, are rewritten into functions that do not have well-defined results for all possible inputs. Some expressions in \cmls{}, however, are rewritten into functions that do not have well-defined results for all possible inputs.
Part of the semantics of a \cml{} is the choice as to how to treat these \gls{partial} functions. Part of the semantics of a \cml{} is the choice as to how to treat these \gls{partial} functions.
\begin{example}\label{ex:back-undef} \begin{example}\label{ex:back-undef}
@ -470,7 +470,7 @@ Part of the semantics of a \cml{} is the choice as to how to treat these \gls{pa
\noindent{}It requires that if \mzninline{i} takes a value less or equal to four, then the value in the \texttt{i}\(^{th}\) position of \gls{array} \mzninline{a} multiplied by \mzninline{x} must be at least six. \noindent{}It requires that if \mzninline{i} takes a value less or equal to four, then the value in the \texttt{i}\(^{th}\) position of \gls{array} \mzninline{a} multiplied by \mzninline{x} must be at least six.
Suppose the \gls{array} \texttt{a} has index set \mzninline{1..5}, but \mzninline{i} takes the value seven. Suppose the \gls{array} \texttt{a} has index set \mzninline{1..5}, but \mzninline{i} takes the value seven.
This means the expression \mzninline{a[i]} undefined. This means the expression \mzninline{a[i]} is undefined.
If \minizinc{} did not implement any special handling for \gls{partial} functions, then the whole expression would have to be marked as undefined and a \gls{sol} cannot be found. If \minizinc{} did not implement any special handling for \gls{partial} functions, then the whole expression would have to be marked as undefined and a \gls{sol} cannot be found.
However, intuitively if \mzninline{i = 7} the \constraint{} should be trivially true. However, intuitively if \mzninline{i = 7} the \constraint{} should be trivially true.
\end{example} \end{example}
@ -509,33 +509,33 @@ There is both the question of what happens when an undefined expression is evalu
If during the \gls{rewriting} or solving process an expression is found to be undefined, then any expressions in which it is used is also marked as undefined. If during the \gls{rewriting} or solving process an expression is found to be undefined, then any expressions in which it is used is also marked as undefined.
Consequently, this means that the occurrence of a single undefined expression causes the full \instance{} to be undefined. Consequently, this means that the occurrence of a single undefined expression causes the full \instance{} to be undefined.
\item[Kleene] The \gls{kleene-sem} treats undefined expressions as expressions for which not enough information is available. \item[Kleene] The \Gls{kleene-sem} treat undefined expressions as expressions for which not enough information is available.
If an expression contains an undefined sub-expression, then it is only marked as undefined if the value of the sub-expression is required to compute its result. If an expression contains an undefined sub-expression, then it is only marked as undefined if the value of the sub-expression is required to compute its result.
Take for example the expression \mzninline{false -> @\(E\)@}. Take for example the expression \mzninline{false -> @\(E\)@}.
When \(E\) is undefined the result of the expression is still be said to be \mzninline{true}, since the value of \(E\) does not influence the result of the expression. When \(E\) is undefined the result of the expression is still be said to be true, since the value of \(E\) does not influence the result of the expression.
However, if we take the expression \mzninline{true /\ @\(E\)@}, then when \(E\) is undefined the overall expression is also undefined since the value of the expression cannot be determined. However, if we take the expression \mzninline{true /\ @\(E\)@}, then when \(E\) is undefined the overall expression is also undefined since the value of the expression cannot be determined.
\item[Relational] The \gls{rel-sem} follows from all expressions in a \cml{} eventually becoming part of a relational \constraint{}. \item[Relational] The \gls{rel-sem} follow from all expressions in a \cml{} eventually becoming part of a relational \constraint{}.
So even though a (functional) expression does not have a well-defined result, we can still decide whether its surrounding relation holds. So even though a (functional) expression does not have a well-defined result, we can still decide whether its surrounding relation holds.
For example, the expression \mzninline{x div 0} is undefined, but the relation \mzninline{int_div(x, 0, y)} is said to be \mzninline{false}. For example, the expression \mzninline{x div 0} is undefined, but the relation \mzninline{int_div(x, 0, y)} is said to be false.
Values for \mzninline{x} and \mzninline{y} such that the relation holds do not exist. Values for \mzninline{x} and \mzninline{y} such that the relation holds do not exist.
It can be said that the relational semantic makes the closest relational expression that contains an undefined expression \mzninline{false}. It can be said that the relational semantic makes the closest relational expression that contains an undefined expression false.
\end{description} \end{description}
In practice, it is often natural to guard against undefined behaviour using Boolean logic. In practice, it is often natural to guard against undefined behaviour using Boolean logic.
\Glspl{rel-sem} therefore often feel the most natural for the users of \glspl{cml}. \Gls{rel-sem} therefore often feel the most natural for the users of \glspl{cml}.
This is why \minizinc{} uses \glspl{rel-sem} during its evaluation. This is why \minizinc{} uses \gls{rel-sem} during its evaluation.
If we, for example, reconsider the \constraint{} from \cref{ex:back-undef}, we will find that \glspl{rel-sem} will correspond to the intuitive expectation. If we, for example, reconsider the \constraint{} from \cref{ex:back-undef}, we will find that \gls{rel-sem} will correspond to the intuitive expectation.
When \mzninline{i} takes the value seven, the expression \mzninline{a[i]} is undefined. When \mzninline{i} takes the value seven, the expression \mzninline{a[i]} is undefined.
Its closest Boolean context will take the value false. Its closest Boolean context will take the value false.
In this case, that means the right-hand side of the implication becomes false. In this case, that means the right-hand side of the implication becomes false.
However, since the left-hand side of the implication is also false, the \constraint{} is \gls{satisfied}. However, since the left-hand side of the implication is also false, the \constraint{} is \gls{satisfied}.
\textcite{frisch-2009-undefinedness} also show that different \solvers{} often employ different semantics. \textcite{frisch-2009-undefinedness} also show that different \solvers{} often employ different semantics.
\minizinc{} therefore implements the \glspl{rel-sem} by translating any potentially undefined expression into an expression that is always defined, by introducing appropriate \glspl{avar} and \gls{reified} \constraints{}. \minizinc{} therefore implements the \gls{rel-sem} by translating any potentially undefined expression into an expression that is always defined, by introducing appropriate \glspl{avar} and \gls{reified} \constraints{}.
That way, the solving result is independent of the semantics of the chosen \solver{}, and always consistent with the \glspl{rel-sem} of the model. That way, the solving result is independent of the semantics of the chosen \solver{}, and always consistent with the \gls{rel-sem} of the model.
\section{Solving Constraint Models}% \section{Solving Constraint Models}%
\label{sec:back-solving} \label{sec:back-solving}
@ -697,7 +697,7 @@ If the search process finds another \gls{sol}, then the incumbent \gls{sol} is u
If the search process does not find any other \glspl{sol}, then it is proven that a better \gls{sol} than the current incumbent \gls{sol} cannot exist. If the search process does not find any other \glspl{sol}, then it is proven that a better \gls{sol} than the current incumbent \gls{sol} cannot exist.
It is an \gls{opt-sol}. It is an \gls{opt-sol}.
\gls{cp} solvers like \gls{chuffed} \autocite{chuffed-2021-chuffed}, Choco \autocite{prudhomme-2016-choco}, \gls{gecode} \autocite{gecode-2021-gecode}, and OR-Tools \autocite{perron-2021-ortools} have long been one of the leading methods to solve \minizinc\ instances. \gls{cp} solvers like \gls{chuffed} \autocite{chu-2011-chuffed}, Choco \autocite{prudhomme-2016-choco}, \gls{gecode} \autocite{schulte-2019-gecode}, and OR-Tools \autocite{perron-2021-ortools} have long been one of the leading methods to solve \minizinc\ instances.
\subsection{Mathematical Programming}% \subsection{Mathematical Programming}%
\label{subsec:back-mip} \label{subsec:back-mip}
@ -721,7 +721,7 @@ The vectors \(l\) and \(u\) respectively contain the lower and upper bounds of t
Finally, the \variables{} of the linear program are held in the \(x\) vector. Finally, the \variables{} of the linear program are held in the \(x\) vector.
For problems that are in the form of a linear program, there are proven methods to find an \gls{opt-sol}. For problems that are in the form of a linear program, there are proven methods to find an \gls{opt-sol}.
One such method, the simplex method, was first conceived by \textcite{dantzig-1955-simplex} during the second world war. One such method, the simplex method, was first conceived by \textcite{dantzig-1955-simplex} after the second world war.
It finds the optimal solution of a linear program in worst-case exponential time. It finds the optimal solution of a linear program in worst-case exponential time.
It was questioned whether the same problem could be solved in worst-case polynomial time, until \textcite{karmarkar-1984-interior-point} proved this possible through the use of interior point methods. It was questioned whether the same problem could be solved in worst-case polynomial time, until \textcite{karmarkar-1984-interior-point} proved this possible through the use of interior point methods.
@ -754,7 +754,7 @@ It does, however, come with its challenges.
Many \minizinc{} models contain \constraint{} that are not linear (in-)equations. Many \minizinc{} models contain \constraint{} that are not linear (in-)equations.
The translation of a single such \constraint{} can introduce many linear \constraints{} and \glspl{avar}. The translation of a single such \constraint{} can introduce many linear \constraints{} and \glspl{avar}.
For example, when a \constraint{} reasons about the value that a variable takes, the \gls{linearization} process introduces indicator variables. For example, when a \constraint{} reasons about the value that a variable takes, the \gls{linearization} process introduces indicator variables.
The indicator variables \(y_{i}\) are \gls{avar} that for a \variable{} \(x\) take the value 1 if \(x = i\) and 0 otherwise. An indicator variable \(y_{i}\) is a \gls{avar} that for a \variable{} \(x\) take the value 1 if \(x = i\) and 0 otherwise.
\Constraints{} reasoning about the value of \(x\) are then rewritten as linear \constraints{} using the \variables{} \(y_{i}\). \Constraints{} reasoning about the value of \(x\) are then rewritten as linear \constraints{} using the \variables{} \(y_{i}\).
\begin{example} \begin{example}
@ -978,9 +978,8 @@ When solving a scheduling problem, \gls{opl} makes use of specialized interval \
\end{listing} \end{listing}
A fragment of a \minizinc{} model, modelling the same parts of the job shop problem, is shown in \cref{lst:back-mzn-jsp}. A fragment of a \minizinc{} model, modelling the same parts of the job shop problem, is shown in \cref{lst:back-mzn-jsp}.
Notably, \minizinc{} does not have explicit activity \variables{}. Notably, \minizinc{} does not have explicit activity \variables{}.
It instead uses integer \variables{} that represent the start times of the tasks and the time at which all tasks are finished. It instead uses integer \variables{} that represent the start times of the tasks and the end time for the \mzninline{makespan} activity that spans all tasks.
This means that much of the implicit behaviour of the \texttt{Activity} \variables{} has to be defined explicitly. This means that much of the implicit behaviour of the \texttt{Activity} \variables{} has to be defined explicitly.
Where in the \gls{opl} model we could just state a global scheduling horizon, in \minizinc{} it has to be explicitly included in the \domains{} of the time \variables{}. Where in the \gls{opl} model we could just state a global scheduling horizon, in \minizinc{} it has to be explicitly included in the \domains{} of the time \variables{}.
And, instead of a \texttt{precedes} operator, we have to explicitly enforce the precedence of tasks using linear \constraints{}. And, instead of a \texttt{precedes} operator, we have to explicitly enforce the precedence of tasks using linear \constraints{}.
@ -1018,7 +1017,7 @@ Instead, \gls{opl} now offers the use of ``search phases'', which function simil
\label{sub:back-essence} \label{sub:back-essence}
\gls{essence} \autocite{frisch-2007-essence} is another high-level \cml{}. \gls{essence} \autocite{frisch-2007-essence} is another high-level \cml{}.
It is cherished for its adoption of high-level \variable{} types. It is notable for its adoption of high-level \variable{} types.
In addition to all variable types that are supported by \minizinc{}, \gls{essence} also contains: In addition to all variable types that are supported by \minizinc{}, \gls{essence} also contains:
\begin{itemize} \begin{itemize}
@ -1117,7 +1116,7 @@ Consequently, this research reiterates the use of \gls{meta-optimization} algori
At the heart of the \gls{rewriting} process that transforms a \minizinc{} \instance{} into a \gls{slv-mod}, lies a \gls{trs}. At the heart of the \gls{rewriting} process that transforms a \minizinc{} \instance{} into a \gls{slv-mod}, lies a \gls{trs}.
A \gls{trs} describes a computational model. A \gls{trs} describes a computational model.
The full process can be described 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}\) \autocite{baader-1998-term-rewriting}. The full process can be described as the application of rules \(l \rightarrow r_{1}, \ldots, r_{n}\), that replace a \gls{term} \(l\) with \(n \geq{} 1\) \glspl{term} \(r_{1}, \ldots, r_{n}\) \autocite{baader-1998-term-rewriting}.
A \gls{term} is an expression with nested sub-expressions consisting of function and constant symbols. A \gls{term} is an expression with nested sub-expressions consisting of function and 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. 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 term variable, which captures a term sub-expression. In a term rewriting rule, a term can also contain a term variable, which captures a term sub-expression.
@ -1305,11 +1304,6 @@ Enforced by \minizinc{}'s type system, at most one rule applies for any given \c
The \gls{rewriting} of expressions is performed bottom-up, we rewrite any sub-expression before its parent expression. The \gls{rewriting} of expressions is performed bottom-up, we rewrite any sub-expression before its parent expression.
For instance, in a call each argument is rewritten before the call itself is rewritten. For instance, in a call each argument is rewritten before the call itself is rewritten.
An exception to this bottom-up approach is the \gls{rewriting} of \glspl{comprehension}.
\glspl{comprehension} have to be instantiated before their sub-expression is rewritten.
The compiler exhaustively binds the values of the \gls{generator} to the specified identifiers.
For each iteration the compiler rewrites the sub-expression and collects its result.
An exception to this bottom-up approach is the \gls{rewriting} of \glspl{comprehension} \mzninline{[@\(E\)@ | @\(i\)@ in @\(S\)@ where @\(F\)@]}. An exception to this bottom-up approach is the \gls{rewriting} of \glspl{comprehension} \mzninline{[@\(E\)@ | @\(i\)@ in @\(S\)@ where @\(F\)@]}.
\Gls{rewriting} \(E\) requires instantiating the identifier \(i\) with the values from the set \(S\), and evaluating the condition \(W\). \Gls{rewriting} \(E\) requires instantiating the identifier \(i\) with the values from the set \(S\), and evaluating the condition \(W\).
The \compiler{} therefore iterates through all values in \(S\), binds the values to the specified identifier(s), and rewrites the condition \(F\). The \compiler{} therefore iterates through all values in \(S\), binds the values to the specified identifier(s), and rewrites the condition \(F\).
@ -1334,7 +1328,7 @@ The creation of this \gls{avar} and defining \constraints{} happens in one of tw
To constrain this \gls{avar}, the \compiler{} then adds the \gls{reif} of the \constraint{}. To constrain this \gls{avar}, the \compiler{} then adds the \gls{reif} of the \constraint{}.
This \constraint{} contains a variation of the call that would have been generated for the expression in \rootc{} context. This \constraint{} contains a variation of the call that would have been generated for the expression in \rootc{} context.
The name of the function is appended with \mzninline{_reif} and an extra Boolean \variable{} argument is added to the call. The name of the function is appended with \mzninline{_reif} and an extra Boolean \variable{} argument is added to the call.
The definition of this \constraint{} should implement the \gls{reif} of the original expression: setting the additional argument to \mzninline{true} if the \constraint{} is \gls{satisfied}, and \mzninline{false} otherwise. The definition of this \constraint{} should implement the \gls{reif} of the original expression: setting the additional argument to true if the \constraint{} is \gls{satisfied}, and false otherwise.
For example, consider the following \minizinc{} \constraint{}. For example, consider the following \minizinc{} \constraint{}.
\begin{mzn} \begin{mzn}
@ -1427,28 +1421,28 @@ However, the expression defining \mzninline{y}, \mzninline{pow(i, 2)}, is then f
In either case, it can be very beneficial for the efficiency of the solving process if we detect that a \gls{reified} \constraint{} is in fact not required. In either case, it can be very beneficial for the efficiency of the solving process if we detect that a \gls{reified} \constraint{} is in fact not required.
If a \constraint{} is present in the \rootc{} context, it means that it must hold globally. If a \constraint{} is present in the \rootc{} context, it means that it must hold globally.
If the same \constraint{} is used in a non-\rootc{} context, \gls{cse} can then replace them with the constant \mzninline{true}, avoiding the need for \gls{reif} (or in fact any evaluation). If the same \constraint{} is used in a non-\rootc{} context, \gls{cse} can then replace them with the constant true, avoiding the need for \gls{reif} (or in fact any evaluation).
We harness \gls{cse} to store the evaluation context when a \constraint{} is added, and detect when the same \constraint{} is used in both contexts. We harness \gls{cse} to store the evaluation context when a \constraint{} is added, and detect when the same \constraint{} is used in both contexts.
Whenever a lookup in the \gls{cse} table is successful, action is taken depending on both the current and stored evaluation context. Whenever a lookup in the \gls{cse} table is successful, action is taken depending on both the current and stored evaluation context.
If the stored expression was in \rootc{} context, then the constant \mzninline{true} is used, independent of the current context. If the stored expression was in \rootc{} context, then the constant true is used, independent of the current context.
Otherwise, if the stored expression was in non-\rootc{} context and the current context is non-\rootc{}, then the stored result variable is used. Otherwise, if the stored expression was in non-\rootc{} context and the current context is non-\rootc{}, then the stored result variable is used.
Finally, if the stored expression was in non-\rootc{} context and the current context is \rootc{} context, then the previous result is replaced by the constant \mzninline{true} and the evaluation proceeds as normal with the \rootc{} context \constraint{}. Finally, if the stored expression was in non-\rootc{} context and the current context is \rootc{} context, then the previous result is replaced by the constant true and the evaluation proceeds as normal with the \rootc{} context \constraint{}.
\begin{example} \begin{example}
Consider the fragment: Consider the following \minizinc{} fragment.
\begin{mzn} \begin{mzn}
function var bool: p(var int: x, var int: y) = q(x) /\ r(y);
constraint b0 <-> q(x); constraint b0 <-> q(x);
constraint b1 <-> t(x,y); constraint b1 <-> t(x,y);
function var bool: p(var int: x, var int: y) = q(x) /\ r(y);
constraint b1 <-> p(x,y); constraint b1 <-> p(x,y);
\end{mzn} \end{mzn}
If we process the \constraints{} in order we create a reified call to \mzninline{q(x)} for the original call. If we process the \constraints{} in order, we create a \gls{reified} call to \mzninline{q(x)} when \gls{rewriting} the first \constraint{}.
Suppose processing the second \constraint{} we discover \mzninline{t(x,y)} is \mzninline{true}, fixing \mzninline{b1}. Suppose when we rewrite the second \constraint{}, we discover \mzninline{t(x,y)} is true, fixing \mzninline{b1}.
When we then process \mzninline{q(x)} in instantiation of the call \mzninline{p(x,y)}, it is in the \rootc{} context. When we then process \mzninline{q(x)} in instantiation of the call \mzninline{p(x,y)}, it is in the \rootc{} context.
So \gls{cse} needs to set \mzninline{b0} to \mzninline{true}. So \gls{cse} needs to set \mzninline{b0} to true.
\end{example} \end{example}
\subsection{Constraint Propagation}% \subsection{Constraint Propagation}%
@ -1482,13 +1476,13 @@ Finally, it can also be helpful for \solvers{} as they may need to decide on a r
If we however consider the first \constraint{}, then we deduce that \mzninline{a} must always take a value that is 4 or lower. If we however consider the first \constraint{}, then we deduce that \mzninline{a} must always take a value that is 4 or lower.
When the compiler adjusts the domain of \mzninline{a} while \gls{rewriting} the first \constraint{}, then the second \constraint{} can be simplified. When the compiler adjusts the domain of \mzninline{a} while \gls{rewriting} the first \constraint{}, then the second \constraint{} can be simplified.
The expression \mzninline{a > 5} is known to be \mzninline{false}, which means that the \constraint{} is simplified to \mzninline{true}. The expression \mzninline{a > 5} is known to be false, which means that the \constraint{} is simplified to true.
\end{example} \end{example}
During \gls{rewriting}, the \minizinc{} compiler actively removes values from the \domain{} when it encounters \constraints{} that trivially reduce it. During \gls{rewriting}, the \minizinc{} compiler actively removes values from the \domain{} when it encounters \constraints{} that trivially reduce it.
For example, it detects \constraints{} with a single comparison expression between a \variable{} and a \parameter{} (\eg\ \mzninline{x != 5}), \constraints{} with a single comparison between two \variables{} (\eg\ \mzninline{x >= y}), \constraints{} that directly change the domain (\eg\ \mzninline{x in 3..5}). For example, it detects \constraints{} with a single comparison expression between a \variable{} and a \parameter{} (\eg\ \mzninline{x != 5}), \constraints{} with a single comparison between two \variables{} (\eg\ \mzninline{x >= y}), \constraints{} that directly change the domain (\eg\ \mzninline{x in 3..5}).
It even performs more complex \gls{propagation} for some known \constraints{}. It even performs more complex \gls{propagation} for some known \constraints{}.
For example, it will reduce the \domains{} for \mzninline{int_times} and \mzninline{int_div}, and we will see in the next subsection how \gls{aggregation} will help simplify certain \constraint{}. For example, it will reduce the \domains{} for \mzninline{int_times} and \mzninline{int_div}, and we will see in the next subsection how \gls{aggregation} will help simplify certain \constraints{}.
However, \gls{propagation} is only performed locally, when the \constraint{} is recognized. However, \gls{propagation} is only performed locally, when the \constraint{} is recognized.
During \gls{rewriting}, the \gls{propagation} of one \constraint{}, will not trigger the \gls{propagation} of another. During \gls{rewriting}, the \gls{propagation} of one \constraint{}, will not trigger the \gls{propagation} of another.
@ -1524,7 +1518,7 @@ It is therefore important that equalities are found early in the \gls{rewriting}
\subsection{Constraint Aggregation}% \subsection{Constraint Aggregation}%
\label{subsec:back-aggregation} \label{subsec:back-aggregation}
Complex \minizinc{} expressions sometimes result in the creation of many \gls{avar} to represent intermediate results. Complex \minizinc{} expressions sometimes result in the creation of many \glspl{avar} to represent intermediate results.
This is in particular true for linear and Boolean equations that are generally written using \minizinc{} operators. This is in particular true for linear and Boolean equations that are generally written using \minizinc{} operators.
\begin{example}% \begin{example}%
@ -1620,5 +1614,5 @@ This means that, depending on the target \solver{}, the \compiler{} will not be
It only understands the meaning of the standard \flatzinc{} \constraints{}, but not any of the \solver{} specific \gls{native} \constraints{}. It only understands the meaning of the standard \flatzinc{} \constraints{}, but not any of the \solver{} specific \gls{native} \constraints{}.
For the standard \flatzinc{} \constraints{}, it employs \gls{propagation} methods, as discussed in \cref{subsec:back-cp}, are used to eliminate values from \domains{} and simplify \constraints{}. For the standard \flatzinc{} \constraints{}, it employs \gls{propagation} methods, as discussed in \cref{subsec:back-cp}, are used to eliminate values from \domains{} and simplify \constraints{}.
In the current implementation, the \minizinc{} \compiler{} propagate mostly Boolean \constraints{} in this phase. In the current implementation, the \minizinc{} \compiler{} propagates mostly Boolean \constraints{} in this phase.
It tries to reduce the number of Boolean \variables{} and tries to reduce the number of literals in clauses and conjunctions. It tries to reduce the number of Boolean \variables{} and tries to reduce the number of literals in clauses and conjunctions.

4
chapters/3_rewriting.tex
View File

@ -528,12 +528,12 @@ The \constraints{} directly succeeding the declaration prepended by \texttt{↳}
constraint bool_or(b, c); constraint bool_or(b, c);
\end{nzn} \end{nzn}
Evaluating \mzninline{constraint c} has resulted in the domain of \mzninline{c} to be bound to \mzninline{true}. Evaluating \mzninline{constraint c} has resulted in the domain of \mzninline{c} to be bound to true.
The disjunction now trivially holds, independent of the value of \mzninline{b}. The disjunction now trivially holds, independent of the value of \mzninline{b}.
The \gls{reif} of \mzninline{abs(x) > y} is therefore not required. The \gls{reif} of \mzninline{abs(x) > y} is therefore not required.
However, the \gls{rewriting} has to choose a particular order in which arguments are evaluated, so it is always possible that it already evaluated the left-hand side before ``noticing'' that the disjunction is true. However, the \gls{rewriting} has to choose a particular order in which arguments are evaluated, so it is always possible that it already evaluated the left-hand side before ``noticing'' that the disjunction is true.
If the system now simplifies the \constraint{} \mzninline{bool_or(b, c)} to \mzninline{true}, then the identifier \mzninline{b} will become unused outside its attached \constraints{}. If the system now simplifies the \constraint{} \mzninline{bool_or(b, c)} to true, then the identifier \mzninline{b} will become unused outside its attached \constraints{}.
It was only referenced from the \mzninline{bool_or} call. It was only referenced from the \mzninline{bool_or} call.
Removing \mzninline{b} leads to its defining \constraint{}, \mzninline{int_gt_reif}, being removed. Removing \mzninline{b} leads to its defining \constraint{}, \mzninline{int_gt_reif}, being removed.
This in turn means that \mzninline{z} is not referenced anywhere outside its attached \constraints{}. This in turn means that \mzninline{z} is not referenced anywhere outside its attached \constraints{}.

26
chapters/4_half_reif.tex
View File

@ -20,7 +20,7 @@ The \gls{rewriting} process then enforces a \constraint{} \mzninline{pred_reif(.
\textcite{feydy-2011-half-reif} show that although using \gls{reif} in the \gls{rewriting} process is well-understood, it suffers from certain weaknesses. \textcite{feydy-2011-half-reif} show that although using \gls{reif} in the \gls{rewriting} process is well-understood, it suffers from certain weaknesses.
\begin{itemize} \begin{itemize}
\item Many \glspl{reif} are created in the \gls{rewriting} of \gls{partial} function calls to accommodate \minizinc{}'s \glspl{rel-sem}. \item Many \glspl{reif} are created in the \gls{rewriting} of \gls{partial} function calls to accommodate \minizinc{}'s \gls{rel-sem}.
\item \Glspl{propagator} for the \glspl{reif} of \glspl{global} are scarce. \item \Glspl{propagator} for the \glspl{reif} of \glspl{global} are scarce.
\end{itemize} \end{itemize}
@ -86,7 +86,7 @@ Since Boolean expressions in \minizinc{} can be used in, for example, integer ex
constraint count(x in arr)(x = 5) > 5; constraint count(x in arr)(x = 5) > 5;
\end{mzn} \end{mzn}
Making the left-hand side of the \constraint{} bigger will only ever help satisfy the \constraint{}. Making the left-hand side of the \constraint{} larger will only ever help satisfy the \constraint{}.
This means \mzninline{propagation} of the expressions \mzninline{x = 5} can never force them to take the value false. This means \mzninline{propagation} of the expressions \mzninline{x = 5} can never force them to take the value false.
The \gls{rewriting} process can thus use \glspl{half-reif} instead of \glspl{reif} for these expressions. The \gls{rewriting} process can thus use \glspl{half-reif} instead of \glspl{reif} for these expressions.
\end{example} \end{example}
@ -328,7 +328,7 @@ Although this would increase the use of \gls{half-reif}, it should be noted that
In this scenario, we prefer to create the full \gls{reif} as it decreases the number of \variables{} and \constraints{} in the model. In this scenario, we prefer to create the full \gls{reif} as it decreases the number of \variables{} and \constraints{} in the model.
When taking into account the possible undefinedness of an expression, every expression in a \minizinc{} model has two different contexts: the context in which the expression itself occurs, its \emph{value context}, and the context in which the partiality of the expression is captured, its \emph{partiality context}. When taking into account the possible undefinedness of an expression, every expression in a \minizinc{} model has two different contexts: the context in which the expression itself occurs, its \emph{value context}, and the context in which the partiality of the expression is captured, its \emph{partiality context}.
As described in \cref{subsec:back-mzn-partial}, \minizinc{} uses \glspl{rel-sem} for partial functions. As described in \cref{subsec:back-mzn-partial}, \minizinc{} uses \gls{rel-sem} for partial functions.
This means that if the result of a function is undefined, then its nearest enclosing Boolean expression becomes false. This means that if the result of a function is undefined, then its nearest enclosing Boolean expression becomes false.
In practice, this means that a condition that tests if the function will return a value is added to the nearest enclosing Boolean expression. In practice, this means that a condition that tests if the function will return a value is added to the nearest enclosing Boolean expression.
The partiality context is the context in which this condition is placed. The partiality context is the context in which this condition is placed.
@ -650,7 +650,7 @@ It is, however, not always safe to do so.
\end{mzn} \end{mzn}
One side of the \gls{conditional} expression is also used in a disjunction. One side of the \gls{conditional} expression is also used in a disjunction.
If \mzninline{b} evaluates to \mzninline{true}, then \mzninline{p} is evaluated in \rootc{} context, and \mzninline{p} can take the value \mzninline{true} in the disjunction. If \mzninline{b} evaluates to true, then \mzninline{p} is evaluated in \rootc{} context, and \mzninline{p} can take the value true in the disjunction.
Otherwise, \mzninline{q} is evaluated in \rootc{} context, and \mzninline{p} in the disjunction must be evaluated in \posc{} context. Otherwise, \mzninline{q} is evaluated in \rootc{} context, and \mzninline{p} in the disjunction must be evaluated in \posc{} context.
In this situation, it is not safe for the \compiler{} to output calls for the \rootc{} variants of these calls. In this situation, it is not safe for the \compiler{} to output calls for the \rootc{} variants of these calls.
\end{example} \end{example}
@ -696,7 +696,7 @@ Otherwise, it will act as a normal \rootc{} context.
\Cref{fig:half-analysis-maybe-root} shows the additional inference rules for \gls{array} access and \gls{conditional} expressions. \Cref{fig:half-analysis-maybe-root} shows the additional inference rules for \gls{array} access and \gls{conditional} expressions.
Looking back at \cref{ex:half-maybe-root}, these additional rules and updated join operation will ensure that the first case will correctly use \rootc{} context calls. Looking back at \cref{ex:half-maybe-root}, these additional rules and updated join operation will ensure that the first case will correctly use \rootc{} context calls.
For the second case, however, it detects that \mzninline{p} is used in both \posc{} and \mayberootc{} context. For the second case, however, it detects that \mzninline{p} is used in both \posc{} and \mayberootc{} context.
Therefore, it will output the \posc{} call for the right-hand side of \mzninline{p}, even when \mzninline{b} evaluates to \mzninline{true}. Therefore, it will output the \posc{} call for the right-hand side of \mzninline{p}, even when \mzninline{b} evaluates to true.
At compile time, this is the only correct context to use. At compile time, this is the only correct context to use.
We will, however, discuss how to adjust contexts dynamically during \gls{rewriting} in \cref{subsec:half-dyn-context}. We will, however, discuss how to adjust contexts dynamically during \gls{rewriting} in \cref{subsec:half-dyn-context}.
@ -857,7 +857,7 @@ In general the following rules apply.
\item The result of \gls{rewriting} an expression in \mixc{} context, a \gls{reif}, can be reused in \posc{}, \negc{}, and \mixc{} context. \item The result of \gls{rewriting} an expression in \mixc{} context, a \gls{reif}, can be reused in \posc{}, \negc{}, and \mixc{} context.
Since we assume that the result of \gls{rewriting} an expression in \negc{} context pushes the negation inwards, the \gls{reif} does, however, need to be negated. Since we assume that the result of \gls{rewriting} an expression in \negc{} context pushes the negation inwards, the \gls{reif} does, however, need to be negated.
\item If the expression was already seen in \rootc{} context, then any repeated usage of the expression can be assumed to take the value \mzninline{true} (or \mzninline{false} in \negc{} context). \item If the expression was already seen in \rootc{} context, then any repeated usage of the expression can be assumed to take the value true (or false in \negc{} context).
\end{itemize} \end{itemize}
@ -963,7 +963,7 @@ The same situation can be caused by \gls{propagation}.
constraint b -> (2*x = y); constraint b -> (2*x = y);
\end{mzn} \end{mzn}
Since the values in the \domain{} of \mzninline{x} are strictly smaller than the values in the \domain{} of \mzninline{y}, \gls{propagation} of \mzninline{b} will set it to the value \mzninline{true}. Since the values in the \domain{} of \mzninline{x} are strictly smaller than the values in the \domain{} of \mzninline{y}, \gls{propagation} of \mzninline{b} will set it to the value true.
This however means that the \constraint{} is equivalent to the following \constraint{}. This however means that the \constraint{} is equivalent to the following \constraint{}.
\begin{mzn} \begin{mzn}
@ -1022,7 +1022,7 @@ In each \instance{} certain values have already been fixed.
It is not always possible for all rows and columns to contain only distinct values. It is not always possible for all rows and columns to contain only distinct values.
In \minizinc{} counting the number of rows/columns with all different values can be accomplished using a \gls{reified} \mzninline{all_different} \constraint{}. In \minizinc{} counting the number of rows/columns with all different values can be accomplished using a \gls{reified} \mzninline{all_different} \constraint{}.
Since the goal of the problem is to maximize the number of \mzninline{all_different} \constraints{} that hold, these \constraints{} are never forced to be \mzninline{false}. Since the goal of the problem is to maximize the number of \mzninline{all_different} \constraints{} that hold, these \constraints{} are never forced to be false.
This means these \constraints{} are in \posc{} context and can be \gls{half-reified}. This means these \constraints{} are in \posc{} context and can be \gls{half-reified}.
\Cref{tab:half-qcp} shows the comparison of two solving configurations in \gls{chuffed} for the QCP-max problem. \Cref{tab:half-qcp} shows the comparison of two solving configurations in \gls{chuffed} for the QCP-max problem.
@ -1034,7 +1034,7 @@ This \gls{propagator} is an adjusted version from the existing \gls{bounds-con}
The implementation of the \gls{propagator} was already split into parts that check the violation of the \constraint{} and parts that prune the \glspl{domain} of the \variables{}. The implementation of the \gls{propagator} was already split into parts that check the violation of the \constraint{} and parts that prune the \glspl{domain} of the \variables{}.
Therefore, the transformation described in \cref{sec:half-propagation} can be directly applied. Therefore, the transformation described in \cref{sec:half-propagation} can be directly applied.
Since \gls{chuffed} is a \gls{lcg} \solver{}, the explanations created by the \gls{propagator} have to be adjusted as well. Since \gls{chuffed} is a \gls{lcg} \solver{}, the explanations created by the \gls{propagator} have to be adjusted as well.
These adjustments happen similar to the adjustments of the general algorithm: explanations used for the violation\glsadd{violated} of the \constraint{} can now be used to set the \gls{cvar} to \mzninline{false}, and the explanations given to prune a \variable{} are extended with a literal that ensures the \gls{cvar} is \mzninline{true}. These adjustments happen similar to the adjustments of the general algorithm: explanations used for the violation\glsadd{violated} of the \constraint{} can now be used to set the \gls{cvar} to false, and the explanations given to prune a \variable{} are extended with a literal that ensures the \gls{cvar} is true.
In our second configuration the \mzninline{all_different} \constraint{} is enforced using the \gls{decomp} shown in \cref{lst:half-alldiff}. In our second configuration the \mzninline{all_different} \constraint{} is enforced using the \gls{decomp} shown in \cref{lst:half-alldiff}.
The \mzninline{!=} \constraints{} produced by this redefinition are \gls{reified}. The \mzninline{!=} \constraints{} produced by this redefinition are \gls{reified}.
@ -1069,8 +1069,8 @@ In this experiment we can show how \gls{half-reif} can reduce the overhead of ha
The \minizinc{} model for this problem contains an \gls{array} lookup \mzninline{pos[next[i]]}, where the \domain{} of \mzninline{next[i]} is larger than the index set of \mzninline{pos}. The \minizinc{} model for this problem contains an \gls{array} lookup \mzninline{pos[next[i]]}, where the \domain{} of \mzninline{next[i]} is larger than the index set of \mzninline{pos}.
We compare safe \gls{decomp} of this \mzninline{element} \constraint{} against a \gls{propagator} of its \gls{half-reif}. We compare safe \gls{decomp} of this \mzninline{element} \constraint{} against a \gls{propagator} of its \gls{half-reif}.
The \gls{decomp} creates a new \variable{} that takes the value of the index only when it is within the index set of the \gls{array}. The \gls{decomp} creates a new \variable{} that takes the value of the index only when it is within the index set of the \gls{array}.
Otherwise, it will set its surrounding context to \mzninline{false}. Otherwise, it will set its surrounding context to false.
The \gls{half-reif} implicitly performs the same task by setting its \gls{cvar} to \mzninline{false} whenever the resulting \variable{} does not equal the element to which the index \variable{} points, or when the index points outside the \gls{array}. The \gls{half-reif} implicitly performs the same task by setting its \gls{cvar} to false whenever the resulting \variable{} does not equal the element to which the index \variable{} points, or when the index points outside the \gls{array}.
Again, for the implementation of the \gls{propagator} of the \gls{half-reif} \constraint{} we adjust the direct \gls{propagator} as described above. Again, for the implementation of the \gls{propagator} of the \gls{half-reif} \constraint{} we adjust the direct \gls{propagator} as described above.
\begin{table} \begin{table}
@ -1084,7 +1084,7 @@ Again, for the implementation of the \gls{propagator} of the \gls{half-reif} \co
The results of the experiment are shown in \cref{tab:half-prize}. The results of the experiment are shown in \cref{tab:half-prize}.
Although the performance on smaller \instances{} is similar, the dedicated \gls{propagator} consistently outperforms the \gls{decomp}. Although the performance on smaller \instances{} is similar, the dedicated \gls{propagator} consistently outperforms the \gls{decomp}.
The difference in performance becomes more pronounced in the bigger \instances{}. The difference in performance becomes more pronounced in the larger \instances{}.
In the 32-4-8 group, we even see that usage of the \gls{propagator} allows us to solve an additional three \instances{}. In the 32-4-8 group, we even see that usage of the \gls{propagator} allows us to solve an additional three \instances{}.
\subsection{Rewriting with Half-Reification} \subsection{Rewriting with Half-Reification}
@ -1146,7 +1146,7 @@ We also see that the \gls{booleanization} library is explicitly defined in terms
Some \constraints{} manually introduce \mzninline{_imp} call as part of their definition. Some \constraints{} manually introduce \mzninline{_imp} call as part of their definition.
Even when we do not automatically introduce \glspl{half-reif}, they are still introduced by other \constraints{}. Even when we do not automatically introduce \glspl{half-reif}, they are still introduced by other \constraints{}.
Furthermore, \gls{chain-compression} does not seem to have any effect. Furthermore, \gls{chain-compression} does not seem to have any effect.
Since all \glspl{half-reif} are defined in terms of clauses, the implications normally removed using \gls{chain-compression} are instead aggregated into bigger clauses. Since all \glspl{half-reif} are defined in terms of clauses, the implications normally removed using \gls{chain-compression} are instead aggregated into larger clauses.
Surprisingly, \gls{half-reif} slightly reduces the \gls{rewriting} time as it reduces the workload. Surprisingly, \gls{half-reif} slightly reduces the \gls{rewriting} time as it reduces the workload.
The relatively small changes shown might indicate that additional work might be warranted in the \gls{booleanization} library. The relatively small changes shown might indicate that additional work might be warranted in the \gls{booleanization} library.
It might be possible to create more dedicated \glspl{decomp} for \gls{half-reified} \constraints{}, and to analyse the library to see if \glspl{annotation} could be added to more function arguments to retain \posc{} contexts. It might be possible to create more dedicated \glspl{decomp} for \gls{half-reified} \constraints{}, and to analyse the library to see if \glspl{annotation} could be added to more function arguments to retain \posc{} contexts.

30
chapters/5_incremental.tex
View File

@ -228,7 +228,7 @@ Instead, we introduce the following function that can be used to signal to the s
function var bool: complete(); function var bool: complete();
\end{mzn} \end{mzn}
\noindent{}When the result of this function is said to be \mzninline{true}, then search is complete. \noindent{}When the result of this function is said to be true, then search is complete.
If any \gls{sol} was found, it is declared an \gls{opt-sol}. If any \gls{sol} was found, it is declared an \gls{opt-sol}.
Using the same methods it is also possible to describe optimization strategies with multiple \glspl{objective}. Using the same methods it is also possible to describe optimization strategies with multiple \glspl{objective}.
@ -294,7 +294,7 @@ To compile a \gls{meta-optimization} algorithms to a \gls{slv-mod}, the \gls{rew
\item It replaces the annotation \mzninline{::on_restart("X")} with a call to predicate \mzninline{X}. \item It replaces the annotation \mzninline{::on_restart("X")} with a call to predicate \mzninline{X}.
\item Inside predicate \mzninline{X} and any other predicate called recursively from \mzninline{X}: it must treat any call to functions \mzninline{sol}, \mzninline{status}, and \mzninline{last_val} as returning a \variable{}; and rename calls to random functions, e.g., \mzninline{uniform} to \mzninline{uniform_slv}, in order to distinguish them from their standard library versions. \item Inside predicate \mzninline{X} and any other predicate called recursively from \mzninline{X}: it must treat any call to functions \mzninline{sol}, \mzninline{status}, and \mzninline{last_val} as returning a \variable{}; and rename calls to random functions, e.g., \mzninline{uniform} to \mzninline{uniform_slv}, in order to distinguish them from their standard library versions.
\item It converts any expression containing a call from step 2 to be a \variable{} to ensure the functions are compiled as \constraints{}, rather than directly evaluated during \gls{rewriting}. \item It converts any expression containing a call from step 2 to be a \variable{} to ensure the functions are compiled as \constraints{}, rather than directly evaluated during \gls{rewriting}.
\item It rewrites the resulting model using an extension of the \minizinc{} standard library that provides declarations for these functions, as defined in the following of subsection. \item It rewrites the resulting model using an extension of the \minizinc{} standard library that provides declarations for these functions, as defined in the following subsection.
\end{enumerate} \end{enumerate}
These transformations will not change the code of many \gls{neighbourhood} definitions, since the functions are often used in positions that accept both \parameters{} and \variables{}. These transformations will not change the code of many \gls{neighbourhood} definitions, since the functions are often used in positions that accept both \parameters{} and \variables{}.
@ -377,7 +377,7 @@ In addition, for the new \constraints{} the \solver{} is extended using the foll
This is straightforward by using a \mzninline{last_val} \gls{propagator}. This is straightforward by using a \mzninline{last_val} \gls{propagator}.
It wakes up whenever its argument is fixed, and updates the last value (a non-\gls{backtrack}able value). It wakes up whenever its argument is fixed, and updates the last value (a non-\gls{backtrack}able value).
\item[Random number functions] Fix their \variable{} argument to a random number in the appropriate probability distribution. \item[Random number functions] Fix their \variable{} argument to a random number in the appropriate probability distribution.
\item[\mzninline{complete_reif(c)}] Stop and mark to search as ``complete'' when its \variable{} argument is forced to be true. \item[\mzninline{complete_reif(c)}] Stop and mark the search as ``complete'' when its \variable{} argument is forced to be true.
\end{description} \end{description}
Importantly, these \constraints{} need to be propagated in a way that their effects can be undone for the next \gls{restart}. Importantly, these \constraints{} need to be propagated in a way that their effects can be undone for the next \gls{restart}.
@ -419,14 +419,14 @@ Note that the \flatzinc{} \gls{slv-mod} shown here has been simplified for prese
\end{listing} \end{listing}
The first time the \solver{} is invoked, it sets \mzninline{s} to one (\mzninline{START}). The first time the \solver{} is invoked, it sets \mzninline{s} to one (\mzninline{START}).
\Gls{propagation} will fix \mzninline{b1} to \mzninline{false} and \mzninline{b3} to \mzninline{false}. \Gls{propagation} will fix \mzninline{b1} to false and \mzninline{b3} to false.
Therefore, the implication in \lref{line:6:x1:end} is not activated, leaving \mzninline{x[1]} unconstrained. Therefore, the implication in \lref{line:6:x1:end} is not activated, leaving \mzninline{x[1]} unconstrained.
The \gls{neighbourhood} \constraints{} are effectively switched off. The \gls{neighbourhood} \constraints{} are effectively switched off.
When the \solver{} \glspl{restart}, all the special \glspl{propagator} are re-executed. When the \solver{} \glspl{restart}, all the special \glspl{propagator} are re-executed.
Now \mzninline{s} is not one, and \mzninline{b1} is set to \mzninline{true}. Now \mzninline{s} is not one, and \mzninline{b1} is set to true.
The \mzninline{float_random} \gls{propagator} assigns \mzninline{rnd1} a new random value and, depending on whether it is greater than \mzninline{0.2}, the Boolean \variables{} \mzninline{b2}, and consequently \mzninline{b3} is assigned. The \mzninline{float_random} \gls{propagator} assigns \mzninline{rnd1} a new random value and, depending on whether it is greater than \mzninline{0.2}, the Boolean \variables{} \mzninline{b2}, and consequently \mzninline{b3} is assigned.
If it is \mzninline{true}, the \constraint{} in \lref{line:6:x1:end} becomes active and assigns \mzninline{x[1]} to its value in the previous \gls{sol}. If it is true, the \constraint{} in \lref{line:6:x1:end} becomes active and assigns \mzninline{x[1]} to its value in the previous \gls{sol}.
Furthermore, it is not strictly necessary to guard \mzninline{int_uniform} against being invoked before the first \gls{sol} is found. Furthermore, it is not strictly necessary to guard \mzninline{int_uniform} against being invoked before the first \gls{sol} is found.
The \mzninline{sol} \constraints{} will simply not propagate anything until the first \gls{sol} is recorded, but we use this simple example to illustrate how these Boolean conditions are rewritten and evaluated. The \mzninline{sol} \constraints{} will simply not propagate anything until the first \gls{sol} is recorded, but we use this simple example to illustrate how these Boolean conditions are rewritten and evaluated.
@ -464,7 +464,7 @@ This includes results of \gls{propagation}, \gls{cse} and other simplifications.
The addition of \constraints{} that can later be removed, is similar to making \glspl{search-decision} in a \gls{cp} \solver{} (see \cref{subsec:back-cp}). The addition of \constraints{} that can later be removed, is similar to making \glspl{search-decision} in a \gls{cp} \solver{} (see \cref{subsec:back-cp}).
As such, we can support the removal of \constraints{} in reverse chronological order by \gls{backtrack}ing. As such, we can support the removal of \constraints{} in reverse chronological order by \gls{backtrack}ing.
The \microzinc{} \interpreter{} maintains \gls{trail} of the changes to be undone when a \constraint{} is removed. The \microzinc{} \interpreter{} maintains a \gls{trail} of the changes to be undone when a \constraint{} is removed.
The \gls{trail} records all changes to the \nanozinc{} program: The \gls{trail} records all changes to the \nanozinc{} program:
\begin{itemize} \begin{itemize}
@ -501,7 +501,7 @@ In particular, this means that until the first choice point is created \gls{rewr
Then the \gls{trail} stores the inverse of all modifications that were made to the \nanozinc{} as a result of \mzninline{c}. Then the \gls{trail} stores the inverse of all modifications that were made to the \nanozinc{} as a result of \mzninline{c}.
The following code fragment illustrates the elements in this \gls{trail}. The following code fragment illustrates the elements in this \gls{trail}.
The reversal actions are annotated on the different elements. The reversal actions are annotated on the different elements.
The \mzninline{attach} and \mzninline{detach} actions signal the \interpreter{} to attach/detach a \constraint{} to the argument \variable{}, or the global \cmodel{} in case the argument is \mzninline{true}. The \mzninline{attach} and \mzninline{detach} actions signal the \interpreter{} to attach/detach a \constraint{} to the argument \variable{}, or the global \cmodel{} in case the argument is true.
The \mzninline{add} action tells to \interpreter{} to add a \variable{} to the \nanozinc{} program. The \mzninline{add} action tells to \interpreter{} to add a \variable{} to the \nanozinc{} program.
Finally, the \mzninline{set_domain} action makes the \interpreter{} restore the \domain{} using declaration to which it was attached. Finally, the \mzninline{set_domain} action makes the \interpreter{} restore the \domain{} using declaration to which it was attached.
@ -549,15 +549,15 @@ We therefore define the following three interfaces, using which we can apply the
In this section we present two experiments to test the efficiency and potency of the incremental methods introduced in this chapter. In this section we present two experiments to test the efficiency and potency of the incremental methods introduced in this chapter.
Our first experiment considers the effectiveness \gls{meta-optimization} within during solving. Our first experiment considers the effectiveness of \gls{meta-optimization} within during solving.
In particular, we investigate a round-robin \gls{lns} implemented using \gls{rbmo}. In particular, we investigate a round-robin \gls{lns} implemented using \gls{rbmo}.
On three different \minizinc{} models we compare this approach with solving the \instances{} directly using 2 different \solvers{}. On three different \minizinc{} models we compare this approach with solving the \instances{} directly using 2 different \solvers{}.
For one of the \solvers{}, we also compare with an oracle approach that can directly apply the exact same \gls{neighbourhood} as our \gls{rbmo}, without the need for computation. For one of the \solvers{}, we also compare with an oracle approach that can directly apply the exact same \gls{neighbourhood} as our \gls{rbmo}, without the need for computation.
As such, we show that the use of \gls{rbmo} introduces an insignificant computational overhead. As such, we show that the use of \gls{rbmo} introduces an insignificant computational overhead.
Our second experiment compares the performance of using \minizinc{} incrementally. Our second experiment evaluates the performance of using \minizinc{} incrementally.
We compare our two methods, \gls{rbmo} and the incremental constraint modelling interface, against the baseline of continuously \gls{rewriting} and reinitializing the \solver{}. We compare our two methods, \gls{rbmo} and the incremental constraint modelling interface, against the baseline of continuously \gls{rewriting} and reinitializing the \solver{}.
For this comparison compare the time that is required to (repeatedly) rewrite an \instance{} and the time required by the \solver{}. For this comparison, we analyse the time that is required to (repeatedly) rewrite an \instance{} and the time required by the \solver{} by different methods.
The first model contains a lexicographic objective. The first model contains a lexicographic objective.
The second model is shared between the two experiments and uses a round-robin \gls{lns} approach. The second model is shared between the two experiments and uses a round-robin \gls{lns} approach.
We compare the application of a fixed number of \glspl{neighbourhood}. We compare the application of a fixed number of \glspl{neighbourhood}.
@ -568,7 +568,7 @@ A description of the used computational environment, \minizinc{} instances, and
We will now show that a solver that evaluates the rewritten \gls{meta-optimization} specifications can (a) be effective and (b) incur only a small overhead compared to a dedicated implementation of the \glspl{neighbourhood}. We will now show that a solver that evaluates the rewritten \gls{meta-optimization} specifications can (a) be effective and (b) incur only a small overhead compared to a dedicated implementation of the \glspl{neighbourhood}.
To measure the overhead, we implemented \gls{rbmo} in \gls{gecode} \autocite{gecode-2021-gecode}. To measure the overhead, we implemented \gls{rbmo} in \gls{gecode} \autocite{schulte-2019-gecode}.
The resulting solver has been instrumented to also output the \domains{} of all \variables{} after propagating the new \gls{native} \constraints{}. The resulting solver has been instrumented to also output the \domains{} of all \variables{} after propagating the new \gls{native} \constraints{}.
We implemented another extension to \gls{gecode} that simply reads the stream of \variable{} \domains{} for each \gls{restart}, essentially ``replaying'' the \gls{meta-optimization} without incurring any overhead for evaluating the \glspl{neighbourhood} or handling the additional \variables{} and \constraints{}. We implemented another extension to \gls{gecode} that simply reads the stream of \variable{} \domains{} for each \gls{restart}, essentially ``replaying'' the \gls{meta-optimization} without incurring any overhead for evaluating the \glspl{neighbourhood} or handling the additional \variables{} and \constraints{}.
Note that this is a conservative estimate of the overhead: this extension has to perform less work than any real \gls{meta-optimization} implementation. Note that this is a conservative estimate of the overhead: this extension has to perform less work than any real \gls{meta-optimization} implementation.
@ -579,7 +579,7 @@ These experiments illustrate that the \gls{meta-optimization} implementations in
We ran experiments for three models from the MiniZinc Challenge \autocite{stuckey-2010-challenge, stuckey-2014-challenge} (\texttt{gbac}, \texttt{steelmillslab}, and \texttt{rcpsp-wet}). We ran experiments for three models from the MiniZinc Challenge \autocite{stuckey-2010-challenge, stuckey-2014-challenge} (\texttt{gbac}, \texttt{steelmillslab}, and \texttt{rcpsp-wet}).
The \instances{} are rewritten using the \minizinc{} 2.5.5 \compiler{}, adjusted to rewrite \gls{rbmo} specifications. The \instances{} are rewritten using the \minizinc{} 2.5.5 \compiler{}, adjusted to rewrite \gls{rbmo} specifications.
For each model we use a round-robin \gls{lns} approach, shown in \cref{lst:inc-round-robin}, of two \glspl{neighbourhood}: a \gls{neighbourhood} that destroys 20\% of the main \variables{} (\cref{lst:inc-lns-minisearch-pred}) and a structured \gls{neighbourhood} for the model (described below). For each model we use a round-robin \gls{lns} approach, shown in \cref{lst:inc-round-robin}, of two \glspl{neighbourhood}: a \gls{neighbourhood} that destroys 20\% of the main \variables{} (\cref{lst:inc-lns-minisearch-pred}) and a structured \gls{neighbourhood} for the model (described below).
For each solving method we show the cumulative integral of the objective values for all \instances{} of the model. For each solving method we show the integral of the cumulative objective values for all \instances{} of the model.
The underlying search strategy used is the fixed search strategy defined in the model. The underlying search strategy used is the fixed search strategy defined in the model.
The restart strategy uses the following \glspl{annotation}. The restart strategy uses the following \glspl{annotation}.
@ -653,7 +653,7 @@ For this problem a solution with zero wastage is always optimal.
As such the \gls{lns} approaches are sometimes able to prove a \gls{sol} is optimal and might finish before the time-out. As such the \gls{lns} approaches are sometimes able to prove a \gls{sol} is optimal and might finish before the time-out.
This is the case for \gls{chuffed} instances, where almost all \instances{} are solved using the \gls{rbmo} method. This is the case for \gls{chuffed} instances, where almost all \instances{} are solved using the \gls{rbmo} method.
As expected, the \gls{lns} approaches find better solutions quicker for \gls{gecode}. As expected, the \gls{lns} approaches find better solutions quicker for \gls{gecode}.
However, We do see that, given enough time, baseline \gls{gecode} will eventually find better \glspl{sol}. However, we do see that, given enough time, baseline \gls{gecode} will eventually find better \glspl{sol}.
% RCPSP/wet % RCPSP/wet
\subsubsection{RCPSP/wet} \subsubsection{RCPSP/wet}
@ -732,7 +732,7 @@ We do not notice any benefit from the use of the incremental solver \gls{api}.
We now revisit the model and method from \cref{ssubsec:inc-exp-gbac1} and compare the efficiency of using round-robin \gls{lns}. We now revisit the model and method from \cref{ssubsec:inc-exp-gbac1} and compare the efficiency of using round-robin \gls{lns}.
Instead, setting a time limit, we limit the number of \glspl{restart} that the \solver{} makes. Instead, setting a time limit, we limit the number of \glspl{restart} that the \solver{} makes.
As such, we limit the number of \glspl{neighbourhood} that are computed and applied to the \instance{}. As such, we limit the number of \glspl{neighbourhood} that are computed and applied to the \instance{}.
It should be noted that the \gls{rbmo} method is not guaranteed to apply the exact same \glspl{neighbourhood}, due to the difference in random number generator. It should be noted that the \gls{rbmo} method is not guaranteed to apply the exact same \glspl{neighbourhood}, due to the difference caused by random number generation.
\Cref{subfig:inc-cmp-lex} shows the results of applying 1000 \glspl{neighbourhood}. \Cref{subfig:inc-cmp-lex} shows the results of applying 1000 \glspl{neighbourhood}.
In this case there is an even more pronounced difference between the incremental methods and the naive method. In this case there is an even more pronounced difference between the incremental methods and the naive method.

14
chapters/6_conclusions.tex
View File

@ -22,7 +22,7 @@ We introduced a transformation language \microzinc{}, a minimal language used to
At the core of this architecture lie formal rewriting rules for \microzinc{} against which an implementation can be checked. At the core of this architecture lie formal rewriting rules for \microzinc{} against which an implementation can be checked.
The \gls{rewriting} process of a \minizinc{} \instance{} into a \gls{slv-mod} then consists of two steps: the translation of \minizinc{} model transformations into \microzinc{}, implemented by a \compiler{}; and the iterative \gls{rewriting} using these \microzinc{} transformations to arrive at a \gls{slv-mod}, implemented using an \interpreter{}. The \gls{rewriting} process of a \minizinc{} \instance{} into a \gls{slv-mod} then consists of two steps: the translation of \minizinc{} model transformations into \microzinc{}, implemented by a \compiler{}; and the iterative \gls{rewriting} using these \microzinc{} transformations to arrive at a \gls{slv-mod}, implemented using an \interpreter{}.
The latter operates on (partial) \glspl{slv-mod}, expressed using the \nanozinc{} language. The latter operates on a (partial) \glspl{slv-mod}, expressed using the \nanozinc{} language.
Distinctively, \nanozinc{} has the ability to attach \constraints{} to a \variable{}. Distinctively, \nanozinc{} has the ability to attach \constraints{} to a \variable{}.
During \gls{rewriting} \constraints{} introduced to define a \variable{} are attached to it. During \gls{rewriting} \constraints{} introduced to define a \variable{} are attached to it.
This ensures that if it is discovered that a \variable{} becomes unused (\ie{} it is not referred to by \constraints{} any longer), it can correctly be removed. This ensures that if it is discovered that a \variable{} becomes unused (\ie{} it is not referred to by \constraints{} any longer), it can correctly be removed.
@ -36,10 +36,10 @@ Crucially, the architecture is easily extended with well-known simplification te
\item \Gls{cse} is used to detect any duplicate calls. \item \Gls{cse} is used to detect any duplicate calls.
We describe how it can be employed both during the compilation from \minizinc{} to \microzinc{}, and in the evaluation of \microzinc{}. We describe how it can be employed both during the compilation from \minizinc{} to \microzinc{}, and in the evaluation of \microzinc{}.
\item When it is beneficial, the architecture can utilize \gls{aggregation} to combine certain \constraints{} and eliminate \gls{avar}. \item When it is beneficial, the architecture can utilize \gls{aggregation} to combine certain \constraints{} and eliminate \glspl{avar}.
\item Finally, \constraints{} can be marked for \gls{del-rew}. \item Finally, \constraints{} can be marked for \gls{del-rew}.
This suggests to the \microzinc{} \interpreter{} to delay the \gls{rewriting} of a certain call until all possible information is available. This requests the \microzinc{} \interpreter{} to delay the \gls{rewriting} of a certain call until all possible information is available.
\end{itemize} \end{itemize}
@ -89,8 +89,8 @@ These techniques were included in the official release in version 2.3.0.
In support of this, we have modified the \gls{rewriting} libraries of existing \minizinc{} \solvers{} to use \gls{half-reif}. In support of this, we have modified the \gls{rewriting} libraries of existing \minizinc{} \solvers{} to use \gls{half-reif}.
Notably, we have implemented explicit \glspl{decomp} of \gls{half-reified} \constraints{} for \gls{mip} and \gls{sat} \solvers{}. Notably, we have implemented explicit \glspl{decomp} of \gls{half-reified} \constraints{} for \gls{mip} and \gls{sat} \solvers{}.
The usage of these \glspl{decomp} significantly reduces the number of \constraints{} in the \gls{slv-mod}. The usage of these \glspl{decomp} significantly reduces the number of \constraints{} in the \gls{slv-mod}.
Additionally, we implemented two \glspl{propagator} for \gls{half-reif} \constraints{}, \mzninline{all_different} and \mzninline{element}, in a state-of-the-art \gls{cp} \solver{}, \gls{chuffed}, to re-evaluate the claims of the original \gls{half-reif} paper. Additionally, we implemented two \glspl{propagator} of \gls{half-reif} \constraints{}, \mzninline{all_different} and \mzninline{element}, in a state-of-the-art \gls{cp} \solver{}, \gls{chuffed}, to re-evaluate the claims of the original \gls{half-reif} paper.
In our experiments, we reaffirmed the effectiveness of the \glspl{propagator}, but we showed mixed results for the use of automatic \gls{half-reif} on a bigger scale. In our experiments, we reaffirmed the effectiveness of the \glspl{propagator}, but we showed mixed results for the use of automatic \gls{half-reif} on a larger scale.
While it was clearly beneficial for \gls{sat}, other \solvers{} did not seem to enjoy the same benefit and in some cases were even negatively impacted. While it was clearly beneficial for \gls{sat}, other \solvers{} did not seem to enjoy the same benefit and in some cases were even negatively impacted.
Although \gls{half-reif} is not a new technique, there are still numerous open questions. Although \gls{half-reif} is not a new technique, there are still numerous open questions.
@ -99,12 +99,12 @@ It is clear that the use of \gls{half-reif} is beneficial in some cases, but it
It is thus important that we achieve a better understanding of when the latter occurs. It is thus important that we achieve a better understanding of when the latter occurs.
As also discussed by \textcite{feydy-2011-half-reif}, we see that \gls{cp} solvers are sometimes negatively impacted because \glspl{half-reif} do not fix their \gls{cvar}, requiring more search. As also discussed by \textcite{feydy-2011-half-reif}, we see that \gls{cp} solvers are sometimes negatively impacted because \glspl{half-reif} do not fix their \gls{cvar}, requiring more search.
As a solution to this problem we could consider a form in between \gls{half-reif} and full \gls{reif}. As a solution to this problem we could consider a form in between \gls{half-reif} and full \gls{reif}.
In this form the propagator would set the \gls{cvar} to \mzninline{true} if the \constraint{} holds, but does not propagate the negation of the \constraint{} when it is set to \mzninline{false}. In this form the propagator would set the \gls{cvar} to true if the \constraint{} holds, but does not propagate the negation of the \constraint{} when it is set to false.
The downside of this form is that it is not equivalent to a logical implication, which means that measures such as \gls{chain-compression} would not be applicable. The downside of this form is that it is not equivalent to a logical implication, which means that measures such as \gls{chain-compression} would not be applicable.
However, \glspl{propagator} for this form are still easy to design/implement, and they ensure that the \gls{cvar} is fixed through \gls{propagation}. However, \glspl{propagator} for this form are still easy to design/implement, and they ensure that the \gls{cvar} is fixed through \gls{propagation}.
Finally, automated \gls{half-reif} in \minizinc{} will allow new solving performance improvements by allowing \solver{} implementers to experiment with \glspl{decomp} or \glspl{propagator} for \gls{half-reified} \constraints{}. Finally, automated \gls{half-reif} in \minizinc{} will allow new solving performance improvements by allowing \solver{} implementers to experiment with \glspl{decomp} or \glspl{propagator} for \gls{half-reified} \constraints{}.
\paragraph{Incremental Solving} Using a \cml{} as the interface for a \gls{meta-optimization} toolchain can be very intuitive and open up new opportunities. \paragraph{Incremental Solving} Using a \cml{} as the interface for a \gls{meta-optimization} toolchain can be very intuitive and opens up new opportunities.
The modeller can describe the process as a changing \cmodel{}. The modeller can describe the process as a changing \cmodel{}.
The overhead of the repeated \gls{rewriting} process to arrive at a \gls{slv-mod} can, however, be a hindrance. The overhead of the repeated \gls{rewriting} process to arrive at a \gls{slv-mod} can, however, be a hindrance.
\Cref{ch:incremental} presents our final contribution: \textbf{two methods to practically eliminate the overhead of using \cmls{} in \gls{meta-optimization}}. \Cref{ch:incremental} presents our final contribution: \textbf{two methods to practically eliminate the overhead of using \cmls{} in \gls{meta-optimization}}.

4
chapters/A2_benchmark.tex
View File

@ -78,7 +78,7 @@ In this thesis we use three different versions of the \minizinc\ flattening tool
In this thesis we use the following \solvers{}: In this thesis we use the following \solvers{}:
\paragraph{Chuffed} is an open source \gls{lcg} \solver{} \cite{chuffed-2021-chuffed}. \paragraph{Chuffed} is an open source \gls{lcg} \solver{} \autocite{chuffed-2021-chuffed,chu-2011-chuffed}.
In this thesis we use three different versions of the \gls{chuffed} \solver{}: In this thesis we use three different versions of the \gls{chuffed} \solver{}:
\begin{itemize} \begin{itemize}
@ -111,7 +111,7 @@ Its source code is available at
\url{https://github.com/coin-or/Cbc/tree/releases/2.10.5} \url{https://github.com/coin-or/Cbc/tree/releases/2.10.5}
\end{center} \end{center}
\paragraph{Gecode} is an open source \gls{cp} solver \autocite{gecode-2021-gecode}. \paragraph{Gecode} is an open source \gls{cp} solver \autocite{schulte-2019-gecode}.
In this thesis we use four different versions of the \gls{gecode} solver: In this thesis we use four different versions of the \gls{gecode} solver:
\begin{itemize} \begin{itemize}