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

Grammar check of the Background

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-24 13:44:15 +10:00
parent e25e0d46c4
commit 6cc7e377b3
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
2 changed files with 71 additions and 72 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

137
chapters/2_background.tex
View File

@ -17,24 +17,24 @@ Consequently, in current times, writing a computer program requires little knowl
\textcite{freuder-1997-holygrail} states that the ``Holy Grail'' of programming languages would be where the user merely states the problem, and the computer solves it, and that \constraint{} modelling is one of the biggest steps towards this goal to this day. \textcite{freuder-1997-holygrail} states that the ``Holy Grail'' of programming languages would be where the user merely states the problem, and the computer solves it, and that \constraint{} modelling is one of the biggest steps towards this goal to this day.
\Cmls{} operate differently from other computer languages. \Cmls{} operate differently from other computer languages.
The modeller does not describe how to solve a problem, but rather formalises the requirements of the problem. The modeller does not describe how to solve a problem, but rather formalizes the requirements of the problem.
It could be said that a \cmodel{} actually describes the answer to the problem. It could be said that a \cmodel{} actually describes the answer to the problem.
In a \cmodel{}, instead of specifying the manner in which we find a \gls{sol}, we give a concise description of the problem. In a \cmodel{}, instead of specifying the manner in which we find a \gls{sol}, we give a concise description of the problem.
The elements of a \cmodel{} include \prbpars{}, what we already know; \variables{}, what we wish to know; and \constraints{}, the relations that should exist between them. The elements of a \cmodel{} include \prbpars{}, what we already know; \variables{}, what we wish to know; and \constraints{}, the relations that should exist between them.
Through the variation of \prbpars{}, a \cmodel{} describes a full class of problems. Through the variation of \prbpars{}, a \cmodel{} describes a full class of problems.
A specific problem is captured by an \instance{}, the combination of a \cmodel{} with a complete \gls{parameter-assignment} (\ie{} a mapping from all \prbpars{} to values). A specific problem is captured by an \instance{}, the combination of a \cmodel{} with a complete \gls{parameter-assignment} (\ie{} a mapping from all \prbpars{} to a value).
The type of problem described by a \cmodel{} is called a \gls{dec-prb}. The type of problem described by a \cmodel{} is called a \gls{dec-prb}.
The goal of a \gls{dec-prb} is to find a \gls{sol}: a complete \gls{variable-assignment} that satisfies the \constraints{}. The goal of a \gls{dec-prb} is to find a \gls{sol}: a complete \gls{variable-assignment} that satisfies the \constraints{}.
Or, when this is not possible, prove that no such \gls{assignment} exists. Or, when this is not possible, prove that no such \gls{assignment} exists.
Many \cmls{} also support the modelling of \glspl{opt-prb}, where a \gls{dec-prb} is augmented with an \gls{objective}. Many \cmls{} also support the modelling of \glspl{opt-prb}, where a \gls{dec-prb} is augmented with an \gls{objective}.
In this case the goal is to find a \gls{sol} that satisfies all \constraints{} while minimising (or maximising) the value of the \gls{objective}. In this case the goal is to find a \gls{sol} that satisfies all \constraints{} while minimizing (or maximizing) the value of the \gls{objective}.
Although a \cmodel{} does not contain any instructions on how to find a suitable \gls{sol}, \instances{} of \cmodels{} can generally be given to a dedicated \solver{}. Although a \cmodel{} does not contain any instructions on how to find a suitable \gls{sol}, \instances{} of \cmodels{} can generally be given to a dedicated \solver{}.
To solve these \instances{}, however, they can go through a \gls{rewriting} process to arrive at a \gls{slv-mod}, 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{}. The \solver{} then uses a dedicated algorithm that finds a \gls{sol} that fits the requirements of the \instance{}.
This process is visualised in \cref{fig:back-cml-flow}. This process is visualized in \cref{fig:back-cml-flow}.
\begin{figure} \begin{figure}
\centering \centering
@ -48,10 +48,10 @@ This process is visualised in \cref{fig:back-cml-flow}.
As an example, let us consider the following scenario: Packing for a weekend trip, I have to decide which toys to bring for my dog, Audrey. As an example, let us consider the following scenario: Packing for a weekend trip, I have to decide which toys to bring for my dog, Audrey.
We only have a small amount of space left in the car, so we cannot bring all the toys. We only have a small amount of space left in the car, so we cannot bring all the toys.
Since Audrey enjoys playing with some toys more than others, we try and pick the toys that bring Audrey the most amount of joy, but still fit in the car. Since Audrey enjoys playing with some toys more than others, we try and pick the toys that bring Audrey the most amount of joy, but still fit in the car.
The following set of equations describes this knapsack problem as an \gls{opt-prb}: The following set of equations describes this ``knapsack'' problem as an \gls{opt-prb}:
\begin{equation*} \begin{equation*}
\text{maximise}~z~\text{subject to}~ \text{maximize}~z~\text{subject to}~
\begin{cases} \begin{cases}
S \subseteq T \\ S \subseteq T \\
z = \sum_{i \in S} joy(i) \\ z = \sum_{i \in S} joy(i) \\
@ -63,7 +63,7 @@ This process is visualised in \cref{fig:back-cml-flow}.
It represents the selection of toys to be packed for the trip. It represents the selection of toys to be packed for the trip.
The \gls{objective} evaluates the quality of the \gls{sol} through the \variable{} \(z\). The \gls{objective} evaluates the quality of the \gls{sol} through the \variable{} \(z\).
And, \(z\) is bound to the amount of joy that the selection of toys will bring. And, \(z\) is bound to the amount of joy that the selection of toys will bring.
This is to be maximised. This is to be maximized.
The \prbpars{} \(T\) is the set of all available toys. The \prbpars{} \(T\) is the set of all available toys.
The \(joy\) and \(space\) functions are \prbpars{} used to map toys, \( t \in T\), to a numeric value describing the amount of enjoyment and space required respectively. The \(joy\) and \(space\) functions are \prbpars{} used to map toys, \( t \in T\), to a numeric value describing the amount of enjoyment and space required respectively.
Finally, the \prbpar{} \(C\) gives the numeric value of the total space that is left in the car before packing the toys. Finally, the \prbpar{} \(C\) gives the numeric value of the total space that is left in the car before packing the toys.
@ -97,7 +97,7 @@ Its expressive language and extensive library of \glspl{global} allow users to e
We also declare the \variable{} \mzninline{total_joy}, on \lref{line:back:knap:tj}, which is functionally defined to be the summation of all the joy for the toy picked in our selection. We also declare the \variable{} \mzninline{total_joy}, on \lref{line:back:knap:tj}, which is functionally defined to be the summation of all the joy for the toy picked in our selection.
The model then contains a \constraint{}, on \lref{line:back:knap:con}, which ensures we do not exceed the given capacity. The model then contains a \constraint{}, on \lref{line:back:knap:con}, which ensures we do not exceed the given capacity.
Finally, it states the goal for the \solver{}: to maximise the value of the \variable{} \mzninline{total_joy}. Finally, it states the goal for the \solver{}: to maximize the value of the \variable{} \mzninline{total_joy}.
\end{example} \end{example}
\begin{listing} \begin{listing}
@ -140,7 +140,7 @@ It is the primary way in which \minizinc{} communicates with \solvers{}.
Their names are no longer present in the \gls{slv-mod}. Their names are no longer present in the \gls{slv-mod}.
This \gls{slv-mod} is then passed to the targeted \solver{}. This \gls{slv-mod} is then passed to the targeted \solver{}.
The \solver{} attempts to determine a complete \gls{variable-assignment} and maximise the \gls{assignment} of the \mzninline{total_joy} \variable{}. The \solver{} attempts to determine a complete \gls{variable-assignment} and maximize the \gls{assignment} of the \mzninline{total_joy} \variable{}.
If there is no such \gls{assignment}, then it reports that the \gls{slv-mod} is \gls{unsat}. If there is no such \gls{assignment}, then it reports that the \gls{slv-mod} is \gls{unsat}.
\end{example} \end{example}
\begin{listing} \begin{listing}
@ -226,8 +226,8 @@ This item signals the \solver{} to perform one of three actions:
\begin{description} \begin{description}
\item[\mzninline{solve satisfy}] to find an \gls{assignment} to the \variables{} that satisfies the \constraints{}, \item[\mzninline{solve satisfy}] to find an \gls{assignment} to the \variables{} that satisfies the \constraints{},
\item[\mzninline{solve minimize @\(E\)@}] to find an \gls{assignment} to the \variables{} that satisfies the \constraints{} and minimises the value of the expression \(E\), or \item[\mzninline{solve minimize @\(E\)@}] to find an \gls{assignment} to the \variables{} that satisfies the \constraints{} and minimizes the value of the expression \(E\), or
\item[\mzninline{solve maximize @\(E\)@}] to similarly maximise the value of the expression \(E\). \item[\mzninline{solve maximize @\(E\)@}] to similarly maximize the value of the expression \(E\).
\end{description} \end{description}
\noindent{}The first type of goal indicates that the problem is a \gls{dec-prb}. \noindent{}The first type of goal indicates that the problem is a \gls{dec-prb}.
@ -235,7 +235,7 @@ The other two types of goals are used when the model describes an \gls{opt-prb}.
If the model does not contain a goal item, then the problem is assumed to be a \gls{dec-prb}. If the model does not contain a goal item, then the problem is assumed to be a \gls{dec-prb}.
\paragraph{Function Items} Common structures in \minizinc\ are captured using function declarations. \paragraph{Function Items} Common structures in \minizinc\ are captured using function declarations.
A functions is declared using the syntax \mzninline{function @\(T\)@: @\(I\)@(@\(P\)@) = @\(E\)@}, where: A function is declared using the syntax \mzninline{function @\(T\)@: @\(I\)@(@\(P\)@) = @\(E\)@}, where:
\begin{itemize} \begin{itemize}
\item \(T\) is the type of its result; \item \(T\) is the type of its result;
\item \(I\) is its identifier; \item \(I\) is its identifier;
@ -300,7 +300,7 @@ Note that using this \gls{global} as follows would have simplified the \minizinc
\end{mzn} \end{mzn}
\noindent{}This has the additional benefit that the knapsack structure of the problem is then known. \noindent{}This has the additional benefit that the knapsack structure of the problem is then known.
The \constraint{} can be rewritten using a specialised \gls{decomp} provided by the \solver{} or it can be marked as a \gls{native} \constraint{}. The \constraint{} can be rewritten using a specialized \gls{decomp} provided by the \solver{}, or it can be marked as a \gls{native} \constraint{}.
Although \minizinc{} contains an extensive library of \glspl{global}, many problems contain structures that are not covered by a \gls{global}. 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{}. There are many other types of expressions in \minizinc{} that help modellers express complex \constraints{}.
@ -346,7 +346,7 @@ A special \mzninline{if_then_else} \glspl{global} is available to implement this
The expression \mzninline{a[i]} selects the element with index \mzninline{i} from the \gls{array} \mzninline{a}. The expression \mzninline{a[i]} selects the element with index \mzninline{i} from the \gls{array} \mzninline{a}.
Note this is not necessarily the \(\mzninline{i}^{\text{th}}\) element because \minizinc{} allows modellers to provide a custom index set. Note this is not necessarily the \(\mzninline{i}^{\text{th}}\) element because \minizinc{} allows modellers to provide a custom index set.
The selection of an element from an \gls{array} is in many way similar to the choice in a \gls{conditional} expression. The selection of an element from an \gls{array} is in many ways similar to the choice in a \gls{conditional} expression.
Like a \gls{conditional} expression, the selector \mzninline{i} can be both a \parameter{} or a \variable{}. Like a \gls{conditional} expression, the selector \mzninline{i} can be both a \parameter{} or a \variable{}.
If the expression is a \gls{variable}, then the expression is rewritten to an \gls{avar} and an \mzninline{element} \constraint{}. If the expression is a \gls{variable}, then the expression is rewritten to an \gls{avar} and an \mzninline{element} \constraint{}.
Otherwise, the \gls{rewriting} replaces the \gls{array} access expression by the chosen element of the \gls{array}. Otherwise, the \gls{rewriting} replaces the \gls{array} access expression by the chosen element of the \gls{array}.
@ -428,7 +428,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}. 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}.
The sub-expressions of a complex expressions are often rewritten into \glspl{avar}. The sub-expressions of a complex expressions are often rewritten into \glspl{avar}.
If the sub-expression, and therefore \gls{avar}, is of Boolean type, then it needs to be rewritten into a \gls{reified} \constraint{}. If the sub-expression, and therefore \gls{avar}, is of Boolean type, then it needs to be rewritten into a \gls{reified} \constraint{}.
The \gls{reif} of a \constraint{} \(c\) creates an Boolean \gls{avar} \mzninline{b}, also referred to as its \gls{cvar}, constrained to be the truth-value of this \constraint{}: \(\texttt{b} \leftrightarrow{} c\). The \gls{reif} of a \constraint{} \(c\) creates a Boolean \gls{avar} \mzninline{b}, also referred to as its \gls{cvar}, constrained to be the truth-value of this \constraint{}: \(\texttt{b} \leftrightarrow{} c\).
\begin{example} \begin{example}
Consider the following \minizinc{} model. Consider the following \minizinc{} model.
@ -439,12 +439,12 @@ The \gls{reif} of a \constraint{} \(c\) creates an Boolean \gls{avar} \mzninline
solve maximize sum(i in 1..10) (x[i] mod 2 == 0); solve maximize sum(i in 1..10) (x[i] mod 2 == 0);
\end{mzn} \end{mzn}
This model maximises the number of even numbers taken by the elements of the \gls{array} \mzninline{x}. This model maximizes the number of even numbers taken by the elements of the \gls{array} \mzninline{x}.
In this model the expression \mzninline{x[i] mod 2 == 0} has to be \gls{reified}. In this model the expression \mzninline{x[i] mod 2 == 0} has to be \gls{reified}.
This means that for each \mzninline{i}, a \gls{cvar} \mzninline{b_i} is added, together with a constraint that makes \mzninline{b_i} true if-and-only-if \mzninline{x[i] mod 2 = 0}. This means that for each \mzninline{i}, a \gls{cvar} \mzninline{b_i} is added, together with a constraint that makes \mzninline{b_i} true if-and-only-if \mzninline{x[i] mod 2 = 0}.
We can then add up the values of all these \mzninline{b_i}, as required by the maximisation. We can then add up the values of all these \mzninline{b_i}, as required by the maximization.
Since the elements have a domain from 1 to 15 and are constrained to take different values, not all elements of \mzninline{x} can take even values. Since the elements have a domain from 1 to 15 and are constrained to take different values, not all elements of \mzninline{x} can take even values.
Instead, the solver is tasked to maximise the number of reified variables it sets to \mzninline{true}. Instead, the solver is tasked to maximize the number of reified variables it sets to \mzninline{true}.
\end{example} \end{example}
When an expression occurs in a position where it can be directly enforced, we say it occurs in \rootc{} context. When an expression occurs in a position where it can be directly enforced, we say it occurs in \rootc{} context.
@ -456,7 +456,7 @@ In \minizinc{}, almost all expressions can be used in both \rootc{} and non-\roo
In this subsection we discuss the handling of partial functions in \cmls{} as studied by \textcite{frisch-2009-undefinedness}. In this subsection we discuss the handling of partial functions in \cmls{} as studied by \textcite{frisch-2009-undefinedness}.
When an function has a well-defined result for all its possible inputs it is said to be total. When a function has a well-defined result for all its possible inputs it is said to be total.
Some expression in \cmls{}, however, are rewritten into functions that do not have well-defined results for all possible inputs. Some expression in \cmls{}, however, are rewritten into functions that do not have well-defined results for all possible inputs.
Part of the semantics of a \cml{} is the choice as to how to treat these partial functions. Part of the semantics of a \cml{} is the choice as to how to treat these partial functions.
@ -469,7 +469,7 @@ Part of the semantics of a \cml{} is the choice as to how to treat these partial
\noindent{}It requires that if \mzninline{i} takes a value less or equal to four, then the value in the \texttt{i}\(^{th}\) position of \gls{array} \mzninline{a} multiplied by \mzninline{x} must be at least six. \noindent{}It requires that if \mzninline{i} takes a value less or equal to four, then the value in the \texttt{i}\(^{th}\) position of \gls{array} \mzninline{a} multiplied by \mzninline{x} must be at least six.
Suppose the \gls{array} \texttt{a} has index set \mzninline{1..5}, but \texttt{i} takes the value seven. Suppose the \gls{array} \texttt{a} has index set \mzninline{1..5}, but \mzninline{i} takes the value seven.
This means the expression \mzninline{a[i]} undefined. This means the expression \mzninline{a[i]} undefined.
If \minizinc{} did not implement any special handling for partial functions, then the whole expression would have to be marked as undefined and no \gls{sol} is found. If \minizinc{} did not implement any special handling for partial functions, then the whole expression would have to be marked as undefined and no \gls{sol} is found.
However, intuitively if \mzninline{i = 7} the \constraint{} should be trivially true. However, intuitively if \mzninline{i = 7} the \constraint{} should be trivially true.
@ -530,8 +530,8 @@ This is why \minizinc{} uses \glspl{rel-sem} during its evaluation.
If we, for example, reconsider the \constraint{} from \cref{ex:back-undef}, we will find that \glspl{rel-sem} will correspond to the intuitive expectation. If we, for example, reconsider the \constraint{} from \cref{ex:back-undef}, we will find that \glspl{rel-sem} will correspond to the intuitive expectation.
When \mzninline{i} takes the value seven, the expression \mzninline{a[i]} is undefined. When \mzninline{i} takes the value seven, the expression \mzninline{a[i]} is undefined.
Its closest Boolean context will take the value false. Its closest Boolean context will take the value false.
In this case, that means the right hand side of the implication becomes false. In this case, that means the right-hand side of the implication becomes false.
However, since the left hand side of the implication is also false, the \constraint{} is \gls{satisfied}. However, since the left-hand side of the implication is also false, the \constraint{} is \gls{satisfied}.
\textcite{frisch-2009-undefinedness} also show that different \solvers{} often employ different semantics. \textcite{frisch-2009-undefinedness} also show that different \solvers{} often employ different semantics.
\minizinc{} therefore implements the \glspl{rel-sem} by translating any potentially undefined expression into an expression that is always defined, by introducing appropriate \glspl{avar} and \gls{reified} \constraints{}. \minizinc{} therefore implements the \glspl{rel-sem} by translating any potentially undefined expression into an expression that is always defined, by introducing appropriate \glspl{avar} and \gls{reified} \constraints{}.
@ -607,7 +607,7 @@ 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. 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 implementations for the same \glspl{propagator}. Similarly, \solvers{} do not all have implementations for the same \glspl{propagator}.
Therefore, a \gls{slv-mod} for one \solver{} looks 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{}. \Cmls{}, like \minizinc{}, serve as a standardized form of input for these \solvers{}.
They allow modellers to always use \glspl{global} and depending on the \solver{} they are either used directly, or they are automatically rewritten using a \gls{decomp}. They allow modellers to always use \glspl{global} and depending on the \solver{} they are either used directly, or they are automatically rewritten using a \gls{decomp}.
\begin{example}% \begin{example}%
@ -637,7 +637,7 @@ They allow modellers to always use \glspl{global} and depending on the \solver{}
When solving the problem, initially no values can be eliminated from the \glspl{domain} of the \variables{}. When solving the problem, initially no values can be eliminated from the \glspl{domain} of the \variables{}.
The first propagation happens when the first queen is placed on the board, the first search decision. The first propagation happens when the first queen is placed on the board, the first search decision.
\Cref{fig:back-nqueens} visualises the \gls{propagation} after placing a queen on the d3 square of an eight by eight chessboard. \Cref{fig:back-nqueens} visualizes the \gls{propagation} after placing a queen on the d3 square of an eight by eight chessboard.
When the queen it placed on the board in \cref{sfig:back-nqueens-1}, it fixes the value of column 4 (d) to the value 3. This implicitly eliminates any possibility of placing another queen in the column. When the queen it placed on the board in \cref{sfig:back-nqueens-1}, it fixes the value of column 4 (d) to the value 3. This implicitly eliminates any possibility of placing another queen in the column.
Fixing the \domain{} of the column triggers the \glspl{propagator} of the \mzninline{all_different} \constraints{}. Fixing the \domain{} of the column triggers the \glspl{propagator} of the \mzninline{all_different} \constraints{}.
As shown in \cref{sfig:back-nqueens-2}, the first \mzninline{all_different} \constraint{} now stops other queens from being placed in the same column. As shown in \cref{sfig:back-nqueens-2}, the first \mzninline{all_different} \constraint{} now stops other queens from being placed in the same column.
@ -676,10 +676,10 @@ They allow modellers to always use \glspl{global} and depending on the \solver{}
In \gls{cp} solving there is a trade-off between the amount of time spent propagating a \constraint{} and the amount of search that is otherwise required. In \gls{cp} solving there is a trade-off between the amount of time spent propagating a \constraint{} and the amount of search that is otherwise required.
The gold standard for a \gls{propagator} is to be \gls{domain-con}. The gold 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{}. A \gls{domain-con} \gls{propagator} leaves only the values in a \domain{} for which there is least one possible \gls{variable-assignment} that satisfies its \constraint{}.
Designing such a \gls{propagator} is, however, not an easy task. Designing such a \gls{propagator} is, however, not an easy task.
The algorithm can 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. Instead, it is sometimes better to use a propagator with a lower level of consistency.
Although it does not eliminate all possible values of the domain, searching the values that are not eliminated may take less time than achieving domain consistency. Although it does not eliminate all possible values of the domain, searching the values that are not eliminated may take less time than achieving domain consistency.
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{}. 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{}.
@ -707,15 +707,15 @@ It is an \gls{opt-sol}.
Mathematical programming \solvers{} are the most prominent solving technique employed in \gls{or} \autocite{schrijver-1998-mip}. Mathematical programming \solvers{} are the most prominent solving technique employed in \gls{or} \autocite{schrijver-1998-mip}.
At its foundation lies \gls{lp}. At its foundation lies \gls{lp}.
A linear program describes a problem using \constraints{} in the form of linear (in-)equations over continuous \variables{}. A linear program describes a problem using \constraints{} in the form of linear (in-)equations over continuous \variables{}.
In general, a linear program can be expressed in the form: In general, a linear program can be expressed in the following form.
\begin{align*} \begin{align*}
\text{maximise} \hspace{2em} & \sum_{j=1}^{V} c_{j} x_{j} & \\ \text{maximize} \hspace{2em} & \sum_{j=1}^{V} c_{j} x_{j} & \\
\text{subject to} \hspace{2em} & l_{i} \leq \sum_{j=0}^{V} a_{ij} x_{j} \leq u_{i} & \forall_{1 \leq{} i \leq{} C} \\ \text{subject to} \hspace{2em} & l_{i} \leq \sum_{j=0}^{V} a_{ij} x_{j} \leq u_{i} & \forall_{1 \leq{} i \leq{} C} \\
& x_{j} \in \mathbb{R} & \forall_{1 \leq{} j \leq{} V} & x_{j} \in \mathbb{R} & \forall_{1 \leq{} j \leq{} V}
\end{align*} \end{align*}
\noindent{}where \(V\) and \(C\) represent the number of \variables{} and number of \constraints{} respectively. In this definition \(V\) and \(C\) represent the number of \variables{} and number of \constraints{} respectively.
The vector \(c\) holds the coefficients of the objective function and the matrix \(a\) holds the coefficients for the \constraints{}. The vector \(c\) holds the coefficients of the objective function and the matrix \(a\) holds the coefficients for the \constraints{}.
The vectors \(l\) and \(u\) respectively contain the lower and upper bounds of the \constraints{}. The vectors \(l\) and \(u\) respectively contain the lower and upper bounds of the \constraints{}.
Finally, the \variables{} of the linear program are held in the \(x\) vector. Finally, the \variables{} of the linear program are held in the \(x\) vector.
@ -727,8 +727,8 @@ It was questioned whether the same problem could be solved in worst-case polynom
Methods for solving linear programs provide the foundation for a harder problem. Methods for solving linear programs provide the foundation for a harder problem.
In \gls{lp} our \variables{} must be continuous. In \gls{lp} our \variables{} must be continuous.
If we require that one or more take a integer value (\(x_{i} \in \mathbb{Z}\)), then the problem becomes \gls{np} hard. If we require that one or more take an integer value (\(x_{i} \in \mathbb{Z}\)), then the problem becomes \gls{np} hard.
The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all} \variables{} must take a integer value). The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all} \variables{} must take an integer value).
Unlike \gls{lp}, there is no algorithm that solves a mixed integer program in polynomial time. Unlike \gls{lp}, there is no algorithm that solves a mixed integer program in polynomial time.
We can, however, adapt \gls{lp} solving methods to solve a mixed integer program. We can, however, adapt \gls{lp} solving methods to solve a mixed integer program.
@ -737,7 +737,7 @@ If the \variables{} happen to take integer values in the \gls{sol}, then we have
Otherwise, we pick one of the \variables{} that needs to be integer but whose value in the \gls{sol} of the linear program is not. Otherwise, we pick one of the \variables{} that needs to be integer but whose value in the \gls{sol} of the linear program is not.
For this \variable{} we create two versions of the linear program: a version where this \variable{} is constrained to be less or equal to the value in the \gls{sol} rounded down to the nearest integer value; and a version where it is constrained to be greater or equal to the value in the \gls{sol} rounded up. For this \variable{} we create two versions of the linear program: a version where this \variable{} is constrained to be less or equal to the value in the \gls{sol} rounded down to the nearest integer value; and a version where it is constrained to be greater or equal to the value in the \gls{sol} rounded up.
Both versions are solved to find the best \gls{sol}. Both versions are solved to find the best \gls{sol}.
The process is repeated recursively until a integer \gls{sol} is found. The process is repeated recursively until an integer \gls{sol} is found.
Much of the power of this solving method comes from bounds that are inferred during the process. Much of the power of this solving method comes from bounds that are inferred during the process.
The \gls{sol} to the linear program provides an upper bound for the solution in the current step of the solving process. The \gls{sol} to the linear program provides an upper bound for the solution in the current step of the solving process.
@ -745,7 +745,7 @@ Similarly, any integer \gls{sol} found in an earlier branch of the search proces
When the upper bound given by the linear program is lower that the lower bound from an earlier solution, then we know that any integer \gls{sol} following from the linear program is strictly worse than the incumbent. When the upper bound given by the linear program is lower that the lower bound from an earlier solution, then we know that any integer \gls{sol} following from the linear program is strictly worse than the incumbent.
Over the years \gls{lp} and \gls{mip} \solvers{} have developed immensely. Over the years \gls{lp} and \gls{mip} \solvers{} have developed immensely.
Modern \solvers{}, such as \gls{cbc} \autocite{forrest-2020-cbc}, \gls{cplex} \autocite{ibm-2020-cplex}, \gls{gurobi} \autocite{gurobi-2021-gurobi}, and \gls{scip} \autocite{gamrath-2020-scip}, are routinely used to solve very large industrial optimisation problems. Modern \solvers{}, such as \gls{cbc} \autocite{forrest-2020-cbc}, \gls{cplex} \autocite{ibm-2020-cplex}, \gls{gurobi} \autocite{gurobi-2021-gurobi}, and \gls{scip} \autocite{gamrath-2020-scip}, are routinely used to solve very large industrial optimization problems.
These \solvers{} are therefore prime targets to solve \minizinc{} \instances{}. These \solvers{} are therefore prime targets to solve \minizinc{} \instances{}.
To solve an \instance{} of a \cmodel{}, it can be rewritten into a mixed integer program. To solve an \instance{} of a \cmodel{}, it can be rewritten into a mixed integer program.
@ -764,7 +764,7 @@ The indicator variables \(y_{i}\) are \gls{avar} that for a \variable{} \(x\) ta
\begin{align} \begin{align}
\text{given} \hspace{2em} & N = {1,\ldots,n} & \notag{}\\ \text{given} \hspace{2em} & N = {1,\ldots,n} & \notag{}\\
\text{maximise} \hspace{2em} & 0 & \notag{}\\ \text{maximize} \hspace{2em} & 0 & \notag{}\\
\text{subject to} \hspace{2em} & q_{i} \in N & \forall_{i \in N} \notag{}\\ \text{subject to} \hspace{2em} & q_{i} \in N & \forall_{i \in N} \notag{}\\
& y_{ij} \in \{0,1\} & \forall_{i,j \in N} \notag{}\\ & y_{ij} \in \{0,1\} & \forall_{i,j \in N} \notag{}\\
\label{line:back-mip-channel} & x_{i} = \sum_{j \in N} j * y_{ij} & \forall_{i \in N} \\ \label{line:back-mip-channel} & x_{i} = \sum_{j \in N} j * y_{ij} & \forall_{i \in N} \\
@ -793,14 +793,14 @@ The problem asks if there is an \gls{assignment} for the \variables{} of a given
This problem is a restriction of the general \gls{dec-prb} where all \variables{} have a Boolean type and all \constraints{} are simple Boolean formulas. This problem is a restriction of the general \gls{dec-prb} where all \variables{} have a Boolean type and all \constraints{} are simple Boolean formulas.
There is a field of research dedicated to solving \gls{sat} problems \autocite{biere-2021-sat}. There is a field of research dedicated to solving \gls{sat} problems \autocite{biere-2021-sat}.
In this field a \gls{sat} problem is generally standardised to be in \gls{cnf}. In this field a \gls{sat} problem is generally standardized to be in \gls{cnf}.
A \gls{cnf} is formulated in terms of literals. A \gls{cnf} is formulated in terms of literals.
These are Boolean \variables{} \(x\) or their negations \(\neg x\). 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}\). 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. 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, much progress has been made towards solving even very complex \gls{sat} problems. Even though the problem is proven to be hard to solve, much progress has been made towards solving even very 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. 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}. 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. However, even problems that contain \variables{} with types other than Boolean can still be encoded as a \gls{sat} problem.
@ -832,7 +832,7 @@ A variation on \gls{sat} is the \gls{maxsat} problem.
In a \gls{sat} problem all clauses need to be \gls{satisfied}, but this is not the case in a \gls{maxsat} problem. In a \gls{sat} problem all clauses need to be \gls{satisfied}, but this is not the case in a \gls{maxsat} problem.
Instead, clauses are given individual weights. Instead, clauses are given individual weights.
The higher the weight, the more important the clause is for the overall problem. The higher the weight, the more important the clause is for the overall problem.
The goal in the \gls{maxsat} problem is then to find an \gls{assignment} for Boolean \variables{} that maximises the cumulative weights of the \gls{satisfied} clauses. The goal in the \gls{maxsat} problem is then to find an \gls{assignment} for Boolean \variables{} that maximizes the cumulative weights of the \gls{satisfied} clauses.
The \gls{maxsat} problem is analogous to an \gls{opt-prb}. The \gls{maxsat} problem is analogous to an \gls{opt-prb}.
Like an \gls{opt-prb}, the aim of \gls{maxsat} is to find the \gls{opt-sol} to the problem. Like an \gls{opt-prb}, the aim of \gls{maxsat} is to find the \gls{opt-sol} to the problem.
@ -877,7 +877,7 @@ Different types of \solvers{} can also have access to different types of \constr
\begin{listing} \begin{listing}
\amplfile{assets/listing/back_tsp.mod} \amplfile{assets/listing/back_tsp.mod}
\caption{\label{lst:back-ampl-tsp} An \gls{ampl} model describing the \gls{tsp}} \caption{\label{lst:back-ampl-tsp} An \gls{ampl} model describing the \gls{tsp}.}
\end{listing} \end{listing}
\Lrefrange{line:back:ampl:parstart}{line:back:ampl:parend} declare the \parameters{} of the \cmodel{}. \Lrefrange{line:back:ampl:parstart}{line:back:ampl:parend} declare the \parameters{} of the \cmodel{}.
@ -935,11 +935,11 @@ The syntax of \gls{opl} is very similar to the \minizinc{} syntax.
Where \gls{opl} really shines is when modelling scheduling problems. Where \gls{opl} really shines is when modelling scheduling problems.
Resources and activities are separate objects in \gls{opl}. Resources and activities are separate objects in \gls{opl}.
This allows users to express resource scheduling \constraints{} in an incremental and more natural fashion. This allows users to express resource scheduling \constraints{} in an incremental and more natural fashion.
When solving a scheduling problem, \gls{opl} makes use of specialised interval \variables{}, which represent when a task is scheduled. When solving a scheduling problem, \gls{opl} makes use of specialized interval \variables{}, which represent when a task is scheduled.
\begin{example} \begin{example}
Let us consider modelling in \gls{opl} using the well-known ``job shop problem''. Let us consider modelling in \gls{opl} using the well-known ``job shop'' problem.
The job shop problem is similar to the open shop problem discussed in the introduction. The job shop problem is similar to the open shop problem discussed in the introduction.
Like the open shop problem, the goal is to schedule jobs with multiple tasks. Like the open shop problem, the goal is to schedule jobs with multiple tasks.
Each task must be performed by an assigned machine. Each task must be performed by an assigned machine.
@ -963,7 +963,7 @@ When solving a scheduling problem, \gls{opl} makes use of specialised interval \
Another activity is declared on \lref{line:back:opl:makespan}. Another activity is declared on \lref{line:back:opl:makespan}.
The \texttt{makespan} \variable{} represents the time spanned by all tasks. The \texttt{makespan} \variable{} represents the time spanned by all tasks.
This is enforced by the \constraint{} on \lref{line:back:opl:con1}. This is enforced by the \constraint{} on \lref{line:back:opl:con1}.
\Lref{line:back:opl:goal} sets the minimisation of \texttt{makespan} to be the goal of the model. \Lref{line:back:opl:goal} sets the minimization of \texttt{makespan} to be the goal of the model.
Resources are important notions in \gls{opl}. Resources are important notions in \gls{opl}.
A resource can be any requirement of an activity. A resource can be any requirement of an activity.
@ -992,7 +992,7 @@ When solving a scheduling problem, \gls{opl} makes use of specialised interval \
This makes it harder in \minizinc{} to write the correct \constraint{} and its meaning is less clear. This makes it harder in \minizinc{} to write the correct \constraint{} and its meaning is less clear.
\end{example} \end{example}
The \gls{opl} also contains a specialised search syntax that is used to instruct its solvers \autocite{van-hentenryck-2000-opl-search}. The \gls{opl} also contains a specialized search syntax that is used to instruct its solvers \autocite{van-hentenryck-2000-opl-search}.
This syntax gives modellers full programmatic control over how the solver explores the search space depending on the current state of the variables. This syntax gives modellers full programmatic control over how the solver explores the search space depending on the current state of the variables.
This gives the modeller more control over the search in comparison to the \gls{search-heuristic} \glspl{annotation} in \minizinc{}, which only allow modellers to select predefined \glspl{search-heuristic} already implemented in the solver. This gives the modeller more control over the search in comparison to the \gls{search-heuristic} \glspl{annotation} in \minizinc{}, which only allow modellers to select predefined \glspl{search-heuristic} already implemented in the solver.
Take, for example, the following \gls{opl} search definition: Take, for example, the following \gls{opl} search definition:
@ -1029,31 +1029,31 @@ In addition to all variable types that are supported by \minizinc{}, \gls{essenc
\item and (regular) partitions of finite types. \item and (regular) partitions of finite types.
\end{itemize} \end{itemize}
Since sets, multi-sets, and functions can be defined on any other type, these types can be arbitrarily nested and the modeller could, for example, define a \variable{} that is a set of sets of integers. Since sets, multi-sets, and functions can be defined on any other type, these types can be arbitrarily nested, the modeller could, for example, define a \variable{} that is a set of sets of integers.
Partitions are defined for finite types: Booleans, enumerated types, or a restricted set of integers. Partitions are defined for finite types: Booleans, enumerated types, or a restricted set of integers.
\begin{example} \begin{example}
Let us consider modelling in \gls{essence} using the well-known ``social golfers problem''. Let us consider modelling in \gls{essence} using the well-known ``social golfer'' problem.
In the social golfers problem, a community of golfers plans games of golf for a set number of weeks. In the social golfer problem, a community of golfers plans games of golf for a set number of weeks.
Every week all the golfers are split into groups of equal size and each group plays a game of golf. Every week all the golfers are split into groups of equal size and each group plays a game of golf.
The goal of the problem is to find a way to split the groups differently every week, such that no two golfers will meet each other twice. The goal of the problem is to find a way to split the groups differently every week, such that no two golfers will meet each other twice.
Two golfers can only be part of the same group once. Two golfers can only be part of the same group once.
A \cmodel{} for the social golfers problem in \gls{essence} can be seen in \cref{lst:back-essence-sgp}. A \cmodel{} for the social golfer problem in \gls{essence} can be seen in \cref{lst:back-essence-sgp}.
\begin{listing} \begin{listing}
\plainfile{assets/listing/back_sgp.essence} \plainfile{assets/listing/back_sgp.essence}
\caption{\label{lst:back-essence-sgp} An \gls{essence} model describing the social golfers problem} \caption{\label{lst:back-essence-sgp} An \gls{essence} model describing the social golfer problem}
\end{listing} \end{listing}
The \gls{essence} model starts with the preamble declaring the version of the language that is used. The \gls{essence} model starts with the preamble declaring the version of the language that is used.
All the \parameters{} of the \cmodel{} are declared on line \lref{line:back:essence:pars}: \texttt{weeks} is the number of weeks to be considered, \texttt{groups} is the number of groups of golfers, and \texttt{size} is the size of each group. All the \parameters{} of the \cmodel{} are declared on \lref{line:back:essence:pars}: \texttt{weeks} is the number of weeks to be considered, \texttt{groups} is the number of groups of golfers, and \texttt{size} is the size of each group.
The input for the \parameters{} is checked to ensure that they take a value that is one or higher. The input for the \parameters{} is checked to ensure that they take a value that is one or higher.
\Lref{line:back:essence:ntype} then uses the \parameters{} to declare a new type to represent the golfers. \Lref{line:back:essence:ntype} then uses the \parameters{} to declare a new type to represent the golfers.
Most of the problem is modelled on \lref{line:back:essence:var}. Most of the problem is modelled on \lref{line:back:essence:var}.
It declares a \variable{} that is a set of partitions of the golfers. It declares a \variable{} that is a set of partitions of the golfers.
The choice in \variable already contains some of the implied \constraints{}. The choice in \variable already contains some implied \constraints{}.
Because the \variable{} reasons about partitions of the golfers, a correct \gls{assignment} is already guaranteed to correctly split the golfers into groups. Because the \variable{} reasons about partitions of the golfers, a correct \gls{assignment} is already guaranteed to correctly split the golfers into groups.
The usage of a set of size \texttt{weeks} means that we directly reason about that number of partitions that have to be unique. The usage of a set of size \texttt{weeks} means that we directly reason about that number of partitions that have to be unique.
@ -1109,7 +1109,7 @@ At its core, however, the \gls{rewriting} of \gls{ess-prime} works very differen
For all concepts in the language the \compiler{} intrinsically knows how to rewrite it for its target \solver{}. For all concepts in the language the \compiler{} intrinsically knows how to rewrite it for its target \solver{}.
Recently, \textcite{gokberk-2020-ess-incr} have also presented Savile Row as the basis of a \gls{meta-optimization} toolchain. Recently, \textcite{gokberk-2020-ess-incr} have also presented Savile Row as the basis of a \gls{meta-optimization} toolchain.
The authors extend Savile Row to bridge the gap between the incremental assumption interface of \gls{sat} \solvers{} and the modelling language and show how this helps to efficiently solve pattern mining and optimisation problems. The authors extend Savile Row to bridge the gap between the incremental assumption interface of \gls{sat} \solvers{} and the modelling language and show how this helps to efficiently solve pattern mining and optimization problems.
Consequently, this research reiterates the use of \gls{meta-optimization} algorithms in \cmls{} and the need for incremental bridging between the modelling language and the \solver{}. Consequently, this research reiterates the use of \gls{meta-optimization} algorithms in \cmls{} and the need for incremental bridging between the modelling language and the \solver{}.
\section{Term Rewriting}% \section{Term Rewriting}%
@ -1149,7 +1149,7 @@ A \gls{trs} is confluent if, no-matter what order the term rewriting rules are a
It is trivial to see that our previous example is non-terminating, since you can repeat rule \(r_{3}\) an infinite amount of times. It is trivial to see that our previous example is non-terminating, since you can repeat rule \(r_{3}\) an infinite amount of times.
The system, however, is confluent, since, if it terminates, it always arrives at the same \gls{normal-form}: if the term contains any \(0\), then the result is \(0\); otherwise, the result is \(1\). The system, however, is confluent, since, if it terminates, it always arrives at the same \gls{normal-form}: if the term contains any \(0\), then the result is \(0\); otherwise, the result is \(1\).
These properties are also interesting in the translation process of a \minizinc{} instance into \flatzinc{}. These properties could also be studied in the translation process of a \minizinc{} instance into \flatzinc{}.
The \gls{confluence} of the \gls{rewriting} process would ensure that the same \gls{slv-mod} is produced independently of the order in which the \minizinc{} \instance{} is processed. The \gls{confluence} of the \gls{rewriting} process would ensure that the same \gls{slv-mod} is produced independently of the order in which the \minizinc{} \instance{} is processed.
Although this is a desirable quality, it is not guaranteed since it conflicts with important simplifications, discussed in \cref{sec:back-mzn-interpreter}, used to improve the quality of \gls{slv-mod}. Although this is a desirable quality, it is not guaranteed since it conflicts with important simplifications, discussed in \cref{sec:back-mzn-interpreter}, used to improve the quality of \gls{slv-mod}.
@ -1243,7 +1243,7 @@ This means that, for some rules, multiple terms must match, to apply the rule.
\end{example} \end{example}
The rules in a \gls{chr} system are categorised into three different categories: simplification, propagation, and simpagation. The rules in a \gls{chr} system are categorized into three different categories: simplification, propagation, and simpagation.
The first two rules in the previous example are simplification rules: they replace some \constraint{} atoms by others. The first two rules in the previous example are simplification rules: they replace some \constraint{} atoms by others.
The final rule in the example was a propagation rule: based on the existence of certain \constraints{}, new \constraints{} are introduced. The final rule in the example was a propagation rule: based on the existence of certain \constraints{}, new \constraints{} are introduced.
Simpagation rules are a combination of both types of rules in the form: Simpagation rules are a combination of both types of rules in the form:
@ -1281,20 +1281,20 @@ For instance, this replaces the usage of enumerated types by normal integers.
compiler.} compiler.}
\end{figure} \end{figure}
The middle-end contains the most important two processes: \gls{rewriting} and optimisation. The middle-end contains the most important two processes: \gls{rewriting} and optimization.
During the \gls{rewriting} process the \minizinc{} model is rewritten into a \gls{slv-mod}. During the \gls{rewriting} process the \minizinc{} model is rewritten into a \gls{slv-mod}.
It could be noted that the \gls{rewriting} step depends on the compilation target to define its \gls{native} \constraints{}. It could be noted that the \gls{rewriting} step depends on the compilation target to define its \gls{native} \constraints{}.
Even though the information required for this step is target dependent, we consider it part of the middle-end as the mechanism is the same for all compilation targets. Even though the information required for this step is target dependent, we consider it part of the middle-end as the mechanism is the same for all compilation targets.
A full description of this process will follow in \cref{subsec:back-rewriting}. A full description of this process will follow in \cref{subsec:back-rewriting}.
Once a \gls{slv-mod} is constructed, the \minizinc{} \compiler{} tries to optimise this model: shrink \domains{} of \variables{}, remove \constraints{} that are proven to hold, and remove \variables{} that have become unused. Once a \gls{slv-mod} is constructed, the \minizinc{} \compiler{} tries to optimize this model: shrink \domains{} of \variables{}, remove \constraints{} that are proven to hold, and remove \variables{} that have become unused.
These optimisation techniques are discussed in \cref{subsec:back-fzn-optimisation}. These optimization techniques are discussed in \cref{subsec:back-fzn-optimization}.
The backend converts the internal \gls{slv-mod} into a format to be used by the targeted \solver{}. The backend converts the internal \gls{slv-mod} into a format to be used by the targeted \solver{}.
Given the formatted artefact, a \solver{} process, controlled by the backend, is then started. Given the formatted artefact, a \solver{} process, controlled by the backend, is then started.
The \solver{} process produces \glspl{sol} for the \gls{slv-mod}. The \solver{} process produces \glspl{sol} for the \gls{slv-mod}.
Before these are given to the modeller, the backend reformulates these \glspl{sol} to become \glspl{sol} of the modeller's \instance{}. Before these are given to the modeller, the backend reformulates these \glspl{sol} to become \glspl{sol} of the modeller's \instance{}.
In this section we discuss the \gls{rewriting} and optimisation process as employed by the 2.5.5 version of \minizinc{} \autocite{minizinc-2021-minizinc}. In this section we discuss the \gls{rewriting} and optimization process as employed by the 2.5.5 version of \minizinc{} \autocite{minizinc-2021-minizinc}.
\subsection{Rewriting}% \subsection{Rewriting}%
\label{subsec:back-rewriting} \label{subsec:back-rewriting}
@ -1383,18 +1383,17 @@ As a consequence, evaluating the same expression twice will always reach an equi
It is therefore possible to reuse the same result for equivalent expressions. It is therefore possible to reuse the same result for equivalent expressions.
This simplification is called \gls{cse}. This simplification is called \gls{cse}.
It is a well understood technique that originates from compiler optimisation \autocite{cocke-1970-cse}. It is a well understood technique that originates from compiler optimization \autocite{cocke-1970-cse}.
\Gls{cse} has also proven to be very effective in discrete optimisation \autocite{marinov-2005-sat-optimisations, araya-2008-cse-numcsp}, including during the evaluation of \cmls{} \autocite{rendl-2009-enhanced-tailoring}. \Gls{cse} has also proven to be very effective in discrete optimization \autocite{marinov-2005-sat-optimisations, araya-2008-cse-numcsp}, including during the evaluation of \cmls{} \autocite{rendl-2009-enhanced-tailoring}.
\begin{example} \begin{example}
\label{ex:back-cse} \label{ex:back-cse}
For instance, in the \constraint{} For instance, in the following \constraint{} the same expression, \mzninline{abs(x)}, occurs twice.
\begin{mzn} \begin{mzn}
constraint (abs(x)*2 >= 20) \/ (abs(x)+5 >= 15); constraint (abs(x)*2 >= 20) \/ (abs(x)+5 >= 15);
\end{mzn} \end{mzn}
\noindent{}the expression \mzninline{abs(x)} occurs twice.
There is however no need to create two separate \variables{} (and defining \constraints{}) to represent the absolute value of \mzninline{x}. There is however no need to create two separate \variables{} (and defining \constraints{}) to represent the absolute value of \mzninline{x}.
The same \variable{} can be used to represent the \mzninline{abs(x)} in both sides of the disjunction. The same \variable{} can be used to represent the \mzninline{abs(x)} in both sides of the disjunction.
\end{example} \end{example}
@ -1417,7 +1416,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. 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} \end{example}
To ensure that two identical instantiations of a function are only evaluated once, the \minizinc{} \compiler{} uses memoisation. To ensure that two identical instantiations of a function are only evaluated once, the \minizinc{} \compiler{} uses memoization.
After the \gls{rewriting} of an expression, the instantiated expression and its result are stored in a lookup table: the \gls{cse} table. 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 rewritten the \gls{cse} table is consulted. Then before any consequent expression is rewritten the \gls{cse} table is consulted.
If an equivalent expression is found, then the accompanying result is used; otherwise, the evaluation proceeds as normal. If an equivalent expression is found, then the accompanying result is used; otherwise, the evaluation proceeds as normal.
@ -1491,9 +1490,9 @@ Finally, it can also be helpful for \solvers{} as they may need to decide on a r
During \gls{rewriting}, the \minizinc{} compiler actively removes values from the \domain{} when it encounters \constraints{} that trivially reduce it. During \gls{rewriting}, the \minizinc{} compiler actively removes values from the \domain{} when it encounters \constraints{} that trivially reduce it.
For example, it detects \constraints{} with a single comparison expression between a \variable{} and a \parameter{} (\eg\ \mzninline{x != 5}), \constraints{} with a single comparison between two \variables{} (\eg\ \mzninline{x >= y}), \constraints{} that directly change the domain (\eg\ \mzninline{x in 3..5}). For example, it detects \constraints{} with a single comparison expression between a \variable{} and a \parameter{} (\eg\ \mzninline{x != 5}), \constraints{} with a single comparison between two \variables{} (\eg\ \mzninline{x >= y}), \constraints{} that directly change the domain (\eg\ \mzninline{x in 3..5}).
It even performs more complex \gls{propagation} for some known \constraints{}. It even performs more complex \gls{propagation} for some known \constraints{}.
For example, it will reduce the \domains{} for \mzninline{int_times} and \mzninline{int_div} and we will see in the next subsection how \gls{aggregation} will help simplify certain \constraint{}. For example, it will reduce the \domains{} for \mzninline{int_times} and \mzninline{int_div}, and we will see in the next subsection how \gls{aggregation} will help simplify certain \constraint{}.
However, \gls{propagation} is only performed locally, when the \constraint{} is recognised. However, \gls{propagation} is only performed locally, when the \constraint{} is recognized.
During \gls{rewriting}, the \gls{propagation} of one \constraint{}, will not trigger the \gls{propagation} of another. During \gls{rewriting}, the \gls{propagation} of one \constraint{}, will not trigger the \gls{propagation} of another.
Crucially, the \minizinc{} compiler also handles equality \constraints{}. Crucially, the \minizinc{} compiler also handles equality \constraints{}.
@ -1517,7 +1516,7 @@ Moreover, replacing one variable for another can improve the effectiveness of \g
\end{mzn} \end{mzn}
The equality \constraint{}, replaces the \variable{} \mzninline{b} with the \variable{} \mzninline{a}. The equality \constraint{}, replaces the \variable{} \mzninline{b} with the \variable{} \mzninline{a}.
Now the two calls to \mzninline{this} suddenly become equivalent and the second will be found in the \gls{cse} table. Now the two calls to \mzninline{this} suddenly become equivalent, and the second will be found in the \gls{cse} table.
\end{example} \end{example}
Note that if the equality \constraint{} in the example would have be found after both calls, then both calls would have already been rewritten. Note that if the equality \constraint{} in the example would have be found after both calls, then both calls would have already been rewritten.
@ -1579,7 +1578,7 @@ Adding \gls{propagation} during \gls{rewriting} means that the system becomes no
This predicate expresses the \constraint{} \mzninline{b -> x<=0}, using a well-known technique called the ``Big M method''. This predicate expresses the \constraint{} \mzninline{b -> x<=0}, using a well-known technique called the ``Big M method''.
The expression \mzninline{ub(x)} returns a valid upper bound for \mzninline{x}, \ie{} a fixed value known to be greater than or equal to \mzninline{x}. The expression \mzninline{ub(x)} returns a valid upper bound for \mzninline{x}, \ie{} a fixed value known to be greater than or equal to \mzninline{x}.
This could be the initial upper bound \mzninline{x} was declared with or the current value adjusted by the \minizinc{} \compiler{}. This could be the initial upper bound \mzninline{x} was declared with, or the current value adjusted by the \minizinc{} \compiler{}.
If \mzninline{b} takes the value 0, the expression \mzninline{ub(x)*(1-b)} is equal to \mzninline{ub(x)}, and the \constraint{} \mzninline{x <= ub(x)} holds trivially. If \mzninline{b} takes the value 0, the expression \mzninline{ub(x)*(1-b)} is equal to \mzninline{ub(x)}, and the \constraint{} \mzninline{x <= ub(x)} holds trivially.
If \mzninline{b} takes the value 1, \mzninline{ub(x)*(1-b)} is equal to 0, enforcing the \constraint{} \mzninline{x <= 0}. If \mzninline{b} takes the value 1, \mzninline{ub(x)*(1-b)} is equal to 0, enforcing the \constraint{} \mzninline{x <= 0}.
\end{example} \end{example}
@ -1611,12 +1610,12 @@ However, since the rewriting of the body was delayed and the \compiler{} does no
This problem can be solved through the use of \minizinc{}'s multi-pass compilation \autocite{leo-2015-multipass}. This problem can be solved through the use of \minizinc{}'s multi-pass compilation \autocite{leo-2015-multipass}.
It can rewrite (and propagate) an \instance{} multiple times, remembering information about the earlier iteration(s). It can rewrite (and propagate) an \instance{} multiple times, remembering information about the earlier iteration(s).
As such, information normally discovered later in the \gls{rewriting} process, such as the final \domains{} of \variables{}, whether two \variables{} are equal, and whether an expressions must be \gls{reified}, can be used from the start. As such, information normally discovered later in the \gls{rewriting} process, such as the final \domains{} of \variables{}, whether two \variables{} are equal, and whether an expression must be \gls{reified}, can be used from the start.
\subsection{FlatZinc Optimisation}% \subsection{FlatZinc Optimization}%
\label{subsec:back-fzn-optimisation} \label{subsec:back-fzn-optimization}
After the \compiler{} has finished \gls{rewriting} the \minizinc{} instance, it enters the optimisation phase. After the \compiler{} has finished \gls{rewriting} the \minizinc{} instance, it enters the optimization phase.
The primary role of this phase is to further perform \gls{propagation} until \gls{fixpoint}. The primary role of this phase is to further perform \gls{propagation} until \gls{fixpoint}.
However, this phase operates at the level of the \gls{slv-mod}, where all \constraints{} are now \gls{native} \constraints{} of the target \solver{}. However, this phase operates at the level of the \gls{slv-mod}, where all \constraints{} are now \gls{native} \constraints{} of the target \solver{}.
This means that, depending on the target \solver{}, the \compiler{} will not be able to understand the meaning of all \constraints{}. This means that, depending on the target \solver{}, the \compiler{} will not be able to understand the meaning of all \constraints{}.

6
chapters/2_background_preamble.tex
View File

@ -1,4 +1,4 @@
The research presented in this thesis investigates the process of \gls{rewriting} \cmls{}. \noindent{}The research presented in this thesis investigates the process of \gls{rewriting} \cmls{}.
This chapter provides the required background information to understand \cmls{}: This chapter provides the required background information to understand \cmls{}:
\begin{itemize} \begin{itemize}
@ -9,13 +9,13 @@ This chapter provides the required background information to understand \cmls{}:
In particular, it gives further information about \minizinc{} and discusses the functionality available to create \cmodels{}. In particular, it gives further information about \minizinc{} and discusses the functionality available to create \cmodels{}.
It also provides some insight into \solvers{}, discussing the most important techniques used to solve \instances{} of \cmodels{}. It also provides some insight into \solvers{}, discussing the most important techniques used to solve \instances{} of \cmodels{}.
Additionally, it summarises the functionality of other \cmls{} to serve as a comparison with \minizinc{}. Additionally, it summarizes the functionality of other \cmls{} to serve as a comparison with \minizinc{}.
This is followed by a brief overview of other closely related \glspl{trs}. This is followed by a brief overview of other closely related \glspl{trs}.
Finally, the chapter analyses the existing approach to \gls{rewriting} \minizinc{} and discusses its limitations. Finally, the chapter analyses the existing approach to \gls{rewriting} \minizinc{} and discusses its limitations.
The overview of \cmls{} presented in this chapter supports the research and discussion presented in subsequent chapters. The overview of \cmls{} presented in this chapter supports the research and discussion presented in subsequent chapters.
In the remainder of this chapter we first, in \cref{sec:back-intro} introduce the reader to \cmls{} and their purpose. In the remainder of this chapter we first, in \cref{sec:back-intro} introduce the reader to \cmls{} and their purpose.
\Cref{sec:back-minizinc} summarises the syntax and functionality of \minizinc{}, the \cml{} used within this thesis. \Cref{sec:back-minizinc} summarizes the syntax and functionality of \minizinc{}, the \cml{} used within this thesis.
In \cref{sec:back-solving} we discuss how \gls{cp}, \gls{mip}, and \gls{sat} are used to solve a \gls{slv-mod}. In \cref{sec:back-solving} we discuss how \gls{cp}, \gls{mip}, and \gls{sat} are used to solve a \gls{slv-mod}.
\Cref{sec:back-other-languages} introduces alternative \cmls{} and compares their functionality to \minizinc{}. \Cref{sec:back-other-languages} introduces alternative \cmls{} and compares their functionality to \minizinc{}.
Then, \cref{sec:back-term} surveys the closely related technologies in the field of \glspl{trs}. Then, \cref{sec:back-term} surveys the closely related technologies in the field of \glspl{trs}.