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

Final changes

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-29 22:19:08 +10:00
parent e6be2ca5af
commit b60e3c426b
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
10 changed files with 117 additions and 88 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
.vscode/ltex.hiddenFalsePositives.en-GB.txt vendored
View File

@ -346,3 +346,28 @@
{"rule":"EN_A_VS_AN","sentence":"^\\QIn previous chapters, we explored \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q as a definitive linear process, where an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is translated into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, for which a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q produces Dummies.\\E$"} {"rule":"EN_A_VS_AN","sentence":"^\\QIn previous chapters, we explored \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q as a definitive linear process, where an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is translated into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, for which a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q produces Dummies.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QWe allow a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q algorithm, implemented in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q or a scripting language, to make incremental changes to an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} {"rule":"EN_A_VS_AN","sentence":"^\\QWe allow a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q algorithm, implemented in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q or a scripting language, to make incremental changes to an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"TOO_LONG_SENTENCE","sentence":"^\\QThe next and final chapter presents the conclusions of this thesis, which reiterate the discoveries and contributions of this research to theory and practice, comment on the scope and limitations of the presented architecture, and present further avenues for research in this area.\\E$"} {"rule":"TOO_LONG_SENTENCE","sentence":"^\\QThe next and final chapter presents the conclusions of this thesis, which reiterate the discoveries and contributions of this research to theory and practice, comment on the scope and limitations of the presented architecture, and present further avenues for research in this area.\\E$"}
{"rule":"TOO_LONG_SENTENCE","sentence":"^\\Qantitone name=antitone, description= A relation \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is said to be antitone w.r.t. its argument \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if given two possible values for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and all other arguments to \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q remain the same, then \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_GB_SIMPLE_REPLACE","sentence":"^\\QThe following set of equations describes this “knapsack” problem as an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qcomputing the square root of a negative value.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QAll the Dummies of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q are declared on \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: nweeks is the number of weeks to be considered, ngroups is the number of groups of golfers, and size is the size of each group.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe following set of equations describes this “knapsack” problem as an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe usage of a set of size nweeks means that we directly reason about that number of partitions that have to be unique.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIn the front-end, a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model is combined with its data into an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q process of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q transforms an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: the encoding of the problem for the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q cannot specify how, for example, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is best rewritten.\\E$"}
{"rule":"THREE_NN","sentence":"^\\QAlthough pure \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q behaves the same under any call evaluation strategy, in implementation a call by value strategy can provide more predictable behaviour with debugging functions in the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q language, such as \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"TOO_LONG_SENTENCE","sentence":"^\\Q\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q whether the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q can still be satisfied (and otherwise declare the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to be \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q), \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q values from the Dummies of Dummies that would violate the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and check whether the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q (i.e., proven to be \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q).\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QDefinition of the “argCtx” function for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Dummies.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QConsider for example the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q on integers, which \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q represents as an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q call.\\E$"}
{"rule":"TOO_LONG_SENTENCE","sentence":"^\\Q[Unsatisfiable] when it proves the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q does not have a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, [Optimal solution] when it has found a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and has proven the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to be optimal, [Satisfied] when it has found a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for the problem, [Unknown] when it does not find a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q within the time limit, and [Error] when the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q program crashes.\\E$"}
{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\Q,\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-ampl name=A Mathematical Programming Language (AMPL), description=AMPL is a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q originally designed to serve as a common input language for mathematical Dummies (e.g., \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q).\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qgls-ast name=Abstract Syntax Tree (AST), description=A tree structure representing the syntactic structure of a piece of computer language.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qboundsz-con name=bounds(\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q) consistent, description=A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is bounds(\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q) consistent when it tightens the integer \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q such that they can satisfy the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-cbls name=constraint-based local search (CBLS), description=A form of local search using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q violations as its \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-cbc name=COIN-OR Branch-and-Cut (CBC), description=A well-known open source \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qgls-cse name=common sub-expression elimination (CSE), description=A technique stemming from compiler optimization to avoid duplicate computation.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qincremental-rewriting name=incremental rewriting, description=The (repeated) \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that is continuously changed.,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qgls-maxsat name=Maximum Satisfiability (MaxSAT), description=An extension of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q problem class into an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qopt-sol name=optimal solution, description=A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for which it has been proven that other \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of higher quality, assessed using an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, do not exist.,\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qgls-sat name=Boolean satisfiability (SAT), description= A problem class that tries to find a valid \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for a set of Boolean Dummies subject to a logical formula.\\E$"}

22
assets/glossary.tex
View File

@ -6,6 +6,14 @@
description={A technique that combines many smaller \glspl{constraint} into a one or, by exception, a few larger \glspl{constraint}.}, description={A technique that combines many smaller \glspl{constraint} into a one or, by exception, a few larger \glspl{constraint}.},
} }
\newglossaryentry{antitone}{
name={antitone},
description={
A relation \( r(\ldots{}, a, \ldots{}) \) is said to be antitone w.r.t.\@ its argument \(a\) if given two possible values for \(a\), \(x\) and \(y\), if \(x \geq{} y\) and all other arguments to \(r\) remain the same, then \(r(\ldots{}, x, \ldots{}) \leq{} r(\ldots{}, y, \ldots{}) \).
},
}
\newglossaryentry{gls-ampl}{ \newglossaryentry{gls-ampl}{
name={A Mathematical Programming Language (AMPL)}, name={A Mathematical Programming Language (AMPL)},
description={AMPL is a \gls{cml} originally designed to serve as a common input language for mathematical \glspl{solver} (e.g., \gls{lp} and \gls{mip}). It has later been extended for other types of \glspl{solver}. See \cref{sub:back-ampl}.}, description={AMPL is a \gls{cml} originally designed to serve as a common input language for mathematical \glspl{solver} (e.g., \gls{lp} and \gls{mip}). It has later been extended for other types of \glspl{solver}. See \cref{sub:back-ampl}.},
@ -172,7 +180,7 @@
\newglossaryentry{gls-cse}{ \newglossaryentry{gls-cse}{
name={common sub-expression elimination (CSE)}, name={common sub-expression elimination (CSE)},
description={A technique stemming from programming languages to avoid duplicate computation. In \glspl{cml} this technique is used to avoid the creation of duplicate \glspl{variable} and \glspl{constraint}. See \cref{subsec:back-cse}.}, description={A technique stemming from compiler optimization to avoid duplicate computation. In \glspl{cml} this technique is used to avoid the creation of duplicate \glspl{variable} and \glspl{constraint}. See \cref{subsec:back-cse}.},
} }
\newglossaryentry{confluence}{ \newglossaryentry{confluence}{
@ -345,7 +353,7 @@
\newglossaryentry{gls-lcg}{ \newglossaryentry{gls-lcg}{
name={lazy clause generation (LCG)}, name={lazy clause generation (LCG)},
description={Types of \gls{solver} that extend \gls{cp} solving with \gls{sat} capabilities. Lazy clause generation \glspl{solver} lazily translate a \gls{cp} model for a \gls{sat} backend. As such, they maintain the pruning ability of a \gls{cp} solver while gaining the ability of \gls{sat} solvers to explain any failures in the search.}, description={Types of \gls{solver} that extend \gls{cp} solving with \gls{sat} capabilities. Lazy clause generation \glspl{solver} lazily translate a \gls{cp} model for a \gls{sat} back-end. As such, they maintain the pruning ability of a \gls{cp} solver while gaining the ability of \gls{sat} solvers to explain any failures in the search.},
} }
\newglossaryentry{gls-lns}{ \newglossaryentry{gls-lns}{
@ -387,6 +395,14 @@
} }
} }
\newglossaryentry{monotone}{
name={monotone},
description={
A relation \( r(\ldots{}, a, \ldots{}) \) is said to be monotone w.r.t.\@ its argument \(a\) when given two possible values for \(a\), \(x\) and \(y\), if \(x \geq{} y\) and all other arguments to \(r\) remain the same, then \(r(\ldots{}, x, \ldots{}) \geq{} r(\ldots{}, y, \ldots{})\).
}
}
\newglossaryentry{minizinc}{ \newglossaryentry{minizinc}{
name={Mini\-Zinc}, name={Mini\-Zinc},
description={ description={
@ -409,7 +425,7 @@
\newglossaryentry{gls-mip}{ \newglossaryentry{gls-mip}{
name={mixed integer programming (MIP)}, name={mixed integer programming (MIP)},
description={ description={
A solving technique that tries to find the \gls{opt-sol} for a \cmodel{} containing a mixture of Integer and floating point \glspl{variable} subject to \glspl{constraint} in the form of linear (in-)equations. A solving technique that tries to find the \gls{opt-sol} for a \cmodel{} containing a mixture of Integer and floating point \glspl{variable} subject to \glspl{constraint} in the form of linear (in\nobreakdash)equations.
Mixed integer programming is extensively studied and there are many successful \glspl{solver} dedicated to solving mixed integer programs. Mixed integer programming is extensively studied and there are many successful \glspl{solver} dedicated to solving mixed integer programs.
See \cref{subsec:back-mip}. See \cref{subsec:back-mip}.
} }

BIN
assets/img/back_compilation_structure.pdf
View File

Binary file not shown.

BIN
assets/img/rew_compilation_structure.pdf
View File

Binary file not shown.

2
chapters/0_abstract.tex
View File

@ -7,7 +7,7 @@
\noindent{}\Cmls{} are a prominent way to model and solve real world problems. \noindent{}\Cmls{} are a prominent way to model and solve real world problems.
They are used in areas such as scheduling, supply chain management, and transportation, among many others. They are used in areas such as scheduling, supply chain management, and transportation, among many others.
The \gls{rewriting} process of a \cml{} transforms a \cmodel{} into a \gls{slv-mod}, the input required by the program that solves the problem. The \gls{rewriting} process of a \cml{} transforms a \cmodel{} into a \gls{slv-mod}, the input required by the program that solves the problem.
In the past, these languages served mainly as a standardized interface between different \solvers{} and the \gls{rewriting} required was negligible. In the past, these languages served mainly as a standardized interface to different \solvers{} and the \gls{rewriting} required was negligible.
However, \cmls{} have evolved to include functionality that is not directly supported by the target \solvers{}. However, \cmls{} have evolved to include functionality that is not directly supported by the target \solvers{}.
As such, the \gls{rewriting} process has become more important and complex. As such, the \gls{rewriting} process has become more important and complex.

4
chapters/1_introduction.tex
View File

@ -71,11 +71,11 @@ We design and evaluate an architecture for \cmls{} that can accommodate the mode
Let us now study the different ways of constraint modelling in more detail, starting with one of the most commonly used \cmls{}: \glsxtrshort{ampl}. Let us now study the different ways of constraint modelling in more detail, starting with one of the most commonly used \cmls{}: \glsxtrshort{ampl}.
\glsxtrshort{ampl} was originally designed as a common interface to different \gls{mip} \solvers{}. \glsxtrshort{ampl} was originally designed as a common interface to different \gls{mip} \solvers{}.
The language provides a natural way to define numeric \variables{} and express \constraints{} in the form of linear (in-)equations as described by the class of problem. The language provides a natural way to define numeric \variables{} and express \constraints{} in the form of linear (in\nobreakdash)equations as described by the class of problem.
The same \glsxtrshort{ampl} model can then be used for different \solvers{}. The same \glsxtrshort{ampl} model can then be used for different \solvers{}.
\glsxtrshort{ampl} was later extended to include other \solver{} targets, including \gls{cp} and quadratic \solvers{}. \glsxtrshort{ampl} was later extended to include other \solver{} targets, including \gls{cp} and quadratic \solvers{}.
As such, additional types of \constraints{} for these problem classes have been added to the language, removing the restriction that \constraints{} must be linear (in-)equations. As such, additional types of \constraints{} for these problem classes have been added to the language, removing the restriction that \constraints{} must be linear (in\nobreakdash)equations.
Let us introduce the \glsxtrshort{ampl} language by modelling the ``open shop'' problem. Let us introduce the \glsxtrshort{ampl} language by modelling the ``open shop'' problem.
In the open shop problem, the goal is to schedule jobs with multiple tasks. In the open shop problem, the goal is to schedule jobs with multiple tasks.

98
chapters/2_background.tex
View File

@ -28,19 +28,20 @@ A specific problem is captured by an \instance{}, the combination of a \cmodel{}
The type of problem described by a \cmodel{} is called a \gls{dec-prb}. The type of problem described by a \cmodel{} is called a \gls{dec-prb}.
The goal of a \gls{dec-prb} is to find a \gls{sol}: a complete \gls{variable-assignment} that satisfies the \constraints{}, or, when this is not possible, prove that such an \gls{assignment} cannot exist. The goal of a \gls{dec-prb} is to find a \gls{sol}: a complete \gls{variable-assignment} that satisfies the \constraints{}, or, when this is not possible, prove that such an \gls{assignment} cannot exist.
Many \cmls{} also support the modelling of \glspl{opt-prb}, where a \gls{dec-prb} is augmented with an \gls{objective}. Many \cmls{} also support the modelling of \glspl{opt-prb}, where a \gls{dec-prb} is augmented with an \gls{objective}.
In this case the goal is to find a \gls{sol} that satisfies all \constraints{} while minimizing (or maximizing) the value of the \gls{objective}. In this case the goal is to find a \gls{sol} that satisfies all \constraints{} while maximizing (or minimizing) the value of the \gls{objective}.
Although a \cmodel{} does not contain any instructions on how to find a suitable \gls{sol}, \instances{} of \cmodels{} can generally be given to a dedicated \solver{}. Although a \cmodel{} does not contain any instructions on how to find a suitable \gls{sol}, \instances{} of \cmodels{} can generally be given to a dedicated \solver{}.
To solve these \instances{}, however, they can go through a \gls{rewriting} process to arrive at a \gls{slv-mod}, which is the input accepted by a \solver{}. However, to solve these \instances{} they first have to go through a \gls{rewriting} process to arrive at a \gls{slv-mod}, which is the input accepted by a \solver{}.
The \solver{} then uses a dedicated algorithm that finds a \gls{sol} that fits the requirements of the \instance{}. The \solver{} then uses a dedicated algorithm that finds a \gls{sol} that fits the requirements of the \instance{}.
\begin{example}% \begin{example}%
\label{ex:back-knapsack} \label{ex:back-knapsack}
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 to 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*}
\text{maximize}~z~\text{subject to}~ \text{maximize}~z~\text{subject to}~
@ -119,7 +120,7 @@ It is the primary way in which \minizinc{} communicates with \solvers{}.
\end{mzn} \end{mzn}
The modeller can then choose a \solver{}. The modeller can then choose a \solver{}.
Let us assume we choose a \gls{mip} \solver{}, whose \gls{native} \variables{} are only integer \variables{} and whose \gls{native} \constraints{} are only linear \constraints{}. Let us assume we choose a \glsxtrshort{mip} \solver{}, whose \gls{native} \variables{} are only integer \variables{} and whose \gls{native} \constraints{} are only linear \constraints{}.
\Gls{rewriting} the \instance{} would result in the \flatzinc{} \gls{slv-mod} in \cref{lst:back-fzn-knapsack}. \Gls{rewriting} the \instance{} would result in the \flatzinc{} \gls{slv-mod} in \cref{lst:back-fzn-knapsack}.
The set type \variable{} \mzninline{selection} is now represented using three integer \variables{}, \mzninline{selection_@\(i\)@}. The set type \variable{} \mzninline{selection} is now represented using three integer \variables{}, \mzninline{selection_@\(i\)@}.
Each represent whether an element is present in the set. Each represent whether an element is present in the set.
@ -136,7 +137,7 @@ It is the primary way in which \minizinc{} communicates with \solvers{}.
\end{example} \end{example}
\begin{listing} \begin{listing}
\mznfile{assets/listing/back_knapsack.fzn} \mznfile{assets/listing/back_knapsack.fzn}
\caption{\label{lst:back-fzn-knapsack} A \flatzinc{} \gls{slv-mod} for a \gls{mip} \solver{}, resulting from \gls{rewriting} \cref{lst:back-mzn-knapsack} with a given complete \gls{parameter-assignment}.} \caption{\label{lst:back-fzn-knapsack} A \flatzinc{} \gls{slv-mod} for a \glsxtrshort{mip} \solver{}, resulting from \gls{rewriting} \cref{lst:back-mzn-knapsack} with a given complete \gls{parameter-assignment}.}
\end{listing} \end{listing}
@ -154,7 +155,7 @@ The structure of a \minizinc{} model can be described directly in terms of a \cm
More complex models also include definitions for custom types, user-defined functions, and a custom output format. More complex models also include definitions for custom types, user-defined functions, and a custom output format.
These items are not constrained to occur in any particular order. These items are not constrained to occur in any particular order.
We briefly discuss the most important model items. We briefly discuss the most important model items.
Note that these items already refer to \minizinc{} expressions, which will be discussed in \cref{subsec:back-mzn-expr}. Note that these items already refer to \minizinc{} expressions, which will be discussed in the next subsection.
For a detailed overview of the structure of \minizinc{} models the full syntactic structure of \minizinc{} 2.5.5 can be consulted in \cref{ch:minizinc-grammar}. For a detailed overview of the structure of \minizinc{} models the full syntactic structure of \minizinc{} 2.5.5 can be consulted in \cref{ch:minizinc-grammar}.
\textcite{nethercote-2007-minizinc} offer a detailed discussion of \minizinc{}. \textcite{nethercote-2007-minizinc} offer a detailed discussion of \minizinc{}.
Much of \minizinc{}'s history can be learned from the description of its predecessor, \zinc{} \autocite{marriott-2008-zinc}. Much of \minizinc{}'s history can be learned from the description of its predecessor, \zinc{} \autocite{marriott-2008-zinc}.
@ -249,7 +250,7 @@ The collection of function declarations to rewrite for a \solver{} is generally
In this library, functions can be declared without a function body. In this library, functions can be declared without a function body.
This marks them as \gls{native} to the \solver{}. This marks them as \gls{native} to the \solver{}.
Calls to these functions are directly placed in the \gls{slv-mod}. Calls to these functions are directly placed in the \gls{slv-mod}.
For non-\gls{native} functions, a \solver{} provides a function body that rewrites calls into (or towards) \gls{native} functions, a \gls{decomp}. For non-\gls{native} functions, \solvers{} provide \glspl{decomp}: functions with a body that rewrites calls into (or towards) \gls{native} functions.
\Solver{} implementers are, however, not forced to provide a definition for all functions in \minizinc{}'s extensive library. \Solver{} implementers are, however, not forced to provide a definition for all functions in \minizinc{}'s extensive library.
Instead, they can rely on a set of standard declarations, known as the standard library, that rewrite functions into a minimal subset of \gls{native} functions, known as the \flatzinc{} built-ins. Instead, they can rely on a set of standard declarations, known as the standard library, that rewrite functions into a minimal subset of \gls{native} functions, known as the \flatzinc{} built-ins.
@ -298,7 +299,7 @@ There are many other types of expressions in \minizinc{} that help modellers exp
\paragraph{Operators} When we express a mathematical formula, we generally do this through the use of \gls{operator} symbols. \paragraph{Operators} When we express a mathematical formula, we generally do this through the use of \gls{operator} symbols.
\minizinc{} includes \glspl{operator} for many mathematical, logic, and set operations. \minizinc{} includes \glspl{operator} for many mathematical, logic, and set operations.
Consider, for example, the following \constraint{} Consider, for example, the following \constraint{}.
\begin{mzn} \begin{mzn}
constraint not (a + b < c); constraint not (a + b < c);
@ -321,7 +322,7 @@ It can, for example, force that the absolute value of \mzninline{a} is larger th
The result of a \gls{conditional} expression is not limited to Boolean types. The result of a \gls{conditional} expression is not limited to Boolean types.
The condition in the expression, the ``if'', must be of a Boolean type, but as long as the different sides of the \gls{conditional} expression are the same type it is a valid \gls{conditional} expression. The condition in the expression, the ``if'', must be of a Boolean type, but as long as the different sides of the \gls{conditional} expression are the same type it is a valid \gls{conditional} expression.
This can be used to, for example, define an absolute value function an integer as follows. This can be used to, for example, define an absolute value function for integer \parameters{} as follows.
\begin{mzn} \begin{mzn}
function int: abs(int: a) = function int: abs(int: a) =
@ -363,7 +364,7 @@ During \gls{rewriting}, the instantiation of the expression with current generat
This means that the type of the \gls{array} primarily depends on the type of the expression. This means that the type of the \gls{array} primarily depends on the type of the expression.
However, in recent versions of \minizinc{} both the collections over which we iterate and the filtering condition could have a \variable{} type. However, in recent versions of \minizinc{} both the collections over which we iterate and the filtering condition could have a \variable{} type.
Since we then cannot decide during \gls{rewriting} if an element is present in the \gls{array}, the elements are made of an \gls{optional} type. Since we then cannot decide during \gls{rewriting} if an element is present in the \gls{array}, the elements are made of an \gls{optional} type.
This means that the \solver{} still will decide if the element is present in the \gls{array} or if it takes a special ``absent'' value (\mzninline{<>}). This means that the \solver{} will decide if the element is present in the \gls{array} or if it takes a special ``absent'' value (\mzninline{<>}).
\paragraph{Let Expressions} Together with function definitions, \glspl{let} are the primary scoping mechanism in the \minizinc{} language. \paragraph{Let Expressions} Together with function definitions, \glspl{let} are the primary scoping mechanism in the \minizinc{} language.
A \gls{let} allows a modeller to provide a list of declarations, that can only be used in the body of the \gls{let}. A \gls{let} allows a modeller to provide a list of declarations, that can only be used in the body of the \gls{let}.
@ -392,17 +393,17 @@ There are three main purposes for \glspl{let}.
\begin{mzn} \begin{mzn}
function var int: int_times(var int: x, var int: y) = function var int: int_times(var int: x, var int: y) =
let { let {
var int: z; var int: z;
constraint pred_int_times(x, y, z); constraint pred_int_times(x, y, z);
} in z; } in z;
\end{mzn} \end{mzn}
\end{enumerate} \end{enumerate}
An important detail in \gls{rewriting} \glspl{let} is that any \variables{} that are introduced may need to be renamed in the resulting \gls{slv-mod}. An important detail in \gls{rewriting} \glspl{let} is that any \variables{} that are introduced may need to be renamed in the resulting \gls{slv-mod}.
Different to \variables{} declared directly in declaration items, the \variables{} declared in \glspl{let} can be evaluated multiple times when used in loops, function definitions (that are called multiple times), and \gls{array} \glspl{comprehension}. Different to variables declared directly in declaration items, the variables declared in \glspl{let} can be evaluated multiple times when used in loops, function definitions (that are called multiple times), and \gls{array} \glspl{comprehension}.
The \gls{rewriting} process must assign any \variables{} in the \gls{let} a new name and use this name in any subsequent definitions and in the resulting expression. The \gls{rewriting} process must assign any variables in the \gls{let} a new name and use this name in any subsequent definitions and in the resulting expression.
\paragraph{Annotations} Although \minizinc{} does not typically prescribe a way to find the \gls{sol} for an \instance{}, it provides the modeller with a way to give ``hints'' to the \solver{}. \paragraph{Annotations} Although \minizinc{} does not typically prescribe a way to find the \gls{sol} for an \instance{}, it provides the modeller with a way to give ``hints'' to the \solver{}.
It does this through the use of \glspl{annotation}. It does this through the use of \glspl{annotation}.
@ -427,18 +428,18 @@ The \gls{reif} of a \constraint{} \(c\) creates a Boolean \gls{avar} \mzninline{
\begin{mzn} \begin{mzn}
array[1..10] of var 1..15: x; array[1..10] of var 1..15: x;
constraint all_different(x); constraint all_different(x);
solve maximize sum(i in 1..10) (x[i] mod 2 == 0); solve maximize sum(i in 1..10) (x[i] mod 2 = 0);
\end{mzn} \end{mzn}
This model maximizes the number of even numbers taken by the elements of the \gls{array} \mzninline{x}. This model maximizes the number of even numbers taken by the elements of the \gls{array} \mzninline{x}.
In this model the expression \mzninline{x[i] mod 2 == 0} has to be \gls{reified}. In this model the expression \mzninline{x[i] mod 2 = 0} has to be \gls{reified}.
This means that for each \mzninline{i}, a \gls{cvar} \mzninline{b_i} is added, together with a constraint that makes \mzninline{b_i} take the value \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} take the value \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 \glspl{cvar} it sets to \true{}. Instead, the \solver{} is tasked to maximize the number of \glspl{cvar} 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{}.
Contrarily, an expression that occurs in non-\rootc{} is reified during the \gls{rewriting} process. Contrarily, an expression that occurs in non-\rootc{} is reified during the \gls{rewriting} process.
In \minizinc{}, almost all expressions can be used in both \rootc{} and non-\rootc{} contexts. In \minizinc{}, almost all expressions can be used in both \rootc{} and non-\rootc{} contexts.
@ -475,13 +476,13 @@ Other examples of \gls{partial} functions in \minizinc{} are:
x div 0 = @??@ x div 0 = @??@
\end{mzn} \end{mzn}
\item finding the minimum or maximum of an empty set, \item finding the minimum or maximum of an empty set, and
\begin{mzn} \begin{mzn}
min({}) = @??@ min({}) = @??@
\end{mzn} \end{mzn}
\item and computing the square root of a negative value. \item computing the square root of a negative value.
\begin{mzn} \begin{mzn}
sqrt(-1) = @??@ sqrt(-1) = @??@
@ -492,7 +493,7 @@ Other examples of \gls{partial} functions in \minizinc{} are:
The existence of undefined expressions can cause confusion in \cmls{}. The existence of undefined expressions can cause confusion in \cmls{}.
There is both the question of what happens when an undefined expression is evaluated and at what point during the process undefined values are resolved, during \gls{rewriting} or by the \solver{}. There is both the question of what happens when an undefined expression is evaluated and at what point during the process undefined values are resolved, during \gls{rewriting} or by the \solver{}.
\textcite{frisch-2009-undefinedness} define three semantic models to deal with the undefinedness in \cmls: \textcite{frisch-2009-undefinedness} define three semantic models to deal with the undefinedness in \cmls{}.
\begin{description} \begin{description}
@ -700,7 +701,7 @@ It is an \gls{opt-sol}.
Mathematical programming \solvers{} are the most prominent solving technique employed in \gls{or} \autocite{schrijver-1998-mip}. Mathematical programming \solvers{} are the most prominent solving technique employed in \gls{or} \autocite{schrijver-1998-mip}.
At its foundation lies \gls{lp}. At its foundation lies \gls{lp}.
A linear program describes a problem using \constraints{} in the form of linear (in-)equations over continuous \variables{}. A linear program describes a problem using \constraints{} in the form of linear (in\nobreakdash)equations over continuous \variables{}.
In general, a linear program can be expressed in the following form. In general, a linear program can be expressed in the following form.
\begin{align*} \begin{align*}
@ -745,14 +746,13 @@ These \solvers{} are therefore prime targets to solve \minizinc{} \instances{}.
To solve an \instance{} of a \cmodel{}, it can be rewritten into a mixed integer program. To solve an \instance{} of a \cmodel{}, it can be rewritten into a mixed integer program.
This process is known as \gls{linearization}. This process is known as \gls{linearization}.
It does, however, come with its challenges. 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\nobreakdash)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.
An indicator variable \(y_{i}\) is a \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}
Let us again consider the N-Queens problem from \cref{ex:back-nqueens}. Let us again consider the N-Queens problem from \cref{ex:back-nqueens}.
The following model shows an integer program of this problem. The following model shows an integer program of this problem.
@ -773,7 +773,6 @@ An indicator variable \(y_{i}\) is a \gls{avar} that for a \variable{} \(x\) tak
The \cref{line:back-mip-channel} is used to connect the \(q\) and \(y\) \variables{} and make sure that their values correspond. The \cref{line:back-mip-channel} is used to connect the \(q\) and \(y\) \variables{} and make sure that their values correspond.
\Cref{line:back-mip-row} ensures that only one queen is placed in the same column. \Cref{line:back-mip-row} ensures that only one queen is placed in the same column.
Finally, \cref{line:back-mip-diag1,line:back-mip-diag2} constrain all diagonals to contain only one queen. Finally, \cref{line:back-mip-diag1,line:back-mip-diag2} constrain all diagonals to contain only one queen.
\end{example} \end{example}
\subsection{Boolean Satisfiability}% \subsection{Boolean Satisfiability}%
@ -908,7 +907,7 @@ Different types of \solvers{} can also have access to different types of \constr
The main reason for this difference is the level at which these models are written. The main reason for this difference is the level at which these models are written.
The \gls{ampl} model is written to target a \gls{mip} solver. The \gls{ampl} model is written to target a \gls{mip} solver.
In the \gls{ampl} language this means that the modeller is required to use the language functionality that is compatible with the targeted \solver{}; in this case, all expression have to be linear (in-)equations. In the \gls{ampl} language this means that the modeller is required to use the language functionality that is compatible with the targeted \solver{}; in this case, all expression have to be linear (in\nobreakdash)equations.
In \minizinc{} the modeller is not constrained in the same way. In \minizinc{} the modeller is not constrained in the same way.
It can use the viewpoint of choosing, from each city, to which city to go next. It can use the viewpoint of choosing, from each city, to which city to go next.
@ -1028,16 +1027,15 @@ Since sets, multi-sets, and functions can be defined on any other type, these ty
In the social golfer problem, a community of golfers plans games of golf for a set number of weeks. In the social golfer problem, a community of golfers plans games of golf for a set number of weeks.
Every week all the golfers are split into groups of equal size and each group plays a game of golf. Every week all the golfers are split into groups of equal size and each group plays a game of golf.
The goal of the problem is to find a way to split the groups differently every week, such that two golfers will not meet each other twice. The goal of the problem is to find a way to split the groups differently every week, such that two golfers will not meet each other twice.
Two golfers can only be part of the same group once.
A \cmodel{} for the social golfer problem in \gls{essence} can be seen in \cref{lst:back-essence-sgp}.
\begin{listing} \begin{listing}
\plainfile[l]{assets/listing/back_sgp.essence} \plainfile[l]{assets/listing/back_sgp.essence}
\caption{\label{lst:back-essence-sgp} An \gls{essence} model describing the social golfer problem} \caption{\label{lst:back-essence-sgp} An \gls{essence} model describing the social golfer problem}
\end{listing} \end{listing}
The \gls{essence} model starts with the preamble declaring the version of the language that is used. A \cmodel{} for the social golfer problem in \gls{essence} can be seen in \cref{lst:back-essence-sgp}.
All the \parameters{} of the \cmodel{} are declared on \lref{line:back:essence:pars}: \texttt{weeks} is the number of weeks to be considered, \texttt{groups} is the number of groups of golfers, and \texttt{size} is the size of each group. It starts with the preamble declaring the version of the language that is used.
All the \parameters{} of the \cmodel{} are declared on \lref{line:back:essence:pars}: \texttt{nweeks} is the number of weeks to be considered, \texttt{ngroups} is the number of groups of golfers, and \texttt{size} is the size of each group.
The input for the \parameters{} is checked to ensure that they take a value that is one or higher. The input for the \parameters{} is checked to ensure that they take a value that is one or higher.
\Lref{line:back:essence:ntype} then uses the \parameters{} to declare a new type to represent the golfers. \Lref{line:back:essence:ntype} then uses the \parameters{} to declare a new type to represent the golfers.
@ -1045,7 +1043,7 @@ Since sets, multi-sets, and functions can be defined on any other type, these ty
It declares a \variable{} that is a set of partitions of the golfers. It declares a \variable{} that is a set of partitions of the golfers.
The choice in \variable already contains some implied \constraints{}. The choice in \variable already contains some implied \constraints{}.
Since the \variable{} reasons about partitions of the golfers, a correct \gls{assignment} is already guaranteed to correctly split the golfers into groups. Since the \variable{} reasons about partitions of the golfers, a correct \gls{assignment} is already guaranteed to correctly split the golfers into groups.
The usage of a set of size \texttt{weeks} means that we directly reason about that number of partitions that have to be unique. The usage of a set of size \texttt{nweeks} means that we directly reason about that number of partitions that have to be unique.
The type of the \variable{} does, however, not guarantee that two golfers will not meet each other twice. The type of the \variable{} does, however, not guarantee that two golfers will not meet each other twice.
Therefore, a \constraint{} that enforces this is found on \lref{line:back:essence:con}. Therefore, a \constraint{} that enforces this is found on \lref{line:back:essence:con}.
@ -1059,7 +1057,6 @@ Since sets, multi-sets, and functions can be defined on any other type, these ty
Note that, through the \gls{essence} type system, the first two \constraints{} in the \minizinc{} model are implied in the \gls{essence} model. Note that, through the \gls{essence} type system, the first two \constraints{} in the \minizinc{} model are implied in the \gls{essence} model.
This is an example where the use of high-level types helps the modeller create more concise models. This is an example where the use of high-level types helps the modeller create more concise models.
Apart from syntax and the \variable{} viewpoint, the \constraint{} that enforces that golfers only occur in the same group once is identical. Apart from syntax and the \variable{} viewpoint, the \constraint{} that enforces that golfers only occur in the same group once is identical.
\end{example} \end{example}
\begin{listing} \begin{listing}
@ -1076,7 +1073,7 @@ Then, an \gls{ess-prime} model forms an \instance{}, and is subsequently rewritt
Compared to \gls{essence}, the \gls{ess-prime} language does not contain the same high-level \variables{}. Compared to \gls{essence}, the \gls{ess-prime} language does not contain the same high-level \variables{}.
As such, the main task of Conjure, the compiler from \gls{essence} to \gls{ess-prime}, is to decide on a representation of these \variables{} in terms of integer and Boolean \variables{} \autocite{akgun-2014-essence}. As such, the main task of Conjure, the compiler from \gls{essence} to \gls{ess-prime}, is to decide on a representation of these \variables{} in terms of integer and Boolean \variables{} \autocite{akgun-2014-essence}.
However, there are often multiple ways to represent a high-level \variable{}, or how to enforce its implicit \constraints{}. However, there are often multiple ways to represent a high-level \variable{} or how to enforce its implicit \constraints{}.
Although the modeller is able to decide on representation, Conjure has been extended to automatically select among the models it produces \autocite{akgun-2013-auto-ess}. Although the modeller is able to decide on representation, Conjure has been extended to automatically select among the models it produces \autocite{akgun-2013-auto-ess}.
\paragraph{Essence'} \paragraph{Essence'}
@ -1101,7 +1098,7 @@ In particular, \glspl{decomp} for \constraints{} are not declared as predicates
Recently, \textcite{kocak-2020-ess-incr} have also presented Savile Row as the basis of a \gls{meta-optimization} toolchain. Recently, \textcite{kocak-2020-ess-incr} have also presented Savile Row as the basis of a \gls{meta-optimization} toolchain.
The authors extend Savile Row to bridge the gap between the incremental assumption interface of \gls{sat} \solvers{} and the modelling language and show how this helps to efficiently solve pattern mining and optimization problems. The authors extend Savile Row to bridge the gap between the incremental assumption interface of \gls{sat} \solvers{} and the modelling language and show how this helps to efficiently solve pattern mining and optimization problems.
Consequently, the usage of \gls{meta-optimization} in Savile Row reiterates the use of \gls{meta-optimization} algorithms in \cmls{} in general and the need for incremental bridging between the modelling language and the \solver{}. Consequently, the usage of \gls{meta-optimization} in Savile Row reiterates the importance of the use of \gls{meta-optimization} algorithms in \cmls{} in general and the need for incremental bridging between the modelling language and the \solver{}.
\section{Term Rewriting}% \section{Term Rewriting}%
\label{sec:back-term} \label{sec:back-term}
@ -1232,7 +1229,6 @@ This means that, for some rules, multiple terms must match, to apply the rule.
\end{itemize} \end{itemize}
Note that the use of multi-headed rewriting rules is essential to define these rules. Note that the use of multi-headed rewriting rules is essential to define these rules.
\end{example} \end{example}
The rules in a \gls{chr} system are categorized into three different categories: simplification, propagation, and simpagation. The rules in a \gls{chr} system are categorized into three different categories: simplification, propagation, and simpagation.
@ -1250,19 +1246,19 @@ Since simpagation rules incorporate both the elements of simplification and prop
\section{Rewriting \glsentrytext{minizinc}}% \section{Rewriting \glsentrytext{minizinc}}%
\label{sec:back-mzn-interpreter} \label{sec:back-mzn-interpreter}
Traditionally a \compiler{} is split into three sequential parts: the ``frontend'', the ``middle-end'', and the ``backend''. Traditionally a \compiler{} is split into three sequential parts: the ``front-end'', the ``middle-end'', and the ``back-end''.
It is the job of the frontend to parse the user input, report on any errors or inconsistencies in the input, and transform it into an internal representation. It is the job of the front-end to parse the user input, report on any errors or inconsistencies in the input, and transform it into an internal representation.
The middle-end performs the main translation, independent of the compilation target. The middle-end performs the main translation, independent of the compilation target.
It converts the internal representation at the level of the compiler frontend to another internal representation as close as possible to the level required by the compilation targets. It converts the internal representation at the level of the compiler front-end to another internal representation as close as possible to the level required by the compilation targets.
The final transformations into the format required by the compilation target are performed by the backend. The final transformations into the format required by the compilation target are performed by the back-end.
When a \compiler{} is separated into these three steps, then adding support for a new language or compilation target only requires the addition of a frontend or backend respectively. When a \compiler{} is separated into these three steps, then adding support for a new language or compilation target only requires the addition of a front-end or back-end respectively.
The \minizinc{} compilation process can be split into the same three parts, as shown in \cref{fig:back-mzn-comp}. The \minizinc{} compilation process can be split into the same three parts, as shown in \cref{fig:back-mzn-comp}.
In the frontend, a \minizinc{} model is combined with its data into an \instance{}. In the front-end, a \minizinc{} model is combined with its data into an \instance{}.
The instance is parsed into an \gls{ast}. The instance is parsed into an \gls{ast}.
The process then analyses the \gls{ast} to discover the types of all expressions used in the \instance{}. The process then analyses the \gls{ast} to discover the types of all expressions used in the \instance{}.
If an inconsistency is discovered, then an error is reported to the modeller. If an inconsistency is discovered, then an error is reported to the modeller.
Finally, the frontend also preprocesses the \gls{ast}. Finally, the front-end also preprocesses the \gls{ast}.
This process is used to transform expressions into a common form for the middle-end, removing the ``syntactic sugar''. This process is used to transform expressions into a common form for the middle-end, removing the ``syntactic sugar''.
For instance, this replaces enumerated types by normal integers. For instance, this replaces enumerated types by normal integers.
@ -1276,16 +1272,14 @@ The middle-end contains the most important two processes: \gls{rewriting} and op
During the \gls{rewriting} process the \minizinc{} model is rewritten into a \gls{slv-mod}. During the \gls{rewriting} process the \minizinc{} model is rewritten into a \gls{slv-mod}.
It could be noted that the \gls{rewriting} step depends on the compilation target to define its \gls{native} \constraints{}. It could be noted that the \gls{rewriting} step depends on the compilation target to define its \gls{native} \constraints{}.
Even though the information required for this step is target dependent, we consider it part of the middle-end as the mechanism is the same for all compilation targets. Even though the information required for this step is target dependent, we consider it part of the middle-end as the mechanism is the same for all compilation targets.
A full description of this process will follow in \cref{subsec:back-rewriting}. A full description of this process will follow in the next subsection.
Once a \gls{slv-mod} is constructed, the \minizinc{} \compiler{} tries to optimize this model: shrink \domains{} of \variables{}, remove \constraints{} that are proven to hold, and remove \variables{} that have become unused. Once a \gls{slv-mod} is constructed, the \minizinc{} \compiler{} tries to optimize this model: shrink \domains{} of \variables{}, remove \constraints{} that are proven to hold, and remove \variables{} that have become unused.
These optimization techniques are discussed in \cref{subsec:back-fzn-optimization}. These optimization techniques are discussed in the remaining subsections.
The backend converts the internal \gls{slv-mod} into a format to be used by the targeted \solver{}. The back-end converts the internal \gls{slv-mod} into a format to be used by the targeted \solver{}.
Given the formatted artefact, a \solver{} process, controlled by the backend, is then started. Given the formatted artefact, a \solver{} process, controlled by the back-end, is then started.
The \solver{} process produces \glspl{sol} for the \gls{slv-mod}. The \solver{} process produces \glspl{sol} for the \gls{slv-mod}.
Before these are given to the modeller, the backend reformulates these \glspl{sol} to become \glspl{sol} of the modeller's \instance{}. Before these are given to the modeller, the back-end reformulates these \glspl{sol} to become \glspl{sol} of the modeller's \instance{}.
In this section we discuss the \gls{rewriting} and optimization process as employed by the 2.5.5 version of \minizinc{} \autocite{minizinc-2021-minizinc}.
\subsection{Rewriting}% \subsection{Rewriting}%
\label{subsec:back-rewriting} \label{subsec:back-rewriting}
@ -1314,7 +1308,7 @@ A notable effect of the \gls{rewriting} is that sub-expressions are replaced by
If the expression contains only \parameters{}, then the \gls{rewriting} of the expression is merely a calculation to find the value of the literal to be put in its place. If the expression contains only \parameters{}, then the \gls{rewriting} of the expression is merely a calculation to find the value of the literal to be put in its place.
If, however, the expression contains a \variable{}, then this calculation cannot be performed during the \gls{rewriting} process. If, however, the expression contains a \variable{}, then this calculation cannot be performed during the \gls{rewriting} process.
Instead, an \gls{avar} must be created to represent the value of the sub-expression, and it must be constrained to take the value corresponding to the expression. Instead, an \gls{avar} must be created to represent the value of the sub-expression, and it must be constrained to take the value corresponding to the expression.
The creation of this \gls{avar} and defining \constraints{} happens in one of two ways: The creation of this \gls{avar} and defining \constraints{} happens in one of two ways.
\begin{itemize} \begin{itemize}

13
chapters/3_rewriting.tex
View File

@ -245,7 +245,6 @@ The translation from \minizinc{} to \microzinc{} involves the following steps.
\begin{nzn} \begin{nzn}
constraint main(10); constraint main(10);
\end{nzn} \end{nzn}
\end{example} \end{example}
\subsection{Partial Evaluation of \glsentrytext{nanozinc}}\label{sub:rew-partial} \subsection{Partial Evaluation of \glsentrytext{nanozinc}}\label{sub:rew-partial}
@ -263,12 +262,11 @@ For this to happen, the \gls{rewriting} process introduces fresh \variables{} to
Consider the (reasonably typical) \minizinc{} encoding for the absolute value function presented in \cref{lst:rew-abs}. Consider the (reasonably typical) \minizinc{} encoding for the absolute value function presented in \cref{lst:rew-abs}.
When an occurrence of \mzninline{abs} is encountered, the call will be replaced by a \variable{} \mzninline{z}. When an occurrence of \mzninline{abs} is encountered, the call will be replaced by a \variable{} \mzninline{z}.
But before that can occur, the \variable{} must be introduced, and the \constraint{} \mzninline{int_abs(x, z)} is added to the model, enforcing its value. But before that can occur, the \variable{} must be introduced, and the \constraint{} \mzninline{int_abs(x, z)} is added to the model, enforcing its value.
\begin{listing}
\mznfile{assets/listing/rew_abs.mzn}
\caption{\label{lst:rew-abs} A \minizinc{} definition for the absolute value function.}
\end{listing}
\end{example} \end{example}
\begin{listing}
\mznfile{assets/listing/rew_abs.mzn}
\caption{\label{lst:rew-abs} A \minizinc{} definition for the absolute value function.}
\end{listing}
The function \mzninline{abs(x)} above is a total function: for every value of \mzninline{x}, there is always exactly one valid value of \mzninline{z}. The function \mzninline{abs(x)} above is a total function: for every value of \mzninline{x}, there is always exactly one valid value of \mzninline{z}.
In this case, the \constraint{} introduced in the \gls{let} may be enforced globally, and multiple occurrences of \mzninline{abs(x)} may be replaced with the same \mzninline{z}. In this case, the \constraint{} introduced in the \gls{let} may be enforced globally, and multiple occurrences of \mzninline{abs(x)} may be replaced with the same \mzninline{z}.
@ -485,7 +483,7 @@ The framework has the ability to support multiple \solvers{}.
It can pretty-print the \nanozinc{} code to standard \flatzinc{}, so that any solver currently compatible with \minizinc{} can be used. It can pretty-print the \nanozinc{} code to standard \flatzinc{}, so that any solver currently compatible with \minizinc{} can be used.
Additionally, a direct C++ \glsxtrshort{api} can be used to connect solvers directly, in order to enable incremental solving. Additionally, a direct C++ \glsxtrshort{api} can be used to connect solvers directly, in order to enable incremental solving.
We revisit this topic in \cref{ch:incremental}. We revisit this topic in \cref{ch:incremental}.
The source code for the complete system has been made available under an open-source license, and it has been included in the experiment resources in \cref{ch:benchmarks}. The source code for the complete system has been made available under an open-source licence, and it has been included in the experiment resources in \cref{ch:benchmarks}.
\section{NanoZinc Simplification}\label{sec:rew-simplification} \section{NanoZinc Simplification}\label{sec:rew-simplification}
@ -708,7 +706,6 @@ Earlier in the process, however, the \minizinc{} to \microzinc{} \compiler{} can
constraint let { var int: y = abs(x) } in constraint let { var int: y = abs(x) } in
(y*2 >= 20) \/ (y+5 >= 15) (y*2 >= 20) \/ (y+5 >= 15)
\end{mzn} \end{mzn}
\end{example} \end{example}
As such, the \compiler{} can enforce sharing of common sub-expressions before evaluation begins. As such, the \compiler{} can enforce sharing of common sub-expressions before evaluation begins.

39
chapters/4_half_reif.tex
View File

@ -26,7 +26,7 @@ The \gls{rewriting} process then enforces a \constraint{} \mzninline{pred_reif(.
As an alternative, the authors introduce \gls{half-reif}. As an alternative, the authors introduce \gls{half-reif}.
It follows from the idea that in many cases it is sufficient to use the logical implication of an expression, \mzninline{b -> pred(...)}, instead of the logical equivalence, \mzninline{b <-> pred(...)}. It follows from the idea that in many cases it is sufficient to use the logical implication of an expression, \mzninline{b -> pred(...)}, instead of the logical equivalence, \mzninline{b <-> pred(...)}.
\Gls{rewriting} with \gls{half-reif} is an approach that improves upon all these weaknesses of \gls{rewriting} with ``full'' \gls{reif}. \Gls{rewriting} with \gls{half-reif} is an approach that improves upon these weaknesses of \gls{rewriting} with ``full'' \gls{reif}.
\begin{itemize} \begin{itemize}
\item \Gls{rewriting} using \glspl{half-reif} can lead to significantly better \glspl{slv-mod} when translating \gls{partial} function calls. \item \Gls{rewriting} using \glspl{half-reif} can lead to significantly better \glspl{slv-mod} when translating \gls{partial} function calls.
@ -37,7 +37,7 @@ Additionally, for many \solvers{} the \gls{decomp} of a \gls{reif} is more compl
We will show that using \glspl{half-reif} can therefore lead to a reduction in \gls{native} \constraints{} in the \gls{slv-mod}. We will show that using \glspl{half-reif} can therefore lead to a reduction in \gls{native} \constraints{} in the \gls{slv-mod}.
\Gls{half-reif} can be used instead of full \gls{reif} when the resulting \gls{cvar} can never be forced to be \false{}. \Gls{half-reif} can be used instead of full \gls{reif} when the resulting \gls{cvar} can never be forced to be \false{}.
This requirement follows from the difference between implication and logical equivalences. This requirement follows from the difference between implication and logical equivalence.
Setting the left-hand side of an implication to \false{} does not influence the value on the right-hand side. Setting the left-hand side of an implication to \false{} does not influence the value on the right-hand side.
This is why the \gls{cvar} should never be forced to be \false{}, since this would not enforce the negation of the \constraint{}. This is why the \gls{cvar} should never be forced to be \false{}, since this would not enforce the negation of the \constraint{}.
Setting the right-hand side of an implication to \true{} also does not influence the left-hand side. Setting the right-hand side of an implication to \true{} also does not influence the left-hand side.
@ -73,7 +73,6 @@ This is, however, not an issue since in this case the value can just be assigned
constraint b2 -> (y = 5); constraint b2 -> (y = 5);
constraint b1 \/ b2; constraint b1 \/ b2;
\end{mzn} \end{mzn}
\end{example} \end{example}
This property can be extended to include non-Boolean expressions. This property can be extended to include non-Boolean expressions.
@ -91,9 +90,9 @@ Since Boolean expressions in \minizinc{} can be used in, for example, integer ex
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}
To systematically analyse whether Boolean expressions can be \gls{half-reified}, we study the \emph{monotonicity} of \constraints{} w.r.t.\@ an expression. To systematically analyse whether Boolean expressions can be \gls{half-reified}, we study the monotonicity of \constraints{} w.r.t.\@ an expression.
A relation \( r(\ldots{}, a, \ldots{}) \) is said to be \emph{monotone} w.r.t.\@ its argument \(a\) when given two possible values for \(a\), \(x\) and \(y\), if \(x \geq{} y\) and all other arguments to \(r\) remain the same, then \(r(\ldots{}, x, \ldots{}) \geq{} r(\ldots{}, y, \ldots{})\). A relation \( r(\ldots{}, a, \ldots{}) \) is said to be \gls{monotone} w.r.t.\@ its argument \(a\) when given two possible values for \(a\), \(x\) and \(y\), if \(x \geq{} y\) and all other arguments to \(r\) remain the same, then \(r(\ldots{}, x, \ldots{}) \geq{} r(\ldots{}, y, \ldots{})\).
The relation is said to be \emph{antitone} w.r.t.\@ its argument \(a\) if given two possible values for \(a\), \(x\) and \(y\), if \(x \geq{} y\) and all other arguments to \(r\) remain the same, then \(r(\ldots{}, x, \ldots{}) \leq{} r(\ldots{}, y, \ldots{}) \). The relation is said to be \gls{antitone} w.r.t.\@ its argument \(a\) if given two possible values for \(a\), \(x\) and \(y\), if \(x \geq{} y\) and all other arguments to \(r\) remain the same, then \(r(\ldots{}, x, \ldots{}) \leq{} r(\ldots{}, y, \ldots{}) \).
Where, for clarification, we assume \( \false{} < \true{} \). Where, for clarification, we assume \( \false{} < \true{} \).
Using these definitions, we introduce additional distinctions in the context of expressions. Using these definitions, we introduce additional distinctions in the context of expressions.
@ -202,9 +201,9 @@ Instead, new explicit methods have to be devised to implement the \gls{propagato
In comparison, a \gls{propagator} for the \gls{reif} of \(c\) cannot be created from these three logical tasks. In comparison, a \gls{propagator} for the \gls{reif} of \(c\) cannot be created from these three logical tasks.
In addition, we require the \(prune\) task from a \gls{propagator} of \(\neg{} c\). In addition, we require the \(prune\) task from a \gls{propagator} of \(\neg{} c\).
Using these additional function, we can define an algorithm for the \gls{propagator}, shown in \cref{alg:reif-prop}. Although this seems reasonable for small \constraints{}, such as integer equality, for many \glspl{global} their negation is hard to define. Using this additional function, we can define an algorithm for the \gls{propagator}, shown in \cref{alg:reif-prop}. Although this seems reasonable for small \constraints{}, such as integer equality, for many \glspl{global} their negation is hard to define.
For example, the negation of the \mzninline{all_different} \constraint{} is a \constraint{} that forces that at least two values are equal. For example, the negation of the \mzninline{all_different} \constraint{} is a \constraint{} that forces that at least two values are equal.
This is far from a common \constraint{} and we are not aware of any \solver{} that implements a \gls{propagator} for it. This is far from a common \constraint{}, and we are not aware of any \solver{} that implements a \gls{propagator} for it.
\begin{algorithm}[t] \begin{algorithm}[t]
@ -284,10 +283,10 @@ The transition from the \gls{cnf} of the regular \constraint{} \(c\) to its \gls
It is, however, not as straightforward to construct its full \gls{reif}. It is, however, not as straightforward to construct its full \gls{reif}.
In addition to the \gls{half-reified} \gls{cnf}, a generic \gls{reif} would require the implication \(\neg \texttt{b} \implies \neg c\). In addition to the \gls{half-reified} \gls{cnf}, a generic \gls{reif} would require the implication \(\neg \texttt{b} \implies \neg c\).
Based on the \gls{cnf} of \(c\), this would result in the following logical formula: Based on the \gls{cnf} of \(c\), this would result in the following logical formula.
\[ \neg b \implies \neg c = \forall_{i} b \lor \neg \exists_{j} lit_{ij} \] \[ \neg b \implies \neg c = \forall_{i} b \lor \neg \exists_{j} lit_{ij} \]
This formula, however, is not direct set of clauses. This formula, however, is not direct set of clauses.
Rewriting this formula into \gls{cnf} would result in: Rewriting this formula would result in the following \gls{cnf}.
\[ \neg b \implies \neg c = \forall_{i,j} b \lor lit_{ij} \] \[ \neg b \implies \neg c = \forall_{i,j} b \lor lit_{ij} \]
It adds a new binary clause for every literal in the original \gls{cnf}. It adds a new binary clause for every literal in the original \gls{cnf}.
In general, many more clauses are needed to decompose a \gls{reif} compared to a \gls{half-reif}. In general, many more clauses are needed to decompose a \gls{reif} compared to a \gls{half-reif}.
@ -500,7 +499,7 @@ This means that if \(ctx\) is \rootc{}, the \compiler{} can use the function as
Otherwise, the \compiler{} follows the following steps to try to introduce the most compatible variant of the function. Otherwise, the \compiler{} follows the following steps to try to introduce the most compatible variant of the function.
\begin{enumerate} \begin{enumerate}
\item If a direct definition for \(ctx\) definition exists, then use this definition. \item If a direct definition for \(ctx\) exists, then use this definition.
\begin{description} \begin{description}
\item[\posc] \Glspl{half-reif} can be defined as \(ident\)\mzninline{_imp}. \item[\posc] \Glspl{half-reif} can be defined as \(ident\)\mzninline{_imp}.
@ -747,13 +746,12 @@ During the \gls{rewriting} process the contexts assigned to the different expres
constraint f_imp(x, y); % y -> f(x) constraint f_imp(x, y); % y -> f(x)
constraint int_ne_imp(x, 5, b2); % b2 -> x != 5 constraint int_ne_imp(x, 5, b2); % b2 -> x != 5
\end{mzn} \end{mzn}
\end{example} \end{example}
As this example shows, the use of \gls{half-reif} can form so-called \glspl{implication-chain}. As this example shows, the use of \gls{half-reif} can form so-called \glspl{implication-chain}.
This happens when the right-hand side of an implication is \gls{half-reified} and a \gls{cvar} is created to represent the expression. This happens when the right-hand side of an implication is \gls{half-reified} and a \gls{cvar} is created to represent the expression.
Instead, we could have used the left-hand side of the implication as the \gls{cvar} of the \gls{half-reified} \constraint{}. Instead, we could have used the left-hand side of the implication as the \gls{cvar} of the \gls{half-reified} \constraint{}.
In next section, we present a new post-processing method we call \gls{chain-compression}. In the next section, we present a new post-processing method we call \gls{chain-compression}.
It can be used to eliminate these \glspl{implication-chain}. It can be used to eliminate these \glspl{implication-chain}.
The \gls{rewriting} with \gls{half-reif} also interacts with some simplification methods used during the \gls{rewriting} process. The \gls{rewriting} with \gls{half-reif} also interacts with some simplification methods used during the \gls{rewriting} process.
@ -820,7 +818,7 @@ These can be split up into multiple implications.
constraint b -> forall(x in N)(x) constraint b -> forall(x in N)(x)
\end{mzn} \end{mzn}
The expression above is logically equivalent to the following expression. \noindent{}The expression above is logically equivalent to the following expression.
\begin{mzn} \begin{mzn}
constraint forall(x in N)(b -> x) constraint forall(x in N)(b -> x)
@ -851,7 +849,7 @@ In general the following rules apply.
\item The result of \gls{rewriting} an expression in \negc{} context, a \gls{half-reif} with its negation pushed inwards, can only be reused if the same expression is again found in \negc{} context. \item The result of \gls{rewriting} an expression in \negc{} context, a \gls{half-reif} with its negation pushed inwards, can only be reused if the same expression is again found in \negc{} context.
\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{cvar} does need to be negated when used in \negc{}.
\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). \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).
@ -911,7 +909,7 @@ This ensures that all \variables{} and \constraints{} created for the earlier ve
Now when \mzninline{b2} is added to the \gls{cse} table as the \gls{cvar} of the \gls{reif} of the \mzninline{int_le(i, 4)} call, it notices that there is already a result in table for the same call in a weaker context. Now when \mzninline{b2} is added to the \gls{cse} table as the \gls{cvar} of the \gls{reif} of the \mzninline{int_le(i, 4)} call, it notices that there is already a result in table for the same call in a weaker context.
As such, it replaces all occurrences of the \gls{cvar} of the \gls{half-reif}, found in the table, with the \gls{cvar} of the \gls{reif}. As such, it replaces all occurrences of the \gls{cvar} of the \gls{half-reif}, found in the table, with the \gls{cvar} of the \gls{reif}.
Once all usage of the \gls{cvar} have been removed, it and its dependent \constraints{} are removed, resulting in the following \nanozinc{} program. Once all usage of the \gls{cvar} has been removed, it and its dependent \constraints{} are removed, resulting in the following \nanozinc{} program.
\begin{nzn} \begin{nzn}
constraint bool_clause([j, b2], []); constraint bool_clause([j, b2], []);
@ -938,7 +936,7 @@ The expression is \gls{reified} and replaces the existing \gls{half-reified} exp
This canonical form for expressions and their negations can also be used for the expressions in other contexts. This canonical form for expressions and their negations can also be used for the expressions in other contexts.
Using the canonical form we can now also be sure that we never create a full \gls{reif} for both an expression and its negation. Using the canonical form we can now also be sure that we never create a full \gls{reif} for both an expression and its negation.
Instead, when one is created, the negation of the resulting \variable{} can directly be used as the \gls{reif} of its negation. Instead, when one is created, the negation of its \gls{cvar} can directly be used as the \gls{reif} of its negation.
Moreover, this mechanism also allows us to detect when an expression and its negation occur in \rootc{} context. Moreover, this mechanism also allows us to detect when an expression and its negation occur in \rootc{} context.
Since a \constraint{} and its negation cannot both hold at the same time, this is a simple way to detect that the \cmodel{} is \gls{unsat}. Since a \constraint{} and its negation cannot both hold at the same time, this is a simple way to detect that the \cmodel{} is \gls{unsat}.
@ -967,7 +965,6 @@ The same situation can be caused by \gls{propagation}.
\end{mzn} \end{mzn}
The linear \constraint{} could be evaluated in \rootc{} context, instead of the \posc{} context that is detected by our context analysis. The linear \constraint{} could be evaluated in \rootc{} context, instead of the \posc{} context that is detected by our context analysis.
\end{example} \end{example}
The situation shown in the example is the most common change of context. The situation shown in the example is the most common change of context.
@ -998,7 +995,7 @@ The \gls{cvar} is thus used to communicate the change in context.
\label{sec:half-experiments} \label{sec:half-experiments}
We now present an experimental evaluation of the presented techniques. We now present an experimental evaluation of the presented techniques.
First, to show the benefit of implementing \glspl{propagator} for \gls{half-reified} \constraints{} by comparing their performance against their \glspl{decomp}. First, to show the benefit of implementing \glspl{propagator} for \gls{half-reified} \constraints{}, we compare their performance against their \glspl{decomp}.
We recreate two experiments presented by \textcite{feydy-2011-half-reif} in the original \gls{half-reif} paper in a modern \gls{cp} solver, \gls{chuffed}. We recreate two experiments presented by \textcite{feydy-2011-half-reif} in the original \gls{half-reif} paper in a modern \gls{cp} solver, \gls{chuffed}.
We adapt the \glspl{propagator} for the non-\gls{reified} \constraints{} to take into account the \gls{cvar}, by reusing the code for checking and pruning as described in \cref{sec:half-propagation}. We adapt the \glspl{propagator} for the non-\gls{reified} \constraints{} to take into account the \gls{cvar}, by reusing the code for checking and pruning as described in \cref{sec:half-propagation}.
@ -1088,7 +1085,7 @@ In the 32-4-8 group, we even see that usage of the \gls{propagator} allows us to
The usage of context analysis and introduction of \glspl{half-reif} allows us to evaluate \gls{half-reif} on a larger scale. The usage of context analysis and introduction of \glspl{half-reif} allows us to evaluate \gls{half-reif} on a larger scale.
In our second experiment we assess its effects on the \gls{rewriting} and solving of the \instances{} of the 2019 and 2020 \minizinc{} challenge \autocite{stuckey-2010-challenge,stuckey-2014-challenge}. In our second experiment we assess its effects on the \gls{rewriting} and solving of the \instances{} of the 2019 and 2020 \minizinc{} challenge \autocite{stuckey-2010-challenge,stuckey-2014-challenge}.
These experiments are conducted using the \gls{gecode} \solver{}, which have \glspl{propagator} for \glspl{half-reif} of many basic \constraints{}, and \minizinc{}'s \gls{linearization} and \gls{booleanization} libraries, which has been adapted to use \gls{half-reif} as earlier described. These experiments are conducted using the \gls{gecode} \solver{}, which has \glspl{propagator} for \glspl{half-reif} of many basic \constraints{}, and \minizinc{}'s \gls{linearization} and \gls{booleanization} libraries, which have been adapted to use \gls{half-reif} as earlier described.
The \minizinc{} instances are rewritten using the \minizinc{} 2.5.5 \compiler{}, which can enable and disable \gls{half-reif}. The \minizinc{} instances are rewritten using the \minizinc{} 2.5.5 \compiler{}, which can enable and disable \gls{half-reif}.
The solving of the linearized \instances{} are tested using the \gls{cbc} and \gls{cplex} \gls{mip} \solvers{}. The solving of the linearized \instances{} are tested using the \gls{cbc} and \gls{cplex} \gls{mip} \solvers{}.
The solving of the Booleanized \instances{} are testing using the \gls{openwbo} \solver{}. The solving of the Booleanized \instances{} are testing using the \gls{openwbo} \solver{}.
@ -1158,7 +1155,7 @@ It may be possible to create more dedicated \glspl{decomp} for \gls{half-reified
\item[Unsatisfiable] when it proves the \instance{} does not have a \gls{sol}, \item[Unsatisfiable] when it proves the \instance{} does not have a \gls{sol},
\item[Optimal solution] when it has found a \gls{sol} and has proven the \gls{sol} to be optimal, \item[Optimal solution] when it has found a \gls{sol} and has proven the \gls{sol} to be optimal,
\item[Satisfied] when it has found a \gls{sol} for the problem, \item[Satisfied] when it has found a \gls{sol} for the problem,
\item[Unknown] when it does not find a \gls{sol} is found within the time limit, and \item[Unknown] when it does not find a \gls{sol} within the time limit, and
\item[Error] when the \solver{} program crashes. \item[Error] when the \solver{} program crashes.
\end{description} \end{description}

2
chapters/5_incremental.tex
View File

@ -107,7 +107,7 @@ If the search does return a new \gls{sol}, then it commits to that \gls{sol}, an
The \mzninline{lns} function also posts the \constraint{} \mzninline{obj < sol(obj)}, ensuring the objective value in the next iteration is strictly better than that of the current \gls{sol}. The \mzninline{lns} function also posts the \constraint{} \mzninline{obj < sol(obj)}, ensuring the objective value in the next iteration is strictly better than that of the current \gls{sol}.
Although \minisearch{} enables the modeller to express declarative \glspl{neighbourhood}, the definition of the \gls{meta-optimization} algorithm is rather unintuitive and difficult to debug, leading to unwieldy code for defining even simple algorithms. Although \minisearch{} enables the modeller to express declarative \glspl{neighbourhood}, the definition of the \gls{meta-optimization} algorithm is rather unintuitive and difficult to debug, leading to unwieldy code for defining even simple algorithms.
Furthermore, the \minisearch{} implementation requires either a close integration of the backend \solver{} into the \minisearch{} system, or it drives the solver through the regular text file based \flatzinc{} interface. Furthermore, the \minisearch{} implementation requires either a close integration of the target \solver{} into the \minisearch{} system, or it drives the solver through the regular text file based \flatzinc{} interface.
This leads to a significant communication overhead. This leads to a significant communication overhead.
To address these two issues, we propose to keep modelling \glspl{neighbourhood} as predicates, but define \gls{meta-optimization} algorithms from an imperative perspective. To address these two issues, we propose to keep modelling \glspl{neighbourhood} as predicates, but define \gls{meta-optimization} algorithms from an imperative perspective.