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

Notes by Guido

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-14 20:42:24 +10:00
parent d0125970cd
commit 5bfe2af4e0
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
14 changed files with 354 additions and 269 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
assets/acronyms.tex
View File

@ -58,7 +58,5 @@
\newacronym{sgp}{SGP}{Social Golfer Problem}
\newacronym[see={[Glossary:]{gls-trs}}]{trs}{TRS\glsadd{gls-trs}}{Term Rewriting System}
\newacronym{tsp}{TSP}{Travelling Salesperson Problem}

19
assets/bibliography/references.bib
View File

@ -1163,6 +1163,25 @@
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@inproceedings{stuckey-2019-conditionals,
author = {Peter J. Stuckey and Guido Tack},
editor = {Thomas Schiex and Simon de Givry},
title = {Compiling Conditional Constraints},
booktitle = {Principles and Practice of Constraint Programming - 25th
International Conference, {CP} 2019, Stamford, CT, USA, September
30 - October 4, 2019, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {11802},
pages = {384--400},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-30048-7\_23},
doi = {10.1007/978-3-030-30048-7\_23},
timestamp = {Sat, 12 Oct 2019 12:51:44 +0200},
biburl = {https://dblp.org/rec/conf/cp/StuckeyT19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@unpublished{van-hentenryck-1992-indexicals,
title = {Constraint processing in cc(FD)},
author = {Van Hentenryck, P. and Saraswat, V. and Deville, Y.},

13
assets/glossary.tex
View File

@ -48,6 +48,11 @@
description={A \gls{solver} is said to backtrack when it revisits a search decision (\eg{} an value assumed during search). Notably the action of backtracking generally involves invalidating all effects of the revisited and subsequent search decisions},
}
\newglossaryentry{binding}{
name={binding},
description={A \gls{variable} is said to have a binding \gls{domain} when it is tighter than the bounds that can be computed from its defining expression. A binding \gls{domain} is a \gls{constraint} of the overall \gls{model}},
}
\newglossaryentry{bnb}{
name={branch and bound},
description={A search method to find an \gls{opt-sol}. After an initial \gls{sol} is found, the search continuously looks for \glspl{sol} for which the \gls{objective} will return a better value than the incumbent \gls{sol}. If it is proven that no such \gls{sol} exists, then the final incumbent \gls{sol} is an \gls{opt-sol}},
@ -170,7 +175,7 @@
name={decomposition},
description={
A formulation of a \gls{constraint} in terms of other \glspl{constraint} in order to reach \gls{native} \glspl{constraint}.
Note that the new \glspl{constraint} might represent the same decisions using a different \glspl{variable}, possibly of different types
Note that the new \glspl{constraint} can represent the same decisions using a different \glspl{variable}, possibly of different types
},
}
@ -455,7 +460,7 @@
description={
Problem parameters are part of the external input for a \gls{model}.
They can be used as immutable data used to define \glspl{constraint} or provide structural information about an \gls{instance}.
For example, a problem parameter might influence the number of \glspl{constraint} in an \gls{instance}
For example, a problem parameter can influence the number of \glspl{constraint} in an \gls{instance}
},
}
@ -546,7 +551,7 @@
description={A chronological account of changes to data structures with as goal to possibly reverse these changes. The usage of a trail is a common way for \gls{solver} to revisit search decisions (\ie{} \gls{backtrack})},
}
\newglossaryentry{gls-trs}{
\newglossaryentry{trs}{
name={term rewriting system},
description={A computational model that expresses computation through the application of rewriting rules. A rewriting rule replaces the \glspl{term} on its left hand side with the \glspl{term} on its right hand side},
}
@ -560,7 +565,7 @@
name={decision variable},
description={
A formalised decision that is yet to be made.
When searching for a \gls{sol} a decision variable is said to have a certain \gls{domain}, which contains the values that the decision variable might still take.
When searching for a \gls{sol} a decision variable is said to have a certain \gls{domain}, which contains the values that the decision variable can still take.
If at any point the \gls{domain} is reduced to a single value, then the decision variable is said to be \gls{fixed}.
If, however, a decision variable has an empty \gls{domain}, then there is no value it can take that is consistent with the \glspl{constraint}
},

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.

11
assets/listing/back_knapsack.fzn Normal file
View File

@ -0,0 +1,11 @@
var 0..1: selection_0;
var 0..1: selection_1;
var 0..1: selection_2;
var 0..175: total_joy:: is_defined_var;
constraint int_lin_le([32,8,40], [selection_0,selection_1,selection_2], 44);
constraint int_lin_eq(
[63,12,100,-1],
[selection_0,selection_1,selection_2,total_joy],
0
);
solve maximize total_joy;

10
chapters/1_introduction.tex
View File

@ -8,8 +8,8 @@ We can think, for instance, about the decision on the country's train system or
Formally, we define a \gls{dec-prb} as a set of \variables{} subject to a set of logical \constraints{}.
A \gls{sol} to such a problem is the \gls{assignment} of all \variables{} to values that abide by the logic of the \constraints{}.
These problems are also highly computationally complex: even with the fastest computers there is no simple way to find a solution.
They get even more complex when we consider \gls{opt-prb}: if there are multiple solution, one might be preferred over the other.
But, although these problems might be hard to solve, finding a (good) solution for these problems is essential in many walks of life.
They get even more complex when we consider \gls{opt-prb}: if there are multiple solution, one may be preferred over the other.
But, although these problems are hard to solve, finding a (good) solution for these problems is essential in many walks of life.
The field of \gls{or} uses advanced computational methods to help make (better) decisions.
Famous classes decision and \glspl{opt-prb}, such as \gls{sat} \autocite{biere-2021-sat}, \gls{cp} \autocite{rossi-2006-cp} and \gls{mip} \autocite{wolsey-1988-mip}, have been studied extensively.
@ -26,7 +26,7 @@ Its \constraints{} have to be in the form of disjunctions of Boolean \variables{
But, not only does the encoding have to be correct, the encoding also has to be performant.
There are often many possible correct encodings of a problem, but there can be a significant difference in how quickly the \solver{} finds a \gls{sol} for them.
The preferred encoding can however differ between \solvers{}.
Two \solvers{} designed to solve the same problem class might perform very differently.
Two \solvers{} designed to solve the same problem class can perform very differently.
\Cmls{} have been designed to tackle these issues.
They serve as a level of abstraction between the user and the \solver{}.
@ -101,7 +101,7 @@ Instead, it enforces one, test if this works, and otherwise enforce the other.
This is a powerful mechanism where any choices are made in the \gls{rewriting} process, and not in the \solver{}.
The problem with the mechanism is that it requires a highly incremental interface with the \solver{} that can incrementally post and retract \constraints{}.
Additionally, \solvers{} might not always be able to verify if a certain set of \constraints{} is consistent.
Additionally, \solvers{} are not always be 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.
As such, a \gls{clp} program is not \solver{}-independent.
@ -182,7 +182,7 @@ In particular:
\item The reasoning about \gls{reif} in the \minizinc{} \compiler{} is limited.
An important decision that is made during \gls{rewriting} is if a \constraint{} can be enforced directly or if it is dependent on other \constraints{}.
In the second case, a \gls{reif} has to be introduced, a often costly form of the \constraint{} that determines whether a \constraint{} holds rather than enforcing the \constraint{} itself.
It is possible, however, that further \gls{rewriting} might reveal a \gls{reif} to be unnecessary.
It is possible, however, that further \gls{rewriting} can reveal a \gls{reif} to be unnecessary.
Currently, the \compiler{} cannot reverse any \gls{reif} decisions once they are made.
And, it also does not consider \gls{half-reif}, a cheaper alternative to \gls{reif} that is often applicable.

106
chapters/2_background.tex
View File

@ -32,7 +32,7 @@ Many \cmls{} also support the modelling of \gls{opt-prb}, where a \gls{dec-prb}
In this case the goal is to find a \gls{sol} that satisfies all \constraints{} while minimising (or maximising) 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{}.
To solve these \instances{}, however, they might have to go through a \gls{rewriting} process to arrive at a \gls{slv-mod}, input accepted by a \solver{}.
To solve these \instances{}, however, they can go through a \gls{rewriting} process to arrive at a \gls{slv-mod}, input accepted by a \solver{}.
The \solver{} then uses a dedicated algorithm that finds a \gls{sol} that fits the requirements of the \instance{}.
This process of a \cml{} is visualised in \cref{fig:back-cml-flow}.
@ -107,10 +107,10 @@ Its expressive language and extensive library of \glspl{global} allow users to e
\begin{listing}
\mznfile{assets/listing/back_knapsack.mzn}
\caption{\label{lst:back-mzn-knapsack} A \minizinc\ model describing a 0-1 knapsack problem}
\caption{\label{lst:back-mzn-knapsack} A \minizinc{} model describing a 0-1 knapsack problem}
\end{listing}
One might note that, although more textual and explicit, the \minizinc\ model definition is very similar to our earlier mathematical definition.
Note that, although more textual and explicit, the \minizinc{} model definition is very similar to our earlier mathematical definition.
A \minizinc{} model cannot be solved directly.
It first need to be transformed into a \gls{slv-mod}: a list of \variables{} and \constraints{} \gls{native} to the \solver{}.
@ -124,7 +124,7 @@ It is the primary way in which \minizinc{} communicates with \solvers{}.
\begin{example}
For example, given the \minizinc{} model in \cref{lst:back-mzn-knapsack} and the \gls{assignment}
For example, given the \minizinc{} model in \cref{lst:back-mzn-knapsack} and the following \gls{assignment} will result in the \flatzinc{} \gls{slv-mod} in \cref{lst:back-fzn-knapsack}.
\begin{mzn}
TOYS = {football, tennisball, stuffed_elephant};
@ -133,21 +133,10 @@ It is the primary way in which \minizinc{} communicates with \solvers{}.
space_left = 44;
\end{mzn}
\noindent{}the following \flatzinc{} \gls{slv-mod} might be the result of \gls{rewriting}:
\begin{mzn}
var 0..1: selection_0;
var 0..1: selection_1;
var 0..1: selection_2;
var 0..175: total_joy:: is_defined_var;
constraint int_lin_le([32,8,40], [selection_0,selection_1,selection_2], 44);
constraint int_lin_eq(
[63,12,100,-1],
[selection_0,selection_1,selection_2,total_joy],
0
);
solve maximize total_joy;
\end{mzn}
\begin{listing}
\mznfile{assets/listing/back_knapsack.fzn}
\caption{\label{lst:back-fzn-knapsack} A \flatzinc{} \gls{slv-mod} resulting from \gls{rewriting} \cref{lst:back-mzn-knapsack} with a given complete \gls{parameter-assignment}.}
\end{listing}
This \gls{slv-mod} is then passed to a \solver{}.
The \solver{} attempts to determine a complete \gls{variable-assignment}, \mzninline{selection_@\(i\)@} and \mzninline{total_joy}, that satisfies all constraints and maximises \mzninline{total_joy}.
@ -166,7 +155,7 @@ The structure of a \minizinc{} model can be described directly in terms of a \cm
\item and the \gls{objective} is included as a solving goal.
\end{itemize}
More complex models might 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.
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}.
@ -188,11 +177,11 @@ Two declarations with the same identifier result in an error during the \gls{rew
The main types used in \minizinc{} are Boolean, integer, floating point numbers, sets of integers, and (user-defined) enumerated types.
The declaration of \parameters{} and \variables{} are distinguishes through their type.
The type of a \variable{} is preceded by the \mzninline{var} keyword.
The type of a \parameter{} might similarly be marked by the \mzninline{par} keyword, but this is not required.
The type of a \parameter{} can similarly be marked by the \mzninline{par} keyword, but this is not required.
These types are used both as normal \parameters{} and as \variables{}.
To better structure models, \minizinc{} allows collections of these types to be contained in \glspl{array}.
Unlike other languages, \glspl{array} have a user defined index set, which can start at any value, but they have to be a continuous range.
For example, an array going from 5 to 10 of new Boolean \variables{} might be declared as
For example, the following declaration declares an array going from 5 to 10 of new Boolean \variables{}.
\begin{mzn}
array[5..10] of var bool: bs;
@ -254,12 +243,12 @@ As an example, we can define a function that squares an integer as follows.
\Gls{rewriting} (eventually) transforms all \minizinc{} expressions into function calls.
As such, the usage of function declarations is the primary method for \solvers{} to specify how to rewrite a \minizinc{} model into a \gls{slv-mod}.
The collection of functions declarations to rewrite for a \solver{} is generally referred to as a \solver{} library.
In this library, functions might 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{}.
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}.
\Solver{} implementers are, however, not forced to provide a definition for all functions in \minizinc{}'s extensive library.
Instead, they might rely on a set of standard declaration, 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 declaration, known as the standard library, that rewrite functions into a minimal subset of \gls{native} functions, known as the \flatzinc{} built-ins.
\subsection{MiniZinc Expressions}%
\label{subsec:back-mzn-expr}
@ -291,7 +280,7 @@ This \gls{global} expresses the knapsack relationship, where the argument:
\item and \mzninline{W} and \mzninline{P}, respectively, represent the weight and profit of the knapsack
\end{itemize}
Note that the usage of this \gls{global} might have simplified the \minizinc{} model in \cref{ex:back-mzn-knapsack}:
Note that the usage of this \gls{global} would have simplified the \minizinc{} model in \cref{ex:back-mzn-knapsack}:
\begin{mzn}
var 0..total_space: space_used;
@ -299,7 +288,7 @@ Note that the usage of this \gls{global} might have simplified the \minizinc{} m
\end{mzn}
\noindent{}This has the additional benefit that the knapsack structure of the problem is then known.
The \constraint{} can be rewritten using specialised \gls{decomp} provided by the \solver{} or it might even be marked as \gls{native} \constraint{}.
The \constraint{} can be rewritten using specialised \gls{decomp} provided by the \solver{} or it can be marked as \gls{native} \constraint{}.
Although \minizinc{} contains an extensive library of \glspl{global}, many problems contain structures that are not covered by a \gls{global}.
There are many other types of expressions in \minizinc{} that help modellers express complex \constraints{}.
@ -375,7 +364,7 @@ This means that the \solver{} still will decide if the element is present in the
\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 its resulting expression.
Additionally, a \gls{let} might contain \constraints{} to constrain the declared values.
Additionally, a \gls{let} can contain \constraints{} to constrain the declared values.
There are three main purposes for \glspl{let}:
\begin{enumerate}
@ -411,8 +400,8 @@ There are three main purposes for \glspl{let}:
\noindent{}returns an \gls{ivar} \mzninline{z} that is constrained to be the multiplication of \mzninline{x} and \mzninline{y} by the relational multiplication constraint \mzninline{pred_int_times}.
\end{enumerate}
An important detail in \gls{rewriting} \glspl{let} is that any \variables{} that are introduced might need to be renamed in the resulting \gls{slv-mod}.
Different \variables{} declared directly in declaration items, the \variables{} declared in \glspl{let} might be flattened multiple times when used in loops, function definitions (that are called multiple times), and \gls{array} \glspl{comprehension}.
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 \variables{} declared directly in declaration items, the \variables{} declared in \glspl{let} can be flattened 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.
\paragraph{Annotations} Although \minizinc{} does not typically prescribe a way to find the \gls{sol} for an \instance{}, it does provide the modeller a way to give ``hints'' to the \solver{}.
@ -430,7 +419,7 @@ Through the use of an \gls{annotation} on the solving goal item, the modeller ca
With the rich expression language in \minizinc{}, \constraints{} can consist of complex expressions that cannot be rewritten into a single \constraint{} in the \gls{slv-mod}.
Different parts of a complex expression are rewritten into different \constraints{}.
However, not all part of the expression are autonomous \constraints{} that can be directly enforced by the solver.
Some parts might have to be \reified{} into a Boolean variable.
Some parts have to be \reified{} into a Boolean variable.
The \gls{reif} of a \constraint{} \(c\) creates an \gls{ivar} \mzninline{b} constrained to be the truth-value of this \constraint{}: \(\texttt{b} \leftrightarrow{} c\).
\begin{example}
@ -457,7 +446,8 @@ In \minizinc{}, almost all expressions can be used in both \rootc{} and non-\roo
In this subsection we discuss the handling of partial expressions in \cmls{} as studied by \textcite{frisch-2009-undefinedness}.
Some expressions in \cmls{} do not have well-defined results.
When an expression has a well-defined result it is said to be total.
Some expressions in \cmls{}, however, do not have well-defined results.
Part of the semantics of a \cml{} is the choice as to how to treat these partial functions.
\begin{example}\label{ex:back-undef}
@ -500,7 +490,7 @@ Other examples of \minizinc{} expressions that result in partial functions are:
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{}.
Frisch and Stuckey 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}
@ -515,7 +505,7 @@ Frisch and Stuckey define three semantic models to deal with the undefinedness i
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{}.
So even though a (functional) expression in itself might not have a well-defined result, we can still decide whether its surrounding relationship holds.
So even though a (functional) expression does not have a well-defined result, we can still decide whether its surrounding relationship holds.
For example, the expression \mzninline{x div 0} is undefined, but the relationship \mzninline{int_div(x, 0, y)} is said to be \mzninline{false}.
It can be said that the relational semantic makes the closest relational expression that contains an undefined expression \mzninline{false}.
@ -525,7 +515,7 @@ In practice, it is often natural to guard against undefined behaviour using Bool
\Glspl{rel-sem} therefore often feel the most natural for the users of constraint modelling languages.
This is why the \minizinc{} uses \glspl{rel-sem} during its evaluation.
For example, one might deal with a zero divisor using a disjunction:
For example, the following \constraint{} shows how we can deal with a zero divisor using a disjunction.
\begin{mzn}
constraint d == 0 \/ a div d < 3;
@ -534,7 +524,7 @@ For example, one might deal with a zero divisor using a disjunction:
In this case we expect the undefinedness of the division to be contained within the second part of the disjunction.
This corresponds to \glspl{rel-sem}.
Frisch and Stuckey also show that different \solvers{} often employ different semantics.
\textcite{frisch-2009-undefinedness} also show that different \solvers{} often employ different semantics.
It is therefore important that the \gls{rewriting} process replaces any potentially undefined expression by an \gls{eqsat} expression that is valid under a \gls{strict-sem}.
This essentially eliminates the existence of undefined expressions in the \gls{slv-mod}.
@ -562,8 +552,7 @@ To understand these \gls{rewriting} challenges, the remainder of this section di
\label{subsec:back-cp}
\glsreset{cp}
When given an \instance{} of a \cmodel{}, one might wonder how to find a \gls{sol}.
When given an \instance{} of a \cmodel{}, one may wonder how to find a \gls{sol}.
The simplest solution would be to apply ``brute force'': try every value in the \domains{} of all \variables{}.
This is an inefficient approach.
Given, for example, the constraint
@ -580,6 +569,7 @@ A \gls{cp} \solver{} performs a depth first search.
Using a mechanism called \gls{propagation} the \solver{} removes values from \domains{} that are no longer possible.
\Gls{propagation} works through the use of \glspl{propagator}: algorithms dedicated to a specific \constraint{} that prune \domains{} when its contains values that are proven to be inconsistent.
This mechanism can be very efficient because a \gls{propagator} only has to be run again if the \domains{} of one of its \variables{} has changed.
If a \gls{propagator} can prove that it is always \gls{satisfied}, then it is subsumed: it never has to be run again.
In the best case scenario, \gls{propagation} eliminates all impossible values and all \variables{} have been \gls{fixed} to a single value.
In this case we have arrived at a \gls{sol}.
@ -590,7 +580,7 @@ This search decision is an assumption made by the \solver{} in the hope of findi
If no \gls{sol} is found using the search decision, then it needs to try making the opposite decision which requires the exclusion of the chosen value or adding the opposite \constraint{}.
Note that there is an important difference between values excluded by \gls{propagation} and making search decisions.
Values excluded by propagation are guaranteed to not occur in any \gls{sol}, whereas, values excluded by a search heuristic are merely removed locally and might still be part of a \gls{sol}.
Values excluded by propagation are guaranteed to not occur in any \gls{sol}, whereas, values excluded by a search heuristic are merely removed locally and can still be part of a \gls{sol}.
A \gls{cp} \solver{} is only able to prove that the \instance{} is \gls{unsat} by trying all possible search decisions.
\Gls{propagation} is not only used when starting the search, but also after making each search decision.
@ -607,7 +597,7 @@ Furthermore, because \gls{propagation} is performed to a \gls{fixpoint}, it is g
The solving method used by \gls{cp} \solvers{} is very flexible.
A \solver{} can support many types of \variables{}: they can range from Boolean, floating point numbers, and integers, to intervals, sets, and functions.
Similarly, \solvers{} do not all have access to the same \glspl{propagator}.
Therefore, a \gls{slv-mod} for one \solver{} might look very different from an \gls{eqsat} \gls{slv-mod} for a different \solver{}.
Therefore, a \gls{slv-mod} for one \solver{} looks very different from an \gls{eqsat} \gls{slv-mod} for a different \solver{}.
\cmls{}, like \minizinc{}, serve as a standardised form of input for these \solvers{}.
They allow modellers to use always use \glspl{global} and depending on the \solver{} they are either used directly, or they are automatically rewritten using a \gls{decomp}.
@ -679,9 +669,9 @@ In \gls{cp} solving there is a trade-off between the amount of time spend propag
The golden standard for a \gls{propagator} is to be \gls{domain-con}.
A \gls{domain-con} \gls{propagator} leaves only values in the \domains{} when there is at least one possible \gls{variable-assignment} that satisfies its \constraint{}.
Designing such a \gls{propagator} is, however, not an easy task.
The algorithm might require high computational complexity.
The algorithm can require high computational complexity.
Instead, it is sometimes be better to use a propagator with a lower level of consistency.
Although it might not eliminate all possible values of the domain, searching the values that are not eliminated might take less time than achieving \gls{domain-con}.
Although it does not eliminate all possible values of the domain, searching the values that are not eliminated may take less time than achieving \gls{domain-con}.
This is, for example, the case for integer linear constraints: \[ \sum_{i} c_{i} x_{i} = d\] where \(c_{i}\) and \(d\) are integer \parameters{} and \(x_{i}\) are integer \variable{}.
For these constraints, no realistic \gls{domain-con} \gls{propagator} exists because the problem is \gls{np}-hard \autocite{choi-2006-fin-cons}.
@ -752,7 +742,7 @@ To solve a \instance{} of a \cmodel{}, it can be encoded as a mixed integer prog
This process is known as \gls{linearisation}.
It does, however, come with its challenges.
Most \constraints{} in a \minizinc{} model are not linear equations.
The translation of a single \constraint{} might introduce many linear \constraints{} and even new \variables{}.
The translation of a single \constraint{} can introduce many linear \constraints{} and even new \variables{}.
For example, when a \constraint{} reasons about the value that a variable takes, the \gls{linearisation} process introduces indicator variables.
The indicator variables \(y_{i}\) are \glspl{ivar} 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}\).
@ -787,7 +777,7 @@ The indicator variables \(y_{i}\) are \glspl{ivar} that for a \variable{} \(x\)
\glsreset{sat}
\glsreset{maxsat}
The study of the \gls{sat} problem might be one of the oldest in computer science.
The study of the \gls{sat} problem is one of the oldest in computer science.
The DPLL algorithm that is used to this day stems from the 60s \autocite{davis-1960-dpll, davis-1962-dpll}, and \gls{sat} was the first problem to be proven to be \gls{np}-complete \autocite{cook-1971-sat}.
The problem asks if there is an \gls{assignment} for the \variables{} of a given Boolean formula, such that the formula is \gls{satisfied}.
This problem is a restriction of the general \gls{dec-prb} where all \variables{} have a Boolean type.
@ -799,12 +789,12 @@ These are Boolean \variables{} \(x\) or their negations \(\neg x\).
These literals are then used in a conjunction of disjunctive clauses: a Boolean formula in the form \(\forall \exists b_{i}\).
To solve the \gls{sat} problem, the \solver{} has to find an \gls{assignment} for the \variables{} where at least one literal is true in every clause.
Even though the problem is proven to be hard to solve, a lot of progress has been made towards solving even the biggest the most complex \gls{sat} problems.
Even though the problem is proven to be hard to solve, much progress has been made towards solving even the biggest the most complex \gls{sat} problems.
Modern day \gls{sat} solvers, like Clasp \autocite{gebser-2012-clasp}, Kissat \autocite{biere-2021-kissat} and MiniSAT \autocite{een-2003-minisat} , solve instances of the problem with thousands of \variables{} and clauses.
Many real world problems modelled using \cmls{} directly correspond to \gls{sat}.
However, even problems that contain \variables{} with types other than Boolean can still be encoded as a \gls{sat} problem.
Depending on the problem, using a \gls{sat} \solvers{} to solve the encoded problem might still be the most efficient way to solve the problem.
Depending on the problem, using a \gls{sat} \solvers{} to solve the encoded problem can still be the most efficient way to solve the problem.
\begin{example}
Let us once more consider the N-Queens problem presented in \cref{ex:back-nqueens}.
@ -847,9 +837,9 @@ For many problems the use of \gls{maxsat} \solvers{} offers a very successful me
Although \minizinc{} is the \cml{} that is the primary focus of this thesis, there are many other \cmls{}.
Each \cml{} has its own focus and purpose and comes with its own strength and weaknesses.
Most of the techniques that are discusses in this thesis might be adapted to these languages.
Most of the techniques that are discusses in this thesis may be adapted to these languages.
We now discuss some other prominent \cmls{} and compare them to \minizinc{} to indicate to the reader where techniques might have to be adjusted to fit other languages.
We now discuss some other prominent \cmls{} and compare them to \minizinc{} to indicate to the reader where techniques will need to be adjusted to fit other languages.
A notable difference between all these languages and \minizinc{} is that only \minizinc{} allows modellers to extend the language using their own (user-defined) functions.
In other \cmls{} the modeller is restricted to the expressions and functions provided by the language.
@ -987,7 +977,7 @@ When solving a scheduling problem, the \gls{opl} makes use of specialised interv
It first states the resource objects and then merely has to use the \texttt{requires} keyword to force tasks on the same machine to be mutually exclusive.
In \minizinc{} the same requirement is implemented through the use of \mzninline{disjunctive} constraints.
Although this has the same effect, all mutually exclusive jobs have to be combined in a single statement in the model.
This might make it harder in \minizinc{} to write the correct \constraint{} and its meaning might be less clear.
This makes it harder in \minizinc{} to write the correct \constraint{} and its meaning is less clear.
\end{example}
The \gls{opl} also contains a specialised search syntax that is used to instruct its solvers \autocite{van-hentenryck-2000-opl-search}.
@ -1141,7 +1131,7 @@ The goal of a constraint logic program is to rewrite all \constraints{} in such
Variables{} are another notable difference between \cmls{} and \gls{clp}.
In \gls{clp}, like in a conventional \gls{trs}, a variable is merely a name.
The symbol might be replaced or equated with a constant symbol, but, different from \cmls{}, this is not a requirement.
The symbol can be replaced or equated with a constant symbol, but, different from \cmls{}, this is not a requirement.
A variable can remain a name in the solution of a constraint logic program.
This means that the solution of a constraint logic program can be a relationship between different variables.
In cases where an instantiated solution is required, a special \mzninline{labeling} \constraint{} is used to force a variable to take a constant value.
@ -1281,7 +1271,7 @@ Once the \gls{generator} is exhausted, the compiler rewrites its surrounding exp
The \gls{decomp} system in \minizinc{} is defined in terms of functions declarations.
Any call, whose declaration has a function body, is eventually replaced by an instantiation of this function body using the arguments to the call.
Calls are, however, not the only type of expression that are decomposed during the \gls{rewriting} process.
Other expression, like \gls{operator} expressions, variable array access, and if-then-else expressions, might also have to be decomposed for the target \solver{}.
Other expression, like \gls{operator} expressions, variable array access, and if-then-else expressions, may also have to be decomposed for the target \solver{}.
During the \gls{rewriting} process, these expressions are rewritten into equivalent call expressions that start the decomposition process.
A notable effect of the \gls{rewriting} is that sub-expression are replaced by literals or identifiers.
@ -1328,7 +1318,7 @@ The creation of this new \variable{} and defining \constraints{} happens in one
These are the basic steps that are followed to rewrite \minizinc{} instance.
This is, however, not the complete process.
The quality of the resulting \gls{slv-mod} is of the utmost importance.
A \gls{slv-mod} containing extra \variables{} and \constraints{} that do not add any information to the solving process might exponentially slow it down.
A \gls{slv-mod} containing extra \variables{} and \constraints{} that do not add any information to the solving process can exponentially slow it down.
Therefore, the \minizinc{} \gls{rewriting} process is extended using many techniques to help improve the quality of the \gls{slv-mod}.
In \crefrange{subsec:back-cse}{subsec:back-delayed-rew}, we discuss the most important techniques used to improve the \gls{rewriting} process.
@ -1376,7 +1366,7 @@ Some expressions only become syntactically equal when instantiated, as in the fo
Although the expressions \mzninline{pow(a, 2)} and \mzninline{pow(b, 2)} are not syntactically equal, the function call \mzninline{pythagoras(i,i)} using the same \variable{} for \mzninline{a} and \mzninline{b} makes them equivalent.
\end{example}
To ensure that the same instantiation of a function are only evaluated once, the \minizinc{} \compiler{} uses memorisation.
To ensure that the same instantiation of a function are only evaluated once, the \minizinc{} \compiler{} uses memoisation.
After the \gls{rewriting} of an expression, the instantiated expression and its result are stored in a lookup table: the \gls{cse} table.
Then before any consequent expression is flattened the \gls{cse} table is consulted.
If an equivalent expression is found, then the accompanying result is used; otherwise, the evaluation proceeds as normal.
@ -1423,9 +1413,9 @@ This is a simple form of \gls{propagation}, which, as discussed in \cref{subsec:
The principles of \gls{propagation} can also be applied during the \gls{rewriting} of a \minizinc{} model.
It is generally a good idea to detect cases where we can directly change the \gls{domain} of a \variable{}.
Sometimes this might mean that the \constraints{} does not need to be added at all and that constricting the \gls{domain} is enough.
Sometimes this means that the \constraints{} does not need to be added at all and that constricting the \gls{domain} is enough.
Tight domains also allow us to avoid the creation of \glspl{reif} when the truth-value of a reified \constraint{} can be determined from the \domains{}.
Finally, it can also be helpful for \solvers{} as they might need to decide on a representation of \variables{} based on their initial \domain{}.
Finally, it can also be helpful for \solvers{} as they may need to decide on a representation of \variables{} based on their initial \domain{}.
\begin{example}%
\label{ex:back-adj-dom}
@ -1517,7 +1507,7 @@ On the other hand, evaluating a predicate may also \emph{impose} new bounds on \
The same problem occurs with \glspl{reif} that are produced during \gls{rewriting}.
Other \constraints{} could fix the \domain{} of the reified \variable{} and make the \gls{reif} unnecessary.
Instead, the \constraint{} (or its negation) might be flattened in \rootc{} context.
Instead, the \constraint{} (or its negation) can be flattened in \rootc{} context.
This could avoid the use of a big \gls{decomp} or an expensive \gls{propagator}.
To tackle this problem, the \minizinc{} \compiler{} employs \gls{del-rew}.
@ -1528,7 +1518,7 @@ All other \constraints{}, that are not yet rewritten and could change the releva
Note that this heuristic does not guarantee that \variables{} have their tightest possible \gls{domain}.
One delayed \constraint{} can still influence the \domains{} of \variables{} used by other delayed \constraints{}.
Delaying the rewriting of constraints might also interfere with the \gls{aggregation}.
Delaying the rewriting of constraints also interferes with \gls{aggregation}.
Since \gls{aggregation} is eagerly performed only when a \constraint{} is first encountered, it cannot aggregate any \constraints{} that follow from delayed values.
For example, if when aggregating Boolean clauses comes across an expression that needs to be reified, then a new Boolean \variable{} is created and the reified \constraint{} is delayed.
The problem is, however, that if the definition of this \gls{reif} turn out to be in terms of Boolean clauses as well, then this definition could have been aggregated as well.
@ -1539,12 +1529,12 @@ Because the \compiler{} does not revisit \gls{aggregation}, this does not happen
After the \compiler{} is done \gls{rewriting} the \minizinc{} instance, it enters the optimisation phase.
This phase occurs at the level at which the targeted \solver{} operates.
Depending on this \solver{}, the \minizinc{} \compiler{} might still understand the meaning of certain \constraints{}.
Depending on this \solver{}, the \minizinc{} \compiler{} may still understand the meaning of certain \constraints{}.
In these cases, \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 main focus of the \compiler{} is to propagate Boolean \constraints{}.
The \compiler{} tries to reduce the number of Boolean \variables{} and tries to reduce the number of literals in clauses and conjunctions.
The additional \gls{propagation} might fix the result of the \gls{reif} of a \constraint{}.
The additional \gls{propagation} can fix the result of the \gls{reif} of a \constraint{}.
If this \constraint{} is not yet rewritten, then the \solver{} knows to use a direct \constraint{} instead of a reified version.
Even more important than the Boolean \constraints{}, are equality \constraints{}.

417
chapters/3_rewriting.tex
View File

@ -9,62 +9,77 @@
\label{sec:rew-arch}
\noindent{}\Gls{rewriting} a \minizinc{} instance into \gls{slv-mod} might often seem like a simple \gls{trs}.
In reality, however, only applying the \glspl{decomp} of \constraints{} to the \instance{} will often result in a sub-optimal \gls{slv-mod}.
This might result in exponentially more work for the \solver{}.
In reality, however, \minizinc{} is quite a complex language, and producing a good \gls{slv-mod} is far from trivial.
Thus, in practice, this rewriting process is a highly complex task that needs to carefully track interactions between \constraints{} and how they affect \variables{}.
To create an efficient \glspl{slv-mod} the \gls{rewriting} process uses many simplification techniques such as:
To create an efficient \gls{slv-mod} the \gls{rewriting} process uses many simplification techniques such as:
\begin{itemize}
\item continuously updating \variable{} \domains{},
\item using specialised \glspl{decomp} when variables get fixed,
\item \gls{propagation} for known \constraints{},
\item specialised \glspl{decomp} when variables get \gls{fixed},
\item \gls{aggregation},
\item \glsxtrlong{cse},
\item and removing \variables{} and \constraints{} that are no longer required.
\end{itemize}
We now present a new architecture for the \gls{rewriting} process that has been designed for the modern day needs of \minizinc{}.
At the core of our \gls{rewriting} process lie formalised rewriting rules.
These rules makes it easy to reason about system and about the simplifications both to the process and the resulting \gls{slv-mod}.
At the core of our \gls{rewriting} process lie formalised rewriting rules.
As such, this architecture represent an abstract machine model for \minizinc{}.
These rules allow us to reason about the system and about the simplifications both to the process and the resulting \gls{slv-mod}.
The process can even be made incremental: in \cref{ch:incremental} we discuss how when making incremental changes to the \minizinc{} model, no recompilation is required for the unchanged parts.
\begin{figure}
\centering
\includegraphics[width=\linewidth]{assets/img/rew_compilation_structure}
\caption{\label{fig:rew-comp} The proposed process for the compilation of \minizinc\ instances.}
\caption{\label{fig:rew-comp} The proposed process for the compilation of \minizinc{} instances.}
\end{figure}
The process of the new architecture is shown in \cref{fig:rew-comp}.
After parsing and typechecking, a \minizinc{} model is first compiled into a smaller constraint language called \microzinc{}, independent of the data.
After the \microzinc{} is transformed into a \gls{byte-code} for an \interpreter{}.
This \interpreter{} continuously updates a \cmodel{} according to the \microzinc{} definition.
The \cmodel in the \interpreter is internally represented as a \nanozinc{} program.
\nanozinc{} is a slight extensions of the \flatzinc{} format.
The \interpreter{} finishes when it reaches a \gls{slv-mod}
For efficient execution, the \microzinc{} is then transformed into a \gls{byte-code}.
Together, the \gls{byte-code} and a complete \gls{parameter-assignment}, form an \instance{} that can be executed by the \microzinc{} \interpreter{}.
During its execution, the \interpreter{} continuously updates a \cmodel{} according to the \microzinc{} definition.
The \cmodel{} in the \interpreter{} is internally represented as a \nanozinc{} program.
\nanozinc{} is a slight extension of the \flatzinc{} format.
The \interpreter{} finishes when it reaches a \gls{slv-mod}.
We have developed a prototype of this tool chain, and present experimental validation of these advantages.
The prototype is still very experimental, but preliminary results suggest the new tool chain can perform flattening much faster, and produce better models, than the current \minizinc\ compiler.
We have developed a prototype of this tool chain, and present experimental validation that the new tool chain can perform \gls{rewriting} much faster, and produce better models, than the current \minizinc{} \compiler{}.
\section{\glsentrytext{microzinc} and \glsentrytext{nanozinc}}\label{sec:rew-micronano}
This section introduces the two sub-languages of \minizinc\ at the core of the new abstract machine model we have developed.
This section introduces the two sub-languages of \minizinc{} at the core of the new architecture we have developed.
\microzinc{} is a simplified subset of \minizinc\ that only contains function declarations and a restricted expression language, but it extends \minizinc{}'s type system with tuples.
\Glspl{model} written in \minizinc\ can be translated into \microzinc{}.
\microzinc{} is a simple language used to define the transformations to be performed by the \interpreter{}.
It is simplified subset of \minizinc{}.
The transformation are represented in the language through the use of function definitions.
A function of type \mzninline{var bool}, describing a relationship, can be defined as a \gls{native} \constraint{}.
Otherwise, a function body must be provided for \gls{rewriting}.
The function body can use a restriction of the \minizinc{} expression language.
An important difference between \minizinc{} and \microzinc{} is that a well-formed \microzinc{} does not contain partial expressions.
Any partiality in the \minizinc{} model must be explicitly expressed using total functions in \microzinc{}.
As such, \constraints{} introduced in \microzinc{} \glspl{let} can be globally enforced.
They are guaranteed to only constrain the \variables{} introduced in the same \gls{let}.
\nanozinc{} is used to represent the current state of the \instance{}.
\nanozinc{} is similar to \flatzinc{} in that it contains only declarations of \variables{} and a flat list of \constraints{}.
However, while all function calls in \flatzinc{} need to be \gls{native}, \nanozinc\ calls can refer to any function implemented in \microzinc{}.
Furthermore, \nanozinc{} allows for \constraints{} to be bound to a specific \variable{} and \constraints{} and \variable{} declarations can be interleaved.
However, while all function calls in \flatzinc{} need to be \gls{native}, \nanozinc{} calls can refer to any function implemented in \microzinc{}.
Furthermore, \nanozinc{} allows for \constraints{} to be ``attached'' to a \variable{}, in order to be able to track their lifetime and remove them if the corresponding \variable{} is no longer required.
As a small syntactic difference with \flatzinc{}, \constraints{} and \variable{} declarations in \nanozinc{} can be freely interleaved.
The core of the syntax of \microzinc{} is defined in \cref{fig:rew-uzn-syntax}.
We have omitted the definitions of \syntax{<mzn-type-inst>} and \syntax{<ident>}, which you can assume to be the same as the definition of \syntax{<type-inst>} and \syntax{<ident>} in the \minizinc\ grammar, see \cref{ch:minizinc-grammar}.
While we omit the typing rules here for space reasons, we will assume that in well-typed \microzinc{} programs, the conditions \syntax{<exp>} in if-then-else and where expressions have \mzninline{par} type.
In \microzinc{} it is specifically used to mark functions that are \gls{native} to the target \solver{}.
We have omitted the definitions of \syntax{<mzn-type-inst>} and \syntax{<ident>}, which can be assumed to be the same as the definition of \syntax{<type-inst>} and \syntax{<ident>} in the \minizinc{} grammar, see \cref{ch:minizinc-grammar}.
While we omit the typing rules here for space reasons, we will assume that in well-typed \microzinc{} programs conditional expressions are \parameters{}.
This means that the where conditions \syntax{<exp>} in \glspl{comprehension}, the conditions \syntax{<exp>} in if-then-else expressions, and the \syntax{<literal>} index in array accesses must have \mzninline{par} type.
\begin{figure}
\begin{grammar}
<model> ::= <pred-decl>*<fun-decl>*
<pred-decl> ::= "predicate" <ident>"(" <param> ["," <param>]* ");"
<fun-decl> ::= "function" <type-inst>":" <ident>"(" <param> ["," <param>]* ")" "=" <exp>";"
<fun-decl> ::= "function" <type-inst>":" <ident>"(" <typing> ["," <typing>]* ")" "=" <exp>";"
\alt "function" "var" "bool" ":" <ident>"(" <typing> ["," <typing>]* ")" ";"
<literal> ::= <constant> | <ident>
@ -75,20 +90,21 @@ While we omit the typing rules here for space reasons, we will assume that in we
\alt "[" <exp> "|" <gen-exp> "where" <exp> "]"
\alt <ident>"[" <literal> "]"
<item> ::= <param> [ "=" <exp> ]";"
<item> ::= <typing> [ "=" <exp> ]";"
\alt "tuple(" <type-inst> ["," <type-inst>]* "):" <ident> = "(" <exp> ["," <exp>]* ")";
\alt "(" <param> ["," <param>]* ")" "=" <exp>";"
\alt "(" <typing> ["," <typing>]* ")" "=" <exp>";"
\alt "constraint" <exp>";"
<param> ::= <type-inst>":" <ident>
<typing> ::= <type-inst>":" <ident>
<gen-exp> ::= <ident> "in" <exp> ["," <ident> "in" <exp> ]*
<gen-exp> ::= <ident> "in" <exp> ["," <ident> "in" <exp> ]*
\end{grammar}
\caption{\label{fig:rew-uzn-syntax}Syntax of \microzinc{}.}
\end{figure}
A \nanozinc\ program, defined in \cref{fig:rew-nzn-syntax}, is simply a list of \variable{} declarations and \constraints{} in the form of calls.
The syntax ``\texttt{↳}'' will be used to track dependent constraints (this will be explained in detail in \cref{sec:rew-nanozinc}, for now you can ignore them).
A \nanozinc{} program, defined in \cref{fig:rew-nzn-syntax}, is simply a list of \variable{} declarations and \constraints{} in the form of calls.
The syntax ``\texttt{↳}'' will be used to ``attach'' \constraints{} to \variables{} in order to track dependent \constraints{}.
This will be explained in detail in \cref{sec:rew-nanozinc}.
\begin{figure}
\begin{grammar}
@ -98,60 +114,74 @@ The syntax ``\texttt{↳}'' will be used to track dependent constraints (this wi
<nzn-con> ::= "constraint" <ident>"(" <literal> ["," <literal>]* ")"";"
<nzn-var> ::= "var" <nzn-dom> ":" <ident> ";" <nzn-bind>*
<nzn-var> ::= "var" <nzn-dom> ":" <ident> ";" <nzn-attach>*
<nzn-dom> ::= <constant> ".." <constant> | <constant>
\alt "bool" | "int" | "float" | "set of int"
<nzn-bind> ::= "↳" <nzn-con>
<nzn-attach> ::= "↳" <nzn-con>
\end{grammar}
\caption{\label{fig:rew-nzn-syntax}Syntax of \nanozinc{}.}
\end{figure}
\subsection{\glsentrytext{minizinc} to \glsentrytext{microzinc}/\glsentrytext{nanozinc}}
\subsection{\glsentrytext{minizinc} to \glsentrytext{microzinc}}
The translation from \minizinc\ to \microzinc{} involves the following steps:
The translation from \minizinc{} to \microzinc{} involves the following steps:
\begin{enumerate}
\item Transform all expressions that are valid in \minizinc\ but not in \microzinc{}.
This includes simple cases such as replacing operator expressions like \mzninline{x+y} by function calls \mzninline{int_plus(x,y)}.
\item Transform all expressions that are valid in \minizinc{} but not in \microzinc{}.
This includes simple cases such as replacing operator expressions, like \mzninline{x+y}, by function calls, \mzninline{int_plus(x,y)}, and replacing generators in calls, like \mzninline{sum(x in A)(x)}, by \glspl{comprehension}, \mzninline{sum([x|x in A])}.
As mentioned above, conditional expressions where the decision is made by a \variable{} are also not directly supported in \microzinc{}.
These expressions are therefore also replaced by function calls that are possibly decomposed.
An expression \mzninline{if x then A else B endif}, where \mzninline{x} is a \variable{}, is replaced by a call:
An expression \mzninline{if x then A else B endif}, where \mzninline{x} is a \variable{}, is replaced the following call.
\begin{mzn}
if_then_else([x, true], [A, B])
\end{mzn}
\noindent{}And, an expression \mzninline{A[x]}, where \mzninline{x} is a \variable{}, is replaced by a call:
And, an expression \mzninline{A[x]}, where \mzninline{x} is a \variable{}, is replaced by the following call.
\begin{mzn}
element(A, x)
\end{mzn}
\mzninline{element} is a well-known \gls{global}.
For many \gls{cp} \solvers{} it is a \gls{native} \constraint{} and for other \solvers{} there have long been accepted \glspl{decomp}.
A recent study by \textcite{stuckey-2019-conditionals} describes how \mzninline{if_then_else} can be decomposed for different types of \solvers{}.
\item Replace optional \variables{} into non-optional forms.
As shown by Mears et al., optional variable types can be represented using a \variable{} of the same non-optional type and a Boolean \variable{} \autocite*{mears-2014-option}.
As shown by \textcite{mears-2014-option}, optional type \variables{} can be represented using a \variable{} of the same non-optional type and a Boolean \variable{}.
The Boolean \variable{}, then, represents if the variable exists or is absent, while the non-optional \variable{} of the same type represents the value of the optional \variable{} if it exists.
In \microzinc{} this can be represented as a tuple of the two \variables{}.
The functions definitions for optional types then take both \variables{} into account.
For example, the definition of \mzninline{int_plus(x, y)} for optional types will add the value variable to the result of the function if Boolean \variable exists.
The function definitions for optional types then take both \variables{} into account.
For example, the definition of \mzninline{int_plus(x, y)} for optional types can be translated into the following function.
\begin{mzn}
function var int: int_plus(tuple(var bool, var int): x, tuple(var bool, var int): y) =
let {
(x1, x2) = x;
(y1, y2) = y;
var int: x3 = if_then_else([x1, true], [x2, 0]);
var int: y3 = if_then_else([y1, true], [y2, 0]);
var int: res = int_plus(x3, y3);
} in res;
\end{mzn}
\item Lift the partiality in expressions into the surrounding context to implement \minizinc{}'s relational semantics.
In contrast to \minizinc{}, the evaluation of \microzinc{} will implement strict semantics for partial expressions, whereas \minizinc\ uses relational semantics.
Stuckey and Tack have extensively examined these problems and describe how to transform any partial function into a total function.
\autocite*{stuckey-2013-functions}.
A general approach for describing the partially in \microzinc{} functions is to make the function return an additional Boolean \variable{}.
This \variable{} indicates the totality with regards to the input to the function.
In contrast to \minizinc{}, a \microzinc{} expression must be total.
\textcite{stuckey-2013-functions} have extensively examined these problems and describe how to transform any partial function into a total function while maintaining the relational semantics of the original \cmodel{}.
A general approach for describing the partiality in \microzinc{} functions is to make the function return an additional Boolean \variable{}.
This \variable{} indicates whether the result of the function call is defined with regards to the function parameters.
The resulting value of the function is then adjusted to return a predefined value when it would normally be undefined.
For example, The function
For example, the \mzninline{element} function in \minizinc{} is declared as follows.
\begin{mzn}
function var int: element(array of int: a, var int: x);
\end{mzn}
\noindent{}is only defined when \mzninline{x in index_set(a)}.
A total version to be used in \microzinc{} could look like\footnote{For brevity's sake, we will still use \minizinc{} \glspl{operator} to write the \microzinc{} definition.}:
\noindent{}It is only defined when \mzninline{x in index_set(a)}.
The following function is a total version of this function that can be used in \microzinc{}.\footnote{For brevity's sake, we will still use \minizinc{} \glspl{operator} to write the \microzinc{} definition.}
\begin{mzn}
function tuple(var int, var bool): element_safe(array of int: a, var int: x) =
@ -170,9 +200,9 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
} in ret;
\end{mzn}
Similar to the replacement of optional values, all usage of the \mzninline{element} function are replaced by \mzninline{element_safe}.
Similar to the replacement of optional values, all occurrences of the \mzninline{element} function are replaced by \mzninline{element_safe}.
The usage of its result should be guarded by the returned totality variable in the surrounding Boolean context.
This means that, for example, the expression \mzninline{element(e, v) = 5 \/ b} would be transformed into:
This means that, for example, the expression \mzninline{element(e, v) = 5 \/ b} would be replaced by the following expression.
\begin{mzn}
let {
@ -181,27 +211,29 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
\end{mzn}
\item Resolve sub-type based overloading statically.
To prevent the runtime overhead of the dynamic lookup of overloaded function definitions for every call, the function dispatch in \microzinc\ is determined statically.
To prevent the runtime overhead of the dynamic lookup of overloaded function definitions for every call, the function dispatch in \microzinc{} is determined statically.
It is important, however, that the correct version of a function is chosen when it allows for either \variable{} and \parameter arguments.
It is important, however, that the correct version of a function is chosen when it allows for either \variable{} and \parameter{} arguments.
And, as we will later discuss in more detail, is possible for a \variable{} to be \gls{fixed} to a single value during the \gls{rewriting} process.
At which point it can be treated as a \parameter{}.
At that point it can be treated as a \parameter{}.
To ensure the correct version of the function is used, functions are changed to, at runtime, check if a \variable{} is fixed and, if so, dispatch to the \parameter{} version of the function.
If we, for example, have a \minizinc{} function \mzninline{f} that is overloaded on \mzninline{var int} and \mzninline{int}, then the \microzinc{} transformation might look like:
If we, for example, have a \minizinc{} function \mzninline{f} that is overloaded on \mzninline{var int} and \mzninline{int}, then the \microzinc{} transformation can be described by the following two functions.
\begin{mzn}
function f_int(int: x) = /* original body */;
function f_varint(varint: x) =
function f_varint(var int: x) =
if is_fixed(x) then
f_int(x)
f_int(fix(x))
else
/* original body */;
endif;
\end{mzn}
\item Transform all function definitions so that they do not refer to top-level \variables{}, by adding those \variables{} as extra arguments to the function declaration and each call site.
\item Transform all function definitions so that they do not refer to \variables{} and \parameters{} defined outside the scope of the function.
Instead they are added as extra arguments to the function definition and each call.
\item Move all top-level \variable{} declarations and \constraints{} into a let expression in the body of a new function called \mzninline{main}, whose arguments are the parameters of the model and which returns a fresh Boolean \variable{}.
\item Move all top-level \variable{} declarations and \constraints{} into a let expression in the body of a new function called \mzninline{main}.
The arguments to this function are the top-level \parameters{} of the \minizinc{} model and it returns a fresh Boolean \variable{}.
\end{enumerate}
@ -224,10 +256,12 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
\begin{mzn}
function var bool: all_different(array[int] of var int: x) =
forall([
let {
set of int: S = range(1, length(x));
} in forall([
int_neq(element(x, i),element(x, j))
| i in range(1, length(x)),
j in range(1, length(x))
| i in S,
j in S
where int_lt(i,j)
]);
@ -248,17 +282,17 @@ The translation from \minizinc\ to \microzinc{} involves the following steps:
\subsection{Partial Evaluation of \glsentrytext{nanozinc}}\label{sub:rew-partial}
Each call in a \nanozinc\ program is either a call to a \gls{native} predicate, or it has a corresponding \microzinc\ function definition.
The goal of partial evaluation is to rewrite the \nanozinc{} program into a \gls{slv-mod}, \ie\ a program where all calls are calls to \gls{native} predicates.
Each call in a \nanozinc{} program is either a call to a \gls{native} \constraint{}, or it has a corresponding \microzinc{} function definition.
The goal of partial evaluation is to rewrite the \nanozinc{} program into a \gls{slv-mod}, \ie{} a program where all calls are calls to \gls{native} \constraints{}.
To achieve this, we define the semantics of \microzinc{} as a \gls{rewriting} system that produces \nanozinc{} calls.
Each non-\gls{native} call in a \nanozinc{} program can then be replaced with the result of evaluating the corresponding \microzinc{} function.
A key element of this \gls{rewriting} process, then, is the transformation of functional expressions into relational form.
For this to happen, the \gls{rewriting} process introduces \glspl{ivar} to represent intermediate expressions.
For this to happen, the \gls{rewriting} process introduces fresh \variables{} to represent intermediate expressions.
\begin{example}\label{ex:rew-abs}
Consider the following (reasonably typical) \minizinc\ encoding for the absolute value function:
Consider the following (reasonably typical) \minizinc{} encoding for the absolute value function:
\begin{mzn}
function var int: abs(var int: x) =
@ -279,27 +313,26 @@ If \mzninline{z} is unused in the rest of the model, both \mzninline{z} and the
As we shall see in \cref{sec:rew-simplification}, certain optimisations and simplifications during the evaluation can lead to many expressions becoming unused.
It is therefore important to track which constraints were merely introduced to define results of function calls.
In order to track these dependencies, \nanozinc\ attaches constraints that define a variable to the item that introduces the \variable{}.
In order to track these dependencies, \nanozinc{} attaches constraints that define a variable to the item that introduces the \variable{}.
\subsection{\glsentrytext{nanozinc}}\label{sec:rew-nanozinc}
A \nanozinc\ model (\cref{fig:rew-nzn-syntax}) consists of a topologically-ordered list of declarations of \variables{} and \constraints{}.
\Variables{} are declared with an identifier, a domain, and it is associated with a list of identifiers of auxiliary \constraints{}.
\Constraints{} can also occur at the top-level of the \nanozinc{} model.
These are said to be the ``root-context'' \constraints{} of the model, \ie\ those that have to hold globally and are not just used to define an \gls{ivar}.
A \nanozinc{} program (\cref{fig:rew-nzn-syntax}) consists of a topologically-ordered list of declarations of \variables{} and \constraints{}.
\Variables{} are declared with an identifier, a domain, and are associated with a list of attached \constraints{}.
\Constraints{} can also occur at the top-level of the \nanozinc{} program.
These are said to be the ``root-context'' \constraints{} of the \cmodel{}, \ie{} those that have to hold globally and are not just used to define an \gls{ivar}.
Only root-context \constraints{} can effectively constrain the overall problem.
\Constraints{} attached to \variables{} originate from function calls, and since all functions are guaranteed to be total, attached constraints can only define the function result.
\begin{example}\label{ex:rew-absnzn}
Consider the \minizinc{} fragment
Consider the following \minizinc{} fragment.
\begin{mzn}
constraint abs(x) > y;
\end{mzn}
\noindent{}where \mzninline{x} and \mzninline{y} have domain \mzninline{-10..10}.
After rewriting all definitions, the resulting \nanozinc{} program could look like this:
\noindent{}If we assume that \mzninline{x} and \mzninline{y} have a \domain{} of \mzninline{-10..10}, then after \gls{rewriting}, the resulting \nanozinc{} program could look like this:
\begin{nzn}
var -10..10: x;
@ -319,7 +352,7 @@ The core of the proposed \minizinc{} architecture is an abstract machine that re
We can now formally define the rewriting rules for this abstract machine.
The full set of rules appears in \cref{fig:rew-rewrite-to-nzn-calls,fig:rew-rewrite-to-nzn-let,fig:rew-rewrite-to-nzn-other}.
To simplify presentation, we assume that all rules that introduce new identifiers into the \nanozinc{} program do so in a way that ensures those identifiers are fresh (\ie\ not used in the rest of the \nanozinc\ program), by suitable alpha renaming.
To simplify presentation, we assume that all rules that introduce new identifiers into the \nanozinc{} program do so in a way that ensures those identifiers are fresh (\ie{} not used in the rest of the \nanozinc{} program), by suitable alpha renaming.
\begin{figure*}
\centering
@ -335,29 +368,29 @@ To simplify presentation, we assume that all rules that introduce new identifier
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\texttt{predicate}~\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog}
\infer1[(CallPredicate)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{}
\hypo{\texttt{function var bool:}~\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog}
\infer1[(CallNative)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{}
\tuple{\ensuremath{\texttt{constraint}~\ptinline{F}(a_1, \ldots, a_k), \Env}}}
\end{prooftree}
\caption{\label{fig:rew-rewrite-to-nzn-calls} Rewriting rules for partial evaluation
of \microzinc\ calls to \nanozinc{}.}
of \microzinc{} calls to \nanozinc{}.}
\end{figure*}
The rules in \cref{fig:rew-rewrite-to-nzn-calls} handle function calls.
The first rule, (Call), evaluates a function call expression in the context of a \microzinc\ program \(\Prog{}\) and \nanozinc\ program \(\Env{}\).
The first rule, (Call), evaluates a function call expression in the context of a \microzinc{} program \(\Prog{}\) and \nanozinc{} program \(\Env{}\).
The rule evaluates the function body \(\ptinline{E}\) where the formal parameters \(p_{i}\) are substituted by the call arguments \(a_{i}\).\footnote{We use \(E_{[a \mapsto b]}\) as a notation for the expression \(E\) where \(a\) is substituted by \(b\).} The result of this evaluation is the result of the function call.
The (CallBuiltin) rule applies to ``built-in'' functions that can be evaluated directly, such as arithmetic and Boolean operations on fixed values.
The rule simply returns the result of evaluating the built-in function on the evaluated parameter values.
The (CallPredicate) rule applies to calls to predicates \gls{native} to the \solver{}.
The (CallNative) rule applies to calls to functions for \constraints{} \gls{native} to the \solver{}.
Since these are directly supported by the \solver{}, they simply need to be transferred into the \nanozinc{} program.
\begin{figure*}
\centering
\begin{prooftree}
\hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \emptyset} \Rightarrow \tuple{x, \Env'}}
\infer1[(Let)]{\Sem{let \{ \(\mathbf{I}\) \} in \(\mathbf{X}\)}{\Prog, \Env} \Rightarrow\ \tuple{x, \Env'}}
\infer1[(Let)]{\Sem{let \{ \(\mathbf{I}\) \} in \(\mathbf{X}\)}{\Prog, \Env} \Rightarrow{} \tuple{x, \Env'}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
@ -368,41 +401,42 @@ Since these are directly supported by the \solver{}, they simply need to be tran
\begin{prooftree}
\hypo{\Sem{\(C\)}{\Prog, \Env} \Rightarrow \tuple{c, \Env'}}
\hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env', \{c\}\cup\Ctx} \Rightarrow \tuple{x, \Env''}}
\infer2[(ItemC)]{\Sem{\(\mbox{constraint}~C\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow\ \tuple{x, \Env''}}
\infer2[(ItemC)]{\Sem{\(\mbox{constraint}~C\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env''}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env\ \cup\ \{t : x\}, \Ctx} \Rightarrow \tuple{x, \Env'}}
\hypo{\Sem{\(\mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env{} \cup{} \{t : x\}, \Ctx} \Rightarrow \tuple{x, \Env'}}
\infer1[(ItemT)]{\Sem{\(t\texttt{:}~x\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{v, \Env'}}
\hypo{\Sem{\(\mathbf{I}_{[x \mapsto v]} \mid{} \mathbf{X}_{[x \mapsto v]}\)}{\Prog, \Env', \Ctx} \Rightarrow\ \tuple{x, \Env''}}
\infer2[(ItemTE)]{\Sem{\(t\texttt{:}~x = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow\ \tuple{x, \Env''}}
\hypo{\Sem{\(\mathbf{I}_{[x \mapsto v]} \mid{} \mathbf{X}_{[x \mapsto v]}\)}{\Prog, \Env', \Ctx} \Rightarrow{} \tuple{x, \Env''}}
\infer2[(ItemTE)]{\Sem{\(t\texttt{:}~x = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env''}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\Sem{\(E_{i}\)}{\Prog,\Env^{i-1}} \Rightarrow \tuple{v_{i}, \Env^{i}}, \forall{} 1 \leq{} i \leq{} k}
\infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env^{k}, \Ctx} \Rightarrow\ \tuple{x, \Env'}}
\infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{\langle{}i\rangle} \mapsto v_{i}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env^{k}, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
\infer1[(ItemTupC)]{\Sem{\( \texttt{tuple(}t_{1}, \ldots, t_{k}\texttt{):}~x = \left(E_{1}, \ldots, E_{k}\right)\)}{\Prog, \Env^{0}, \Ctx} \Rightarrow{} \tuple{x, \Env'}}
\end{prooftree} \\
\bigskip
\begin{prooftree}
\hypo{\Sem{\(E\)}{\Prog, \Env} \Rightarrow \tuple{\left(v_{\langle{}1\rangle}, \ldots, v_{\langle{}k\rangle}\right), \Env'}}
\infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env', \Ctx} \Rightarrow\ \tuple{x, \Env''}}
\infer1[(ItemTupD)]{\Sem{\(\left(t_{1}\texttt{:}~x_{1}, \ldots, t_{k}\texttt{:}~x_{k}\right) = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow\ \tuple{x, \Env''}}
\infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env', \Ctx} \Rightarrow{} \tuple{x, \Env''}}
\infer1[(ItemTupD)]{\Sem{\(\left(t_{1}\texttt{:}~x_{1}, \ldots, t_{k}\texttt{:}~x_{k}\right) = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env''}}
\end{prooftree}
\caption{\label{fig:rew-rewrite-to-nzn-let} Rewriting rules for partial evaluation
of \microzinc\ let expressions to \nanozinc{}.}
of \microzinc{} \glspl{let} to \nanozinc{}.}
\end{figure*}
The rules in \cref{fig:rew-rewrite-to-nzn-let} considers let expressions.
The rules in \cref{fig:rew-rewrite-to-nzn-let} consider \glspl{let}.
Starting from the main rule, (Let), the let items \textbf{I} are evaluated one at a time.
\Glspl{constraint} that follow from the evaluation of the let expression, by the (ItemC) rule, are captured in a third evaluation arguments.
When all inner items have been evaluated, the captured \constraints{} are bound to the literal returned by the body of the let expression \textbf{X} in (Item0).
\Glspl{constraint} that follow from the evaluation of the let expression, by the (ItemC) rule, are collected in the third component, \(\phi{}\)
, of the evaluation arguments.
When all inner items have been evaluated, the captured \constraints{} are attached to the literal returned by the body of the let expression \textbf{X} in (Item0).
The (ItemT) rule handles introduction of new \variables{} by adding them to the context.
The (ItemTE) rule handles introduction of new \variables{} with a defining equation by evaluating them in the current context and substituting the name of the new \variable{} by the result of evaluation in the remainder of the namespace.
The (ItemTE) rule handles introduction of new \variables{} with a defining equation by evaluating them in the current context and substituting the name of the new \variable{} by the result of evaluation in the entire scope of the variable.
The rules (ItemTupC) and (ItemTupD) are for the construction and deconstruction of tuple objects.
We use the notation \(x_{\langle{}i\rangle}\) to mark the \(i^{\text{th}}\) member of the tuple \(x\) in our substitution notation.
@ -410,7 +444,7 @@ We use the notation \(x_{\langle{}i\rangle}\) to mark the \(i^{\text{th}}\) memb
\centering
\begin{prooftree}
\hypo{x \in \langle \text{ident} \rangle}
\hypo{\{t: x \texttt{~↳~} \phi\ \} \in \Env}
\hypo{\{t: x \texttt{~↳~} \phi{} \} \in \Env}
\infer2[(Ident)]{\Sem{\(x\)}{\Prog, \Env} \Rightarrow{} \tuple{x, \Env}}
\end{prooftree} \\
\bigskip
@ -454,13 +488,11 @@ We use the notation \(x_{\langle{}i\rangle}\) to mark the \(i^{\text{th}}\) memb
\tuple{\mbox{concat} [ A_v~|~v \in{} S ], \Env{} \cup{} \bigcup{}_{v \in{} S} \Env{}_{v}}}
\end{prooftree}
\caption{\label{fig:rew-rewrite-to-nzn-other} Rewriting rules for partial evaluation
of other \microzinc\ expressions to \nanozinc{}.}
of other \microzinc{} expressions to \nanozinc{}.}
\end{figure*}
Finally, the rules in \cref{fig:rew-rewrite-to-nzn-other} handle the evaluation of \variables{}, constants, conditionals and comprehensions.
For completeness, we give the details here.
The (Ident) rule looks up a \variable{} in the environment and return its bound value (for constants) or the \variable{} itself.
The (Ident) rule looks up a \variable{} in the environment and return its fixed value (for constants) or the \variable{} itself.
The (Const) rule simply returns the constant.
The (If\(_T\)) and (If\(_F\)) rules evaluate the if condition and then return the result of the then or else branch appropriately.
The (WhereT) rule evaluates the guard of a where comprehension and if true returns the resulting expression in a list.
@ -474,7 +506,7 @@ It returns the concatenation of the resulting lists with all the additional \nan
Our prototype implementation of the \microzinc{}/\nanozinc{} framework consists of the following components.
The \gls{compiler} translates \minizinc{} into a \gls{byte-code} encoding of \microzinc{}.
The compiler currently supports a significant subset of the full \minizinc\ language, with the missing features (such floating point values and complex output statements) requiring additional engineering effort but no new technology.
The compiler currently supports a significant subset of the full \minizinc{} language, with the missing features (such floating point values and complex output statements) requiring additional engineering effort but no new technology.
The \gls{interpreter} evaluates \microzinc{} \gls{byte-code} and \nanozinc{} programs based on the \gls{rewriting} system introduced in this section.
It can read \parameters{} from a file or via an \gls{api}.
@ -482,12 +514,10 @@ The \gls{interpreter} constructs the call to the \mzninline{main} function, and
Memory management is implemented using reference counting, which lends itself well to the optimisations discussed in the next section.
The interpreter is written in around 3.5kLOC of C++ to enable easy embedding into applications and other programming languages.
The framework has the ability to multiple \solvers{}.
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.
Additionally, a direct C++ \gls{api} can be used to connect solvers directly, in order to enable incremental solving.
We revisit this topic in \cref{ch:incremental}.
\textbf{Python bindings} to the framework are provided to enable easy scripting.
The source code for the complete system will be made available under an open source license.
\todo{actually make source available}
@ -496,17 +526,18 @@ The source code for the complete system will be made available under an open sou
The previous section introduced the basic evaluation model of \nanozinc: each call that has a corresponding \microzinc{} definition can be rewritten into a set of calls by evaluating the \microzinc{} code.
This section looks at further steps that the system can perform in order to produce better, more compact \glspl{slv-mod}.
\subsection{Removing dead variables and constraints}
\subsection{Removing unused variables and constraints}
The most basic form of simplification is to identify \variables{} that are not used by any call, and remove them.
This is correct because the semantics of \nanozinc{} requires us to find values for all \variables{} such that all \constraints{} are \gls{satisfied} --- but if a \variable{} does not occur in any \constraint{}, we can pick any value for it.
The model without the \variable{} is therefore \gls{eqsat} with the original model.
The model without the unused \variable{} is therefore \gls{eqsat} with the original model.
Consider now the case where a \variable{} in \nanozinc is only used in its own auxiliary definitions (the constraints directly succeeding the declaration prepended by \texttt{↳}).
Consider now the case where a \variable{} in \nanozinc{} is only used in its attached \constraints{}.
The constraints directly succeeding the declaration prepended by \texttt{↳}.
\begin{example}\label{ex:rew-absreif}
The following is a slight variation on the \minizinc{} fragment in \cref{ex:rew-absnzn}:
The following is a slight variation on the \minizinc{} fragment in \cref{ex:rew-absnzn}.
\begin{mzn}
constraint abs(x) > y \/ c;
@ -516,7 +547,8 @@ Consider now the case where a \variable{} in \nanozinc is only used in its own a
The \constraint{} \mzninline{abs(x) > y} is now used in a disjunction.
This means that instead of enforcing the \constraint{} globally, we need to create a \gls{reif}.
Following the rewriting rules, the generated \nanozinc{} code will look very similar to the code generated in \cref{ex:rew-absnzn}, but with an additional \mzninline{bool_or} \constraint{} for the disjunction.
It uses a \variable \mzninline{b} that will be introduced for \mzninline{abs(x) > y}:
It uses a \variable{} \mzninline{b} that will be introduced for \mzninline{abs(x) > y}.
The \gls{rewriting} of this fragment will result in the following \nanozinc{} program.
\begin{nzn}
var true: c;
@ -534,12 +566,12 @@ Consider now the case where a \variable{} in \nanozinc is only used in its own a
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.
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 auxiliary definitions.
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{}.
It was only referenced from the \mzninline{bool_or} call.
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 auxiliary definitions
This in turn means that \mzninline{z} is not referenced anywhere outside its attached \constraints{}.
It can also be removed together with its definition.
The resulting \nanozinc\ program is much more compact:
The resulting \nanozinc{} program is much more compact:
\begin{nzn}
var true: c;
@ -548,17 +580,18 @@ Consider now the case where a \variable{} in \nanozinc is only used in its own a
\end{nzn}
We assume here that \mzninline{c}, \mzninline{x} and \mzninline{y} are used in other parts of the model not shown here and therefore not removed.
Note how counting usage of \variables{} outside its auxiliary definitions allows us to remove the \mzninline{z} variable --- we could not simply have counted the usage of \mzninline{z} in all \constraints{} since the \constraint{} used to define it, \mzninline{int_abs(x, z)}, would have kept it alive.
Note how it is crucial to exclude the attached \constraints{} when counting the usage of \variables{}.
\mzninline{int_abs(x, z)}, the \constraint{} which merely defines \mzninline{z}, would otherwise force us to keep \mzninline{z} in the \nanozinc{} program, if it were included in the count.
\end{example}
It is important to notice the difference between \constraints{} that appear at the top level and \constraints{} that appear as part of the auxiliary definitions of a \variable{}.
Top-level \constraint{} help define the problem, they are globally enforced and cannot be removed from the problem unless it can be proved that its relationship is already enforced.
\Constraints{} in auxiliary definitions, on the other hand, are used to define a \variable{}.
Auxiliary definitions generally occur from a functional relationship, like \mzninline{abs(x)} in the example, or from a \gls{reif}, like \mzninline{abs(x) > y} when used in the disjunction with \mzninline{c}.
In this thesis we will follow the same naming standard as \minizinc{} where a \gls{reif} of a constraint has the same name as the original constraint with \texttt{\_reif} appended.
It is important to notice the difference between \constraints{} that appear at the top level and \constraints{} that appear as part of the attached \constraints{} of a \variable{}.
Top-level \constraints{} help define the problem, they are globally enforced and cannot be removed from the problem unless it can be proved that its relationships are already enforced.
\Constraints{} attached to a \variable{}, on the other hand, are used to define a \variable{}.
\Constraints{} are generally attached when they stem from a functional relationship, like \mzninline{abs(x)} in the example, or from a \gls{reif}, like \mzninline{abs(x) > y} when used in the disjunction with \mzninline{c}.
In this thesis we will follow the same naming standard as \minizinc{}, where a \gls{reif} of a constraint has the same name as the original constraint with \texttt{\_reif} appended.
\begin{example}
The importance of the use of auxiliary definitions when removing dead \variables{} and \constraints{} is demonstrated in the following example:
The importance of the use of attached \constraints{} when removing unused \variables{} and \constraints{} is demonstrated in the following \minizinc{} fragment.
\begin{mzn}
int: n;
@ -572,10 +605,10 @@ In this thesis we will follow the same naming standard as \minizinc{} where a \g
The \gls{rewriting} of this \minizinc{} model will initially create the \mzninline{n} elements for the array comprehension.
Each element is evaluated as a new \variable{} \mzninline{y} and a \constraint{} to ensure that \mzninline{y} is the multiplication of \mzninline{x} and \mzninline{i}.
Although \mzninline{n} variables are created, only the first \variable{} is constrained to be 10. All other \variables{} can thus be removed and the model will stay \gls{eqsat}.
Although \mzninline{n} variables are created, only the last \variable{} is constrained to be 10. All other \variables{} can thus be removed and the model will stay \gls{eqsat}.
In the \nanozinc{} version of this model, each of the multiplications \constraints{} will be added to the list of auxiliary \constraints{} of its corresponding \mzninline{y} \variable{}.
When, after evaluating the array access, all of those \variables{} except the first are detected to be unused, their removal triggers the removal of the subtraction \constraints{}.
In the \nanozinc{} version of this model, each of the multiplications \constraints{} will be added to the list of attached \constraints{} of its corresponding \mzninline{y} \variable{}.
When, after evaluating the array access, all of those \variables{} except the last are detected to be unused, their removal triggers the removal of the subtraction \constraints{}.
For this example the current \minizinc{} compiler, version 2.5.5, will produce a \gls{slv-mod} that contains:
@ -586,7 +619,7 @@ In this thesis we will follow the same naming standard as \minizinc{} where a \g
\end{itemize}
\noindent{}This is despite the fact that the \domain{} of the \variable{} \mzninline{x} has already been \gls{fixed} to 10\@.
The \nanozinc{} system, can correctly detect that the \mzninline{y} \variables{} and multiplication \constraints{} are not required.
The \nanozinc{} system can correctly detect that the \mzninline{y} \variables{} and multiplication \constraints{} are not required.
\end{example}
\paragraph{Implementation} The removal of unused identifiers is taken care of by garbage collection in the interpreter.
@ -594,13 +627,14 @@ Since our prototype interpreter uses reference counting, it already accurately t
\subsection{Constraint Propagation}
\Gls{propagation} is another important technique used to simplify the produced \nanozinc{}.
It allows us to tighten the \glspl{domain} of \variables{} in the \nanozinc{} and remove \constraints{} proven to hold.
This, in turn, offers another way that \variables{} can become unused.
\Gls{propagation} is the main inference technique used in \gls{cp} \solvers{}, as discussed in \cref{subsec:back-cp}.
At its core, \gls{propagation} simplifies the internal representation of the \gls{slv-mod}: it removes inconsistent values from \variable{} \domains{}, and it may be able to detect that certain \constraints{} are subsumed, which means that they can be removed safely.
Since a \nanozinc{} program is in fact quite similar to the internal representation of \gls{cp} \solver{}, we can use \gls{propagation} to simplify \nanozinc{}.
When using \gls{propagation} for \nanozinc{} simplification, we have to carefully consider its effects.
For instance, given the \constraint{} \mzninline{x > y}, with initial \domains{} \mzninline{x in 1..10, y in 1..10}, \gls{propagation} would result in the \domains{} being tightened to \mzninline{x in 2..10, y in 1..9}.
Note, however, that this may now prevent us from removing \mzninline{x} or \mzninline{y}: even if they later become unused, the tightened domains may impose a constraint on their definition.
Note, however, that this may now prevent us from removing \mzninline{x} or \mzninline{y}: even if they later become unused, the tightened \domains{} may impose a \constraint{} on their \variables{}.
When the \domain{} of a \variable{} is tighter than the bounds given by its defining expression, the \domain{} are said to be \gls{binding}.
For instance, if \mzninline{x} is defined as \mzninline{abs(z)}, then any restriction on the \domain{} of \mzninline{x} constrains the possible values of \mzninline{z} through the \mzninline{abs} function.
We therefore need to track whether the \domain{} of a \variable{} is the result of external \constraints{}, or is the consequence of its own definition.
@ -619,8 +653,9 @@ Equalities therefore present a valuable opportunity for model simplification, bu
Consider the simple case of \mzninline{x=y} where one of the \variables{}, say \mzninline{x}, was a top-level variable introduced by the modeller, and not defined as the result of a function call.
In that case, we can propagate the equality \constraint{} by replacing all occurrences of \mzninline{x} with \mzninline{y}, and remove the definition of \mzninline{x}.
The more complicated case for \mzninline{x=y} is when both \mzninline{x} and \mzninline{y} are the result of function calls, \eg\ from a \constraint{} such as \mzninline{constraint f(a)=g(b)}.
The corresponding \nanozinc{} code looks like this:
The more complicated case for \mzninline{x=y} is when both \mzninline{x} and \mzninline{y} are the result of function calls.
For example, a \constraint{} such as \mzninline{constraint f(a)=g(b)}.
Assuming functions \mzninline{f} and \mzninline{g} are directly rewritten into relational forms \mzninline{f_rel} and \mzninline{g_rel}, the corresponding \nanozinc{} code looks as follows.
\begin{nzn}
var int: x;
@ -635,8 +670,8 @@ This would trigger the removal of the corresponding definition \mzninline{f_rel(
Rather, the \interpreter{} needs to pick one of the two definitions and \emph{promote} it to top-level status.
Let us assume that the \interpreter{} decides to replace \mzninline{y} by \mzninline{x}.
\mzninline{y} is then globally replaced by \mzninline{x}, and its declaration is removed.
The \interpreter{} moves all auxiliary \constraints{} from \mzninline{y} into the list of top-level \constraints{}, and then removes the \mzninline{int_eq} \constraint{}.
The resulting \nanozinc{} looks like this:
The \interpreter{} moves all attached \constraints{} from \mzninline{y} into the list of top-level \constraints{}, and then removes the \mzninline{int_eq} \constraint{}.
The following \nanozinc{} program would be its result.
\begin{nzn}
var int: x;
@ -645,46 +680,46 @@ The resulting \nanozinc{} looks like this:
\end{nzn}
The process of equality propagation is similar to unification in logic programming \autocite{warren-1983-wam}.
However, since equations in \minizinc\ always concern scalar variables rather than terms, we can restrict ourselves to this simple substitution scheme and leave the further checking of the resulting equalities to the target \solver{}.
However, since equations in \minizinc{} always concern scalar variables rather than terms, we can restrict ourselves to this simple substitution scheme and leave the further checking of the resulting equalities to the target \solver{}.
\paragraph{Implementation}
\Gls{rewriting} a function call that has a \microzinc{} definition and \gls{rewriting} a constraint due to \gls{propagation} are very similar.
The \interpreter{} therefore simply interleaves both forms of \gls{rewriting}.
Efficient \gls{propagation} engines ``wake up'' a \gls{propagator} only when one of its \variables{} has received an update (\ie\ when its \domain{} has been shrunk).
Efficient \gls{propagation} engines ``wake up'' a \gls{propagator} only when one of its \variables{} has received an update (\ie{} when its \domain{} has been shrunk).
To enable this, the \interpreter{} needs to keep a data structure linking \variables{} to the \constraints{} where they appear (in addition to the reverse links from calls to the \variables{} in their arguments).
These links do not take part in the reference counting.
Together with its current \domain{}, each \variable{} in the interpreter also contains a Boolean flag.
This flag signifies whether the \gls{domain} of the \variable{} is an additional constraint.
This flag signifies whether the \domain{} of the \variable{} is \gls{binding}.
When the flag is set, the \variable{} cannot be removed, even when the reference count is zero.
This happens when a \constraint{} that does not define the variable changes its \gls{domain}.
This \constraint{} might thereafter be removed, if it now proven to hold, but its effects will still be enforced.
If, however, any defining \constraint{} further tightens the \gls{domain}, then its constraint is no longer constraining.
The flag can then be unset and the variable can potentially be removed.
This flag is set when the \domain{} of a \variable{} is tightened by a \constraint{} that is not attached to the \variable{}.
This \constraint{} may then become subsumed after \gls{propagation} and can then be removed.
Its meaning is now completely captured by the \domains{} of the \variables{}.
If, however, any defining \constraint{} further tightens the \domain{}, then it is is no longer \gls{binding}, because it is again fully implied by its defining \constraints{}.
The flag can then be unset and the \variable{} can potentially be removed.
\subsection{Delayed Rewriting}
\gls{propagation} might change \variables{}.
It might shrink their \domains{} or even fix them to a single value.
When this happens for the arguments of a call, a more specific \gls{decomp} might become available.
It is therefore important to evaluate calls when all possible information is available to create efficient \nanozinc{}.
\Gls{propagation} can tighten \domains{} of \variables{} or even fix them to a single value.
When this happens for the arguments of a call, a more specific \gls{decomp} may become available.
As discussed in \cref{subsec:back-delayed-rew}, it is therefore important to evaluate calls when all possible information is available to create efficient \glspl{slv-mod}.
In our \microzinc{}/\nanozinc{} system, we allow predicates and functions to be annotated as potential candidates for \gls{del-rew}.
Any annotated \constraint{} is handled by the (CallPredicate) rule rather than the (Call) rule, which means that it is simply added as a call into the \nanozinc{} code, without evaluating its body.
When \gls{propagation} reaches a fix-point, all annotations are removed from the current \nanozinc{} program, and evaluation resumes with the predicate bodies.
In our \microzinc{}/\nanozinc{} system, we allow functions to be annotated as potential candidates for \gls{del-rew}.
Any annotated \constraint{} is handled by the (CallNative) rule rather than the (Call) rule, which means that it is simply added as a call into the \nanozinc{} code, without evaluating its body.
When \gls{propagation} reaches a \gls{fixpoint}, all annotations are removed from the current \nanozinc{} program, and evaluation resumes with the function bodies.
This crucial optimisation enables rewriting in multiple \emph{phases}.
For example, a \cmodel{} targeted at a \gls{mip} \solver{} is rewritten into Boolean and reified \constraints{}, whose definitions are annotated to be delayed.
The \nanozinc{} program can then be fully simplified by \gls{propagation}, before the Boolean and reified \constraints{} are rewritten into \gls{native} linear \constraints suitable for \gls{mip}.
The \nanozinc{} program can then be fully simplified by \gls{propagation}, before the Boolean and reified \constraints{} are rewritten into \gls{native} linear \constraints{} suitable for \gls{mip}.
\subsection{Common Sub-expression Elimination}%
\label{sec:rew-cse}
\Gls{cse} is a crucial technique to avoid duplications in a \gls{model}.
As shown in \cref{subsec:back-cse}, \gls{cse} is a crucial technique to avoid duplications in a \gls{model}.
In our architecture \gls{cse} is performed on two levels.
The \microzinc{} \interpreter{} performs \gls{cse} through memorisation.
The \microzinc{} \interpreter{} performs \gls{cse} through memoisation.
It maintains a table that maps a function identifier and the call arguments to its result for each call instruction that is executed.
Before it executes a call instruction, it searches the table for an entry with identical function identifier and call arguments.
Since functions in \microzinc{} are guaranteed to be pure and total, whenever the table search succeeds, the result can be used instead of executing the call instruction.
@ -699,7 +734,7 @@ Earlier in the process, however, the \minizinc{} to \microzinc{} \compiler{} can
\end{mzn}
In this case a static \gls{compiler} analysis could detect that the same syntactical expression, \mzninline{abs(x)}, occurs twice.
Since these expressions are guaranteed to have equivalent result, this analysis could then be able to hoist into a let expression.
Since these expressions are guaranteed to have equivalent results, this analysis could then hoist the shared expression into a \gls{let}.
\begin{mzn}
constraint let { var int: y = abs(x) } in
@ -709,55 +744,81 @@ Earlier in the process, however, the \minizinc{} to \microzinc{} \compiler{} can
\end{example}
As such, the \compiler{} can enforce sharing of common sub-expressions before evaluation begins.
It is worth noting that, although the \gls{cse} approach based on memorisation would also covers the static example above, this method can potentially avoid many dynamic table look-ups.
It is worth noting that, although the \gls{cse} approach based on memorisation would also cover the static example above, this method can potentially avoid many dynamic table look-ups.
Since the static analysis is cheap, it is valuable to combine both approaches.
The static approach can be further improved by \emph{inlining} function calls, since that may expose more calls as being syntactically equal.
\paragraph{Implementation} In the implementation of our \microzinc{} \interpreter{}, \gls{cse} directly interacts with the reference counting mechanism.
It is clear that a new reference must created when an entry of the \gls{cse} is reused in \nanozinc{}, but the entries of the table themselves are also essentially references.
However, when a \variable{} is no longer referenced in the \nanozinc{}, we still expect it to be removed, even if it is still part of the \gls{cse} table.
As such, we treat \gls{cse} entries as \emph{weak} references.
They reference an object, but do not affect its liveness (\ie{} increase its reference count).
It is clear that when an expression is reused by returning it from the \gls{cse} table, this creates a new reference to that expression.
However, the entries in the \gls{cse} table should not keep the corresponding variables alive.
Otherwise, no \variable{} would ever become unused.
Therefore, we treat \gls{cse} entries as weak references.
They reference a \variable{}, but do not affect its liveness (\ie{} increase its reference count).
If an entry is found in the \gls{cse} table with a reference count of zero, it is removed from the table and its contents are not used.
The usage of a \gls{cse} table can be costly.
It requires a lot of memory and the time to find entries can be significant in the overall process.
The memory requirement and time spent finding entries can be significant in the overall process.
This is aggravated by the fact that \minizinc{} has many places where a function's body only contains a single call to a function that is not used anywhere else.
Although this structure offers flexibility when defining \minizinc{} libraries, it results in many \gls{cse} entries that differ only by their function identifier.
For example, the \mzninline{knapsack} \gls{global} is defined in the \minizinc{} standard library as follows.
\begin{mzn}
predicate knapsack(
array[int] of int: w,
array[int] of int:p,
array[int] of var int:x,
var int: W, var int: P
) =
assert(
index_set(w) = index_set(p) /\ index_set(w) = index_set(x),
"index set of weights must be equal to index set of profits and index set of items",
) /\ assert(
lb_array(w) >= 0,
"weights must be non-negative",
) /\ assert(
lb_array(p) >= 0,
"profits must be non-negative",
) /\ fzn_knapsack(w, p, x, W, P);
\end{mzn}
After checking the \parameter{} arguments, the function merely returns the result of \mzninline{fzn_knapsack}.
This function is implemented in the \solver{} library to provide the implementation of the \mzninline{knapsack} \gls{global}.
The extra function layer ensures that these checks can be performed independently of the \solver{} library and that the \solver{} can make certain assumptions about the function arguments.
But because the modeller will only use \mzninline{knapsack}, it does not make sense to also create \gls{cse} entries for \mzninline{fzn_knapsack}, as it will never be used.
Therefore, we have added an additional flag to our call instruction.
This flag controls whether the call is subject \gls{cse}.
This flag controls whether the call is subject to \gls{cse}.
This allows us to disable the \gls{cse} when it is guaranteed to be unnecessary.
\subsection{Constraint Aggregation}%
\label{subsec:rew-aggregation}
In our new system it is still possible to support \gls{aggregation}.
We aggregate \constraints{} by combining \constraints{} connected through functional definitions, eliminating the need for \glspl{ivar}.
We aggregate \constraints{} by combining \constraints{} connected through attached \constraints{}, eliminating the need for \glspl{ivar} to which they are attached.
To aggregate a certain kind of \constraint{}, it is marked as a \gls{native} \constraint{}.
These \constraints will now be kept as temporary functional definitions in the \nanozinc{} program.
These functional definitions are kept in the \nanozinc{} program until a top-level (relational) \constraint{} is posted that uses these definitions.
Once this happens, the interpreter will employ dedicated \gls{aggregation} logic to visit the functional definitions and combine their constraints.
These functional definitions are kept in the \nanozinc{} program until a top-level \constraint{} is posted that uses the \variables{} to which they are attached.
Once this happens, the interpreter will employ dedicated \gls{aggregation} logic to visit the attached \constraints{} and combine them.
The top-level \gls{constraint} is then replaced by the combined \gls{constraint}.
When the \glspl{ivar} become unused, they will be removed using the normal mechanisms.
\begin{example} For example, let us reconsider the linear constraint from \cref{ex:back-agg}: \mzninline{x + 2*y <= z}.
The constraint will result in the following \nanozinc{}:
The constraint will result in the following \nanozinc{}.
\begin{nzn}
var int: x;
var int: y;
var int: z;
var int: i1;
↳ constraint '*'(y, 2);
↳ constraint '*'(y, 2, i1);
var int: i2;
↳ constraint '+'(x, i1);
↳ constraint '+'(x, i1, i2);
constraint '<='(i2, z);
\end{nzn}
\mzninline{*} and \mzninline{+} were marked as \gls{native} \constraints{} as they can be aggregated into a linear \constraint{}.
Their functional definitions are put in place in the \nanozinc{}, and then a top-level \mzninline{<=} \constraint{} is created.
The \interpreter{} will then recursively visit the arguments of the \constraints{}.
The \constraints{} are then combined into a single linear \constraint{}:
The \constraints{} are then combined into the following linear \constraint{}.
\begin{mzn}
constraint int_lin_le([1,2,-1], [x,y,z], 0)
@ -767,23 +828,23 @@ When the \glspl{ivar} become unused, they will be removed using the normal mecha
\section{Experiments}\label{sec:rew-experiments}
We have created a prototype implementation of the architecture presented in the preceding sections.
It consists of a \compiler{} from \minizinc{} to \microzinc{}, and an incremental \microzinc{} \interpreter{} producing \nanozinc{}.
It consists of a \compiler{} from \minizinc{} to \microzinc{}, and a \microzinc{} \interpreter{} producing \nanozinc{}.
The system supports a significant subset of the full \minizinc{} language; notable features that are missing are support for set and float variables, option types, and compilation of model output expressions and annotations.
We will release our implementation under an open-source license and can make it available to the reviewers upon request.
\todo{I suppose it is time to release the prototype.}
The implementation is not optimised for performance yet, but was created as a faithful implementation of the developed concepts, in order to evaluate their suitability and provide a solid baseline for future improvements.
In the following we present experimental results on basic \gls{rewriting} performance as well as an comparison with \glspl{interpreter} of other programming languages to demonstrate the efficiency gains that are possible thanks to the new architecture.
In the following we present experimental results on basic \gls{rewriting} performance as well as a comparison with \glspl{interpreter} of other programming languages to demonstrate the efficiency gains that are possible thanks to the new architecture.
A description of the used computational environment, \minizinc{} instances, and versioned software has been included in \cref{ch:benchmarks}.
For our first experiment, we selected 17 models from the annual \minizinc\ challenge and compiled 5 instances of each model to \flatzinc{}, using the current \minizinc\ release version 2.5.5 and the new prototype system.
In both cases we use the standard \minizinc\ library of global constraints (\ie\ we decompose those constraints rather than using solver primitives, in order to stress-test the flattening).
We measured pure flattening time, \ie\ without time required to parse and type check in version 2.5.5, and without time required for compilation to \microzinc\ in the new system (compilation is usually very fast).
For our first experiment, we selected 17 models from the annual \minizinc{} challenge and compiled 5 instances of each model to \flatzinc{}, using the current \minizinc{} release version 2.5.5 and the new prototype system.
In both cases we use the standard \minizinc{} library of \glspl{global} (\ie{} we decompose those \constraints{} rather than using \solver{} \gls{native} \constraints{}, in order to stress-test the \gls{rewriting}).
We measured pure \gls{rewriting} time, \ie{} without time required to parse and type check in version 2.5.5, and without time required for compilation to \microzinc{} in the new system (compilation is usually very fast).
Times are averages of 10 runs.
\Cref{sfig:rew-compareruntime} compares the flattening time for each of the 100 instances.
\Cref{sfig:rew-compareruntime} compares the \gls{rewriting} time for each of \instances{}.
Points below the line indicate that the new system is faster.
On average, the new system achieves a speed-up of 5.5, with every \instance{} achieving at least 2.5 speedup and multiple \instances{} with a speedup of over \(100\).
On average, the new system achieves a speed-up of 5.5, with every \instance{} achieving at least 2.5 speedup and multiple \instances{} with a speedup of over 100.
In terms of memory performance (\cref{sfig:rew-comparemem}), version 2.5.5 can sometimes still outperform the new prototype.
We have identified that the main memory bottlenecks are our currently unoptimised implementations of \gls{cse} lookup tables and argument vectors.
These are very encouraging results, given that we are comparing a largely unoptimised prototype to a mature piece of software.
@ -801,8 +862,8 @@ These are very encouraging results, given that we are comparing a largely unopti
\includegraphics[width=\columnwidth]{assets/img/rew_compare_memory}
\caption{\label{sfig:rew-comparemem}Maximum resident set size (kbytes)}
\end{subfigure}
\caption{\label{fig:4-runtime}Performance on flattening MiniZinc Challenge
instances. \minizinc\ 2.5.5 (x-axis) vs new architecture (y-axis), log-log
\caption{\label{fig:4-runtime}Performance on \gls{rewriting} MiniZinc Challenge
\instances{}. \minizinc{} 2.5.5 (x-axis) vs new architecture (y-axis), log-log
plot. Dots below the line indicate the new system is better.}
\end{figure}
@ -836,18 +897,18 @@ We are convinced, however, that we can get closer to its performance given the r
% \section{Summary}%
% \label{sec:rew-summary}
% In this chapter, we introduced a systematic view of the execution of \minizinc{}, revisiting the rewriting from high-level \minizinc\ to solver-level \flatzinc{}.
% We first introduced the intermediate languages \microzinc{} and \nanozinc{} and explained how \minizinc\ can be transformed into a set of \microzinc\ definitions and a \nanozinc\ program.
% We then, crucially, discussed how to partially evaluate a \nanozinc\ program using \microzinc\ definitions and present formal definitions of the rewriting rules applied during partial evaluation.
% In this chapter, we introduced a systematic view of the execution of \minizinc{}, revisiting the rewriting from high-level \minizinc{} to solver-level \flatzinc{}.
% We first introduced the intermediate languages \microzinc{} and \nanozinc{} and explained how \minizinc{} can be transformed into a set of \microzinc{} definitions and a \nanozinc{} program.
% We then, crucially, discussed how to partially evaluate a \nanozinc{} program using \microzinc{} definitions and present formal definitions of the rewriting rules applied during partial evaluation.
% Continuously applying these rules would result in a correct solver-level model, but it is unlikely to be the best model for the solver.
% We, therefore, discuss multiple techniques to improve the solver-level constraint model during the partial evaluation of \nanozinc{}.
% First, we introduce a novel technique to eliminate all unused variables and constraints: we track all constraints that are introduced only to define a variable.
% This means we can keep an accurate count of when a variable becomes unused by counting only the references to a variable in constraints that do not help define it.
% Then, we discuss the use of \gls{propagation} during the partial evaluation of the \nanozinc\ program.
% Then, we discuss the use of \gls{propagation} during the partial evaluation of the \nanozinc{} program.
% This technique can help shrink the domains of the decision variable or even combine variables known to be equal.
% When a redefinition of a constraint requires the introspection into the current domain of a variable, it is often important to have the tightest possible domain.
% Hence, we discuss how in choosing the next \nanozinc\ constraint to rewrite, the interpreter can sometimes delay the rewriting of certain constraints to ensure the most amount of information is available.
% Hence, we discuss how in choosing the next \nanozinc{} constraint to rewrite, the interpreter can sometimes delay the rewriting of certain constraints to ensure the most amount of information is available.
% \Gls{cse}, our next optimisation technique, ensures that we do not create or evaluate the same constraint or function twice and reuse variables where possible.
% Finally, the last optimisation technique we discuss is the use of \gls{aggregation}.
% The use of \gls{aggregation} ensures that individual functional constraints can be collected and combined into an aggregated form.
@ -855,5 +916,5 @@ We are convinced, however, that we can get closer to its performance given the r
% This optimisation is very important for \gls{mip} solvers.
% Finally, we test the described system using an experimental implementation.
% We compare this experimental implementation against the current \minizinc\ interpreter, version 2.5.3, and look at both runtime and its memory usage.
% Although the experimental implementation there are instances where the experimental implementation uses more memory than the current \minizinc\ interpreter, it clearly outperforms the current \minizinc\ interpreter in terms of time.
% We compare this experimental implementation against the current \minizinc{} interpreter, version 2.5.3, and look at both runtime and its memory usage.
% Although the experimental implementation there are instances where the experimental implementation uses more memory than the current \minizinc{} interpreter, it clearly outperforms the current \minizinc{} interpreter in terms of time.

6
chapters/3_rewriting_preamble.tex
View File

@ -1,6 +1,4 @@
\noindent{}\todo{This probably needs a ``why?''}
In this chapter, we revisit the \gls{rewriting} of \minizinc{} into \glspl{slv-mod}.
\noindent{}In this chapter, we develop a new architecture for \gls{rewriting} \minizinc{} into \glspl{slv-mod}.
We describe a new \textbf{systematic view of the execution of \minizinc{}} and build on this to propose a new tool chain.
We show how this tool chain allows us to:
@ -14,6 +12,8 @@ We show how this tool chain allows us to:
\end{itemize}
\noindent{}In addition to providing the first formalisation and systematic description of rewriting MiniZinc, we will see that the resulting architecture is also significantly more efficient and flexible than the current \minizinc{} system.
This chapter is organised as follows.
\Cref{sec:rew-arch} provides an quick overview of the proposed architecture.
\Cref{sec:rew-micronano} introduces the core of our \gls{rewriting} system using the \microzinc{} and \nanozinc{} languages. These new languages provide a new intermediate representation that enables more efficient \gls{rewriting}.

19
chapters/4_half_reif.tex
View File

@ -66,7 +66,7 @@ The flattener then enforces a \constraint{} \mzninline{pred_reif(...,b)}, which
\end{enumerate}
In contrast, the authors introduce \gls{half-reif}.
\gls{half-reif} follows from the idea that in many cases it might be sufficient to use the logical implication of an expression, \mzninline{b -> pred(...)}, instead of the logical equivalence, \mzninline{b <-> pred(...)}.
\gls{half-reif} 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(...)}.
Flattening with \gls{half-reif} is an approach that improves upon all these weaknesses of flattening with \emph{full} reification:
\begin{enumerate}
@ -574,7 +574,7 @@ It is, however, not always safe to do so.
It is, therefore, not safe to assume that all sides of the if-then-else expressions are evaluated in \rootc{} context.
\end{example}
Using the \changepos{} transformation for sub-expression contexts is safe, but it might place a large burden on the \solver{}.
Using the \changepos{} transformation for sub-expression contexts is safe, but it places a large burden on the \solver{}.
The solver is likely to perform better when the direct constraint predicate is used.
To detect situation where the sub-expression are only used in an array access or if-then-else expression we introduce the \mayberootc{} context.
@ -629,13 +629,13 @@ During the flattening process the contexts assigned to the different expressions
\todo{Replace the previous example. It was too long and complex.}
\end{example}
A consequence of the use of \gls{half-reif}, shown in the example, is that it might form so called \emph{implication chains}.
A consequence of the use of \gls{half-reif}, shown in the example, is that it forms so called \emph{implication chains}.
This happens when the right hand side of an implication is half reifed and a new Boolean variable is created to represent the variable.
Instead, we could have directly posted the half-reified constraint using the left hand side of the implication as its control variable.
In \cref{subsec:half-compress} we present a new post-processing method, \emph{chain compression}, that can be used to eliminate these implication chains.
The flattening with \gls{half-reif} also interacts with some of the optimisation methods used during the flattening process.
Most importantly, \gls{half-reif} has to be considered when using \gls{cse} and \gls{propagation} might change the context of expression.
Most importantly, \gls{half-reif} has to be considered when using \gls{cse} and \gls{propagation} can change the context of expression.
In \cref{subsec:half-cse} we will discuss how \gls{cse} can be adjusted to handle \gls{half-reif}.
Finally, in \cref{subsec:half-dyn-context} we will discuss how the context in which a expression is executed can be adjusted during the flattening process.
@ -761,7 +761,7 @@ Clearly, a \constraint{} and its negation cannot both hold at the same time.
\subsection{Dynamic Context Switching}%
\label{subsec:half-dyn-context}
In \cref{subsec:half-?root} we discussed the fact that the correct context of an expression might not be known when analysing a \microzinc{} model.
In \cref{subsec:half-?root} we discussed the fact that the correct context of an expression is not always known when analysing a \microzinc{} model.
Its context depends on data that is only known at an instance level.
The same situation can be caused by \gls{propagation}.
@ -979,7 +979,8 @@ Since there are many more constraints, the introduced optimisation mechanisms ha
Finally, statistics for the flattening the instances is shown in \cref{subtab:half-flat-bool}.
Like linearisation, the usage of \gls{half-reif} significantly reduces number of constraints and \glspl{reif}.
Different, however, is that the booleanisation library is explicitly defined in terms of \glspl{half-reif}.Some constraints might manually introduce \mzninline{_imp} call as part of their definition.
Different, however, is that the booleanisation library is explicitly defined in terms of \glspl{half-reif}.
Some \constraints{} manually introduce \mzninline{_imp} call as part of their definition.
Furthermore, the usage of 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 chain compression are instead aggregated into bigger clauses.
Surprisingly, the usage of \gls{half-reif} also reduces the flattening time as it reduces the workload.
@ -1006,7 +1007,7 @@ For \gls{gecode}, the usage of \gls{half-reif} does not seem to impact its solvi
Although we would have hoped that propagators for \glspl{half-reif} would be more efficient and reduce the number of propagators scheduled in general.
Neither number of instances solved, nor the solving time required improved.
A single instance, however, is negatively impacted by the change; an optimal solution for this instance is no longer found.
We expect that this instance might have benefited from the increased Boolean propagation that is caused by full \gls{reif}.
We expect that this \instance{} has benefited from the increased Boolean propagation that is caused by full \gls{reif}.
Overall, these results do not show any significant positive or negative effects in \gls{gecode}'s performance when using \gls{half-reif}.
When using \gls{cplex} the usage of \gls{half-reif} is clearly a positive one.
@ -1015,9 +1016,9 @@ The same linearised instances when using the \gls{cbc} solver seem to have the o
Even though it reduces the time required to prove that two instances are unsatisfiable, it can no longer find six optimal solutions.
These results are hard to explain.
In general, we would expect the reduction of constraints in a \gls{mip} instance would help the \gls{mip} solver.
However, we can imagine that the removed constraints might in some cases help the \gls{mip} solver.
However, we can imagine that the removed constraints in some cases help the \gls{mip} solver.
An important technique used by \gls{mip} solvers is to detect certain pattern, such as cliques, during the pre-processing of the \gls{mip} instance.
Some patterns might only be detected when using a full \gls{reif}.
Some patterns can only be detected when using a full \gls{reif}.
Furthermore, the performance of \gls{mip} solvers is often dependent on the order and form in which the constraints are given.
\todo{Is there a citation for this?} With the usage of the \gls{aggregation} and \gls{del-rew}, these can be exceedingly different when using \gls{half-reif}.

4
chapters/5_incremental.tex
View File

@ -21,7 +21,7 @@ This extension is based on the construct introduced in \minisearch\ \autocite{re
A meta-search in \minisearch\ typically solves a given \minizinc\ model, performs some calculations on the solution, adds new constraints and then solves again.
Most \gls{meta-search} definitions in \minisearch\ consist of two parts.
The first part is a declarative definition of any restriction to the search space that the \gls{meta-search} algorithm might apply, called a \gls{neighbourhood}.
The first part is a declarative definition of any restriction to the search space that the \gls{meta-search} algorithm can apply, called a \gls{neighbourhood}.
In \minisearch\ these definitions can make use of the function: \mzninline{function int: sol(var int: x)}, which returns the value that variable \mzninline{x} was assigned to in the previous solution (similar functions are defined for Boolean, float and set variables).
This allows the \gls{neighbourhood} to be defined in terms of the previous solution.
In addition, a neighbourhood predicate will typically make use of the random number generators available in the \minizinc\ standard library.
@ -233,7 +233,7 @@ If we are not in the first run for a stage we add the branch and bound cut to tr
Finally, we set the objective to be the objective for the current stage.
There is not always a clear order of importance for different objectives in a problem.
In these cases we might instead look for a number of diverse solutions and allow the user to pick the most acceptable options.
In these cases we instead look for a number of diverse solutions and allow the user to pick the most acceptable options.
The following fragment shows a \gls{meta-search} for the Pareto optimality of a pair of objectives:
\begin{mzn}

2
chapters/5_incremental_preamble.tex
View File

@ -17,7 +17,7 @@ Examples of these methods are:
Here we aim to provide a set of solutions that are sufficiently different from each other in order to give human decision makers an overview of the solution space.
Diversity can be achieved by repeatedly solving a problem instance with different objectives.
\item Interactive Optimisation \autocite{belin-2014-interactive}.
In some scenarios it might be useful to allow a user to directly provide feedback on solutions found by the solver.
In some scenarios it can be useful to allow a user to directly provide feedback on solutions found by the solver.
The feedback in the form of constraint are added back into the problem, and a new solution is generated.
Users may also take back some earlier feedback and explore different aspects of the problem to arrive at the best solution that suits their needs.
\end{itemize}

14
chapters/6_conclusions.tex
View File

@ -55,7 +55,7 @@ This framework enables many avenues of further research.
For one, the formal rewriting rules presented open up possibilities to more extended formal reasoning about \cmls{}.
This could potentially lead to the ability to proof certain properties of the rewriting process.
Additionally, the framework introduces reasoning about the transition from \minizinc{} to \solver{} specification as two different levels: the transition from \minizinc{} to \microzinc{} and the evaluation of the \microzinc{} to create a \solver{} specification.
In our prototype we have presented techniques to help improve the quality of the \solver{} specification, but many improvements to these techniques and other techniques might be beneficial.
In our prototype we have presented techniques to help improve the quality of the \solver{} specification, but many improvements to these techniques and other techniques may be beneficial.
Finally, we use our language \nanozinc{} to track \constraints{} that are introduced to define a \variable{}.
Although we have showed how this helps when a \variable{} becomes unused, we have yet to discover its uses within the \solvers{} themselves.
In \gls{cp} \solvers, for example, it is no longer has to required propagate these defining \constraints{} once their \variable{} has been fixed (under certain circumstances).
@ -73,7 +73,7 @@ We noted that the usage of \gls{half-reif} interacts with some of the existing o
Foremost, \gls{cse} can no longer always reuse the same results for identical \constraint{}, it must now consider the context of the \constraint{}.
For \constraints{} were \gls{cse} is triggered in multiple context, we propose rules to either use the result that is acceptable in both contexts, or create such a result.
Using this adjustment we ensure that identical \constraints{} still have a single result.
The usage of \constraint{} \gls{propagation} might change the context of a \constraint{} during the rewriting process.
The usage of \gls{propagation} can change the context of a \constraint{} during the rewriting process.
We described how we can communicate this change through the control variables of (half-)\glspl{reif}.
Lastly, the introduction of a \gls{half-reif} on the right hand side of an logical implication essentially introduce layered implications.
In this case, the created control variable forms an extra barrier in during propagation where the left hand side of the implication could have been used directly.
@ -112,25 +112,25 @@ In our experiments, we have shown that his method is highly effective.
Even compared to an ``oracle'' approach, where the changes are merely read and not computed, this approach only slightly underperforms.
Meanwhile, the time required to compile the meta-search description is negligible.
It might not always be possible to extend a \solver{}, for these cases we have defined a second method.
It is not always possible to extend a \solver{}, for these cases we have defined a second method.
This method significantly reduces the overhead of rewriting models that incrementally changes.
In particular we defined an interface for \cmls{}.
A modeller can repeatedly add \constraints{} and \variables{} to the model and, crucially, the additions to the model can retracted in reverse order through the use of trailing.
Each of these changes to the \constraint{} model is incrementally applied to the \solver{} specification.
Since multiple generations of meta-optimisation share large parts of their \constraint{} model, this significantly reduces the amount work required in the rewriting process.
As an additional improvement, the changes observed in the \solver{} specification might also be incrementally applied within the \solver{}.
As an additional improvement, the changes observed in the \solver{} specification can be incrementally applied within the \solver{}.
Ideally, the solver can fully support the incremental changes made to the specification.
This avoids the overhead of re-initialisation and allows the solver to retain all search information.
Otherwise, the solver might still be warm-started.
Otherwise, the solver can still be warm-started.
Instead of starting the search without any information, the \solver{} is given information about the previous solution to speed up it search.
Although our experiments show that this method is not as effective as the initial method.
It is still a significant improvement over the recompilation approach.
The improvements offered by these new method might spark future research.
The improvements offered by these new method may spark future research.
Primarily, it will allow and promote the usage of meta-optimisation methods in \cmls{} for new problems.
New meta-optimisation techniques might require extensions of the methods presented.
New meta-optimisation techniques could require extensions of the methods presented.
It would even be possible to revisit existing research that uses the combination of \cmls{} and meta-optimisation to study improvements that these methods offer.
\paragraph{Summary} In conclusion, this thesis presented an architecture for the rewriting of high-level \cmls{}.