diff --git a/assets/glossary.tex b/assets/glossary.tex index 14b52b5..6018e74 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -15,7 +15,7 @@ } \newglossaryentry{gls-ampl}{ - name={AMPL: A Mathematical Programming Language}, + name={AMPL:\ A Mathematical Programming Language}, description={}, } @@ -130,7 +130,7 @@ } \newglossaryentry{domain-con}{ - name={domain consistent}, + name={domain consistent}, description={}, } @@ -256,7 +256,7 @@ } \newglossaryentry{gls-opl}{ - name={OPL: The optimisation modelling language}, + name={OPL:\ The optimisation modelling language}, description={}, } diff --git a/chapters/2_background.tex b/chapters/2_background.tex index e0fda3d..f9d59fd 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -41,7 +41,7 @@ model. \end{listing} \begin{example}% -\label{ex:back-knapsack} + \label{ex:back-knapsack} 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 @@ -53,8 +53,8 @@ model. \begin{equation*} \text{maximise}~z~\text{subject to}~ \begin{cases} - S \subseteq T \\ - z = \sum_{i \in S} joy(i) \\ + S \subseteq T \\ + z = \sum_{i \in S} joy(i) \\ \sum_{i \in S} space(i) < C \\ \end{cases} \end{equation*} @@ -84,10 +84,10 @@ introduce \minizinc\ as the leading \cml\ used within this thesis. In constraint model. We also briefly discuss other solving techniques and the problem format these techniques expect. \Cref{sec:back-other-languages} introduces alternative \cmls\ and compares their functionality to \minizinc{}. -Then,\cref{sec:back-term} survey the some closely related technologies in the -field of \glspl{trs}. Finally, \cref{sec:back-mzn-interpreter} explores the -process that the current \minizinc\ interpreter uses to translate a \minizinc\ -instance into a solver-level constraint model. +Then,\cref{sec:back-term} survey the closely related technologies in the field +of \glspl{trs}. Finally, \cref{sec:back-mzn-interpreter} explores the process +that the current \minizinc\ interpreter uses to translate a \minizinc{} instance +into a solver-level constraint model. \section{\glsentrytext{minizinc}}% \label{sec:back-minizinc} @@ -104,7 +104,7 @@ library of constraints allow users to easily model complex problems. \end{listing} \begin{example}% -\label{ex:back-mzn-knapsack} + \label{ex:back-mzn-knapsack} Let us introduce the language by modelling the problem from \cref{ex:back-knapsack}. A \minizinc\ model encoding this problem is shown in @@ -140,22 +140,22 @@ and primitive constraints. Given the assignments \begin{mzn} -TOYS = {football, tennisball, stuffed_elephant}; -toy_joy = [63, 12, 100]; -toy_space = [32, 8, 40]; -space_left = 44; + TOYS = {football, tennisball, stuffed_elephant}; + toy_joy = [63, 12, 100]; + toy_space = [32, 8, 40]; + space_left = 44; \end{mzn} the following model is the result of flattening: \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):: defines_var(total_joy); -solve maximize total_joy; + 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):: defines_var(total_joy); + solve maximize total_joy; \end{mzn} This \emph{flat} problem will be passed to some \solver{}, which will attempt to @@ -279,13 +279,13 @@ expressions capture common (complex) relations between \variables{}. \Glspl{global} in the \minizinc\ language are used as function calls. An example of a \gls{global} is \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, -); + predicate knapsack( + array [int] of int: w, + array [int] of int: p, + array [int] of var int: x, + var int: W, + var int: P, + ); \end{mzn} This \gls{global} expresses the knapsack relationship, where the \parameters{} @@ -315,7 +315,7 @@ functions that can be used to transform or combine other expressions. For example the constraint \begin{mzn} -constraint not (a + b < c); + constraint not (a + b < c); \end{mzn} contains the infix \glspl{operator} \mzninline{+} and \mzninline{<}, and the @@ -383,7 +383,7 @@ parts: \begin{description} \item[\mzninline{G}] The generator expression which assigns the values of - collections to identifiers, + collections to identifiers, \item[\mzninline{F}] an optional filtering condition, which has to evaluate to \mzninline{true} for the iteration to be included in the array, \item[\mzninline{E}] and the expression that is evaluation for each iteration @@ -415,34 +415,34 @@ resulting definition. There are three main purposes for \glspl{let}: \item To name an intermediate expression, so it can be used multiple times or to simplify the expression. For example, the constraint - \begin{mzn} - constraint let { var int: tmp = x div 2; } in tmp mod 2 == 0 \/ tmp = 0; - \end{mzn} + \begin{mzn} + constraint let { var int: tmp = x div 2; } in tmp mod 2 == 0 \/ tmp = 0; + \end{mzn} - constrains that half of \mzninline{x} is even or zero. + constrains that half of \mzninline{x} is even or zero. \item To introduce a scoped \variable{}. For example, the constraint - \begin{mzn} - let {var -2..2: slack;} in x + slack = y; - \end{mzn} + \begin{mzn} + let {var -2..2: slack;} in x + slack = y; + \end{mzn} - constrains that \mzninline{x} and \mzninline{y} are at most two apart. + constrains that \mzninline{x} and \mzninline{y} are at most two apart. \item To constrain the resulting expression. For example, the following function - \begin{mzn} - function var int: int_times(var int: x, var int: y) = - let { - var int: z; - constraint pred_int_times(x, y, z); - } in z; - \end{mzn} + \begin{mzn} + function var int: int_times(var int: x, var int: y) = + let { + var int: z; + constraint pred_int_times(x, y, z); + } in z; + \end{mzn} - returns a new \variable{} \mzninline{z} that is constrained to be the - multiplication of \mzninline{x} and \mzninline{y} by the relational - multiplication constraint \mzninline{pred_int_times}. + returns a new \variable{} \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 flattening \glspl{let} is that any \variables{} that @@ -457,14 +457,14 @@ definitions and in the resulting expression. \subsection{Reification}% \label{subsec:back-reification} -With the rich expression language in \minizinc{}, \constraints{} can consist -of complex expressions that do not translate to a single constraint at the -\solver{} level. Instead different parts of a complex expression will be -translated into different \constraints{}. Not all of these constraint will -be globally enforced by the solver. \constraints{} stemming for -sub-expressions will typically be \emph{reified} into a Boolean variable. -\Gls{reification} means that a variable \mzninline{b} is constrained to be true -if and only if a corresponding constraint \mzninline{c(...)} holds. +With the rich expression language in \minizinc{}, \constraints{} can consist of +complex expressions that do not translate to a single constraint at the +\solver{} level. Instead, different parts of a complex expression will be +translated into different \constraints{}. Not all of these \constraints{} will be +globally enforced by the solver. \constraints{} stemming for sub-expressions +will typically be \emph{reified} into a Boolean variable. \Gls{reification} +means that a variable \mzninline{b} is constrained to be true if and only if a +corresponding constraint \mzninline{c(...)} holds. \begin{example} Consider the \minizinc\ model: @@ -477,9 +477,9 @@ if and only if a corresponding constraint \mzninline{c(...)} holds. This model maximises the number of even numbers taken by the elements of the array \mzninline{x}. In this model the expression \mzninline{x[i] mod 2 == 0} - has to reified. Since the elements have a domain from 1 to 15 and are + has to be reified. 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 + take even values. Instead, the solver is tasked to maximise the number of reified variables it can set to \mzninline{true}. \end{example} @@ -509,33 +509,33 @@ Some expressions in the \cmls\ do not always have a well-defined result. the constraint should be trivially true. \end{example} -Part of the semantics of a \cmls\ is the choice as to how to treat these partial +Part of the semantics of a \cmls{} is the choice as to how to treat these partial functions. Examples of such expressions in \minizinc\ are: \begin{itemize} \item Division (or modulus) when the divisor is zero: - \begin{mzn} - x div 0 = @??@ - \end{mzn} + \begin{mzn} + x div 0 = @??@ + \end{mzn} \item Array access when the index is outside the given index set: - \begin{mzn} - array1d(1..3, [1,2,3])[0] = @??@ - \end{mzn} + \begin{mzn} + array1d(1..3, [1,2,3])[0] = @??@ + \end{mzn} \item Finding the minimum or maximum or an empty set: - \begin{mzn} - min({}) = @??@ - \end{mzn} + \begin{mzn} + min({}) = @??@ + \end{mzn} \item Computing the square root of a negative value: - \begin{mzn} - sqrt(-1) = @??@ - \end{mzn} + \begin{mzn} + sqrt(-1) = @??@ + \end{mzn} \end{itemize} @@ -550,32 +550,32 @@ in \cmls\ \autocite*{frisch-2009-undefinedness}: \begin{description} \item[Strict] \cmls\ employing a ``strict'' undefinedness semantic do not - allow any undefined behaviour during the evaluation of the constraint model. - If during the flattening or solving process an expression is found to be - undefined, then any expressions in which it is used is also marked as - undefined. In the end, this means that the occurrence of a single undefined - expression will mark the full model as undefined. + allow any undefined behaviour during the evaluation of the constraint model. + If during the flattening or solving process an expression is found to be + undefined, then any expressions in which it is used is also marked as + undefined. In the end, this means that the occurrence of a single undefined + expression will mark the full model as undefined. \item[Kleene] The ``Kleene'' semantic treat undefined expressions as - expressions for which not enough information is available. This if an - expression contains undefined sub-expression, it will only be marked as - undefined if the value of the sub-expression is required to compute its - result. Take for example the expression \mzninline{false -> E}. Here, when - \mzninline{E} is undefined the result of the expression can still be said to - be \mzninline{true}, since the value of \mzninline{E} does not influence the - result of the expression. However, if we take the expression \mzninline{true - /\ E}, then when \mzninline{E} is undefined the overall expression is also - undefined since the value of the expression cannot be determined. + expressions for which not enough information is available. This if an + expression contains undefined sub-expression, it will only be marked as + undefined if the value of the sub-expression is required to compute its + result. Take for example the expression \mzninline{false -> E}. Here, when + \mzninline{E} is undefined the result of the expression can still be said to + be \mzninline{true}, since the value of \mzninline{E} does not influence the + result of the expression. However, if we take the expression \mzninline{true + /\ E}, then when \mzninline{E} is undefined the overall expression is also + undefined since the value of the expression cannot be determined. \item[Relational] The ``relational'' semantic follows from the fact that all - expressions in \cmls\ will eventually become 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. For example, the expression \mzninline{x div 0} is - undefined, but the relationship \mzninline{int_div(x,0,y)} can be said to be - \mzninline{false}. It can be said that the relational semantic will make the - closest relational expression that contains an undefined expression - \mzninline{false}. + expressions in \cmls\ will eventually become 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. For example, the expression \mzninline{x div 0} is + undefined, but the relationship \mzninline{int_div(x,0,y)} can be said to be + \mzninline{false}. It can be said that the relational semantic will make the + closest relational expression that contains an undefined expression + \mzninline{false}. \end{description} @@ -593,7 +593,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 ``relational'' semantics. \jip{TODO:\@ This also corresponds to Kleene semantics, maybe I -should use a different example} + should use a different example} Frisch and Stuckey also show that different \solvers{} often employ different semantics \autocite*{frisch-2009-undefinedness}. It is therefore important that, @@ -606,11 +606,11 @@ model. \label{sec:back-solving} There are many prominent techniques to solve a \constraint{} model, but none of -them will solve a \minizinc\ model directly. Instead a \minizinc\ model get +them will solve a \minizinc\ model directly. Instead, a \minizinc\ model get translated into \variables{} and \constraints{} of the type that the solver supports directly. -\minizinc\ was initially designed as an input language for \gls{cp} \solvers{}. +\minizinc{} was initially designed as an input language for \gls{cp} \solvers{}. These \glspl{solver} often support many of the high-level \constraints{} that are written in a \minizinc\ model. For \gls{cp} solvers the amount of translation required can vary a lot. It depends on which \constraints{} the @@ -618,7 +618,7 @@ targeted \gls{cp} \solver{} are directly supported and which \constraints{} have to be decomposed. Because \gls{cp} \solvers{} work on a similar level as the \minizinc\ language, -some of the techniques used in \gls{cp} \solvers{} can also be used during the +some techniques used in \gls{cp} \solvers{} can also be used during the transformation from \minizinc\ to \flatzinc{}. The usage of these techniques can often help shrink the \glspl{domain} of \variables{} and eliminate or simplify \constraint{}. \Cref{subsec:back-cp} explains the general method employed by @@ -630,7 +630,7 @@ approaches to finding solutions to \constraint{} models. Although these they also bring new challenges in to efficiently encode the problem for these \solvers{}. To understand these challenges in the translations a \minizinc\ model into a solver level \constraint{} model, the remainder of this section -will discuss the other dominant technologies used used by \minizinc\ \solver{} +will discuss the other dominant technologies used by \minizinc\ \solver{} targets and their input language. \subsection{Constraint Programming}% @@ -643,13 +643,13 @@ every value in the \gls{domain} all \variables{}. It will not surprise the reader that this is an inefficient approach. Given, for example, the constraint \begin{mzn} -constraint a + b = 5; + constraint a + b = 5; \end{mzn} It is clear that when the value \mzninline{a} is known, then the value of \mzninline{b} can be deduced. \gls{cp} is the idea solving \glspl{csp} by -performing an intelligent search by inferring which which values are still -feasible for each \variable{} \autocite{rossi-2006-cp}. +performing an intelligent search by inferring which values are still feasible +for each \variable{} \autocite{rossi-2006-cp}. To find a solution to a given \gls{csp}, a \gls{cp} \solver{} will perform a depth first search. At each node, the \solver{} will try and eliminate any @@ -678,10 +678,10 @@ only able to prove that the problem is unsatisfiable by exploring the full search space. \Gls{propagation} is not only used when starting the search, but also after -making each search decision. This means that some of the \gls{propagation} -depends on the search decision. Therefore, if the \solver{} needs to reconsider -a search decision, then it must also undo all \gls{domain} changes that were -caused by \gls{propagation} dependent on that search decision. +making each search decision. This means that some \gls{propagation} depends on +the search decision. Therefore, if the \solver{} needs to reconsider a search +decision, then it must also undo all \gls{domain} changes that were caused by +\gls{propagation} dependent on that search decision. The general most common method in \gls{cp} \solvers{} to achieve this is to keep track of \gls{domain} changes using a \gls{trail}. For every \gls{domain} change @@ -696,78 +696,78 @@ search decision. Furthermore, because propagation is performed to a \gls{fixpoint}, it is guaranteed that no duplicate propagation is required. The solving method used by \gls{cp} \solvers{} is very flexible. A \solver{} can -support many different 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 propagators. Therefore, -a \gls{csp} modelled for one \solver{} might look very different to an -equivalent \gls{csp} modelled for a different solver. Instead, \cmls{}, like -\minizinc{}, can serve as a standardised form of input for these \solvers{}. -They allow modellers to use high-level constraints that are used directly by the -solver when supported or they are automatically translated to a collection of -equivalent supported constraints otherwise. +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 propagators. Therefore, a \gls{csp} modelled +for one \solver{} might look very different to an equivalent \gls{csp} modelled +for a different solver. Instead, \cmls{}, like \minizinc{}, can serve as a +standardised form of input for these \solvers{}. They allow modellers to use +high-level constraints that are used directly by the solver when supported, or +they are automatically translated to a collection of equivalent supported +constraints otherwise. \begin{example}% -\label{ex:back-nqueens} -Consider as an example the N-Queens problem. Given a chess board of size -\(n \times n\), find a placement for \(n\) queen chess pieces such that no queen -can attack another. Meaning only one queen per row, one queen per column, and -one queen per diagonal. The problem can be modelled in \minizinc\ as follows. + \label{ex:back-nqueens} + Consider as an example the N-Queens problem. Given a chess board of size + \(n \times n\), find a placement for \(n\) queen chess pieces such that no queen + can attack another. Meaning only one queen per row, one queen per column, and + one queen per diagonal. The problem can be modelled in \minizinc\ as follows. -\begin{mzn} - int: n; - array [1..n] of var 1..n: q; + \begin{mzn} + int: n; + array [1..n] of var 1..n: q; - constraint all_different(q); - constraint all_different([q[i] + i | i in 1..n]); - constraint all_different([q[i] - i | i in 1..n]); -\end{mzn} + constraint all_different(q); + constraint all_different([q[i] + i | i in 1..n]); + constraint all_different([q[i] - i | i in 1..n]); + \end{mzn} -Since we know that there can only be one queen per column, the decision in the -model left to make is, for every queen, where in the column the piece is placed. -The \constraints{} in the model model the remaining rules of the problem: no two -queen can be placed in the same row, no two queen can be place in the same -upward diagonal, and no two queens can be place in the same downward diagonal. -This model can be directly used in most \gls{cp} \solvers{}, since integer -\variables{} and an \mzninline{all_different} \gls{propagator} are common. + Since we know that there can only be one queen per column, the decision in the + model left to make is, for every queen, where in the column the piece is + placed. The \constraints{} in the model the remaining rules of the problem: no + two queen can be placed in the same row, no two queen can be place in the same + upward diagonal, and no two queens can be place in the same downward diagonal. + This model can be directly used in most \gls{cp} \solvers{}, since integer + \variables{} and an \mzninline{all_different} \gls{propagator} are common. -When solving the problem, initially no values can be eliminated from the -\glspl{domain} of the \variables{}. The first propagation will happen when the -first queen is placed on the board. The search space will then look like this: + When solving the problem, initially no values can be eliminated from the + \glspl{domain} of the \variables{}. The first propagation will happen when the + first queen is placed on the board. The search space will then look like this: -\jip{insert image of nqueens board with one queen assigned.} + \jip{Insert image of n-queens board with one queen assigned.} -Now that one queen is placed on the board the propagators for the -\mzninline{all_different} constraints can start propagating. They can eliminate -all values that are on the same row or diagonal as the queen placed on the -board. + Now that one queen is placed on the board the propagators for the + \mzninline{all_different} constraints can start propagating. They can eliminate + all values that are on the same row or diagonal as the queen placed on the + board. -\jip{insert previous image with all impossible moves marked red.} + \jip{Insert previous image with all impossible moves marked red.} \end{example} In \gls{cp} solving there is a trade-off between the amount of time spend -propagating a constraint and the the amount of search that is otherwise -required. The golden standard for a \gls{propagator} is to be \gls{domain-con}, -meaning that all values left in the \glspl{domain} of its \variables{} there is -at least one possible variable assignment that satisfies the constraint. -Designing an algorithm that reaches this level of consistency is, however, an -easy task and might require high complexity. Instead it can 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}. +propagating a constraint and the amount of search that is otherwise required. +The golden standard for a \gls{propagator} is to be \gls{domain-con}, meaning +that all values left in the \glspl{domain} of its \variables{} there is at least +one possible variable assignment that satisfies the constraint. Designing an +algorithm that reaches this level of consistency is, however, an easy task and +might require high complexity. Instead, it can 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}. 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. Instead \solvers{} generally -use a \gls{bounds-con} \gls{propagator}, which guarantee only that the minimum -and maximum values in the \glspl{domain} of the \variables{} are used in at -least one possible assignment that satisfies the constraint. +realistic \gls{domain-con} \gls{propagator} exists. Instead, \solvers{} +generally use a \gls{bounds-con} \gls{propagator}, which guarantee only that the +minimum and maximum values in the \glspl{domain} of the \variables{} are used in +at least one possible assignment that satisfies the constraint. Thus far, we have only considered \glspl{csp}. \gls{cp} solving can, however, also be used to solve optimisation problems using a method called \gls{bnb}. The \gls{cp} \solver{} will follow the same method as previously described. However, -when it find a solution, it does not yet know if this solution is optimal. It is +when it finds a solution, it does not yet know if this solution is optimal. It is merely an incumbent solution. The \solver{} must therefore resume its search, but it is no longer interested in just any solution, only solutions that have a better \gls{objective} value. This is achieved by adding a new \gls{propagator} @@ -778,7 +778,7 @@ process does not find any other solutions, then it is proven that there are no better solutions than the current incumbent solution. \gls{cp} solvers like Chuffed \autocite{chuffed-2021-chuffed}, Choco -\autocite{prudhomme-2016-choco}, Gecode \autocite{gecode-2021-gecode}, and +\autocite{prudhomme-2016-choco}, \gls{gecode} \autocite{gecode-2021-gecode}, and OR-Tools \autocite{perron-2021-ortools} have long been one of the leading method to solve \minizinc\ instances. @@ -793,9 +793,9 @@ using a set of linear equations over continuous variables. In general, a linear program can be expressed in the form: \begin{align*} - \text{maximise} \hspace{2em} & \sum_{j=1}^{V} c_{j} x_{j} & \\ + \text{maximise} \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_{i=1}^{C} \\ - & x_{i} \in \mathbb{R} & \forall_{i=1}^{V} + & x_{i} \in \mathbb{R} & \forall_{i=1}^{V} \end{align*} where \(V\) and \(C\) represent the number of variables and number of @@ -817,7 +817,7 @@ The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all} Unlike \gls{lp}, there is no algorithm that can solve a mixed integer program in polynomial time. The general method to solve a mixed integer program is to treat -it as an linear program and find an optimal solution using the simplex method. +it as a linear program and find an optimal solution using the simplex method. If the \variables{} in the problem that are required to be discrete already have discrete values, then we have found our optimal solution. Otherwise, we pick one of the \variables{}. For this \variable{} we create a version of the linear @@ -830,7 +830,7 @@ found. Much of the power of this solving method comes from bounds that can be inferred during the process. The solution that the simplex provides an upper bound for the solution in the current step of the solving process. Similarly, any discrete -solution found in an earlier branches of the search process provide a lower +solution found in an earlier branch of the search process provide a lower bound. When the upper bound given by the simplex method is lower that the lower bound from an earlier solution, then we know that any discrete solutions following from the linear program will be strictly worse than the incumbent. @@ -839,7 +839,7 @@ Over the years \gls{lp} and \gls{mip} \solvers{} have developed immensely. \solvers{}, such as CBC \autocite{forrest-2020-cbc}, CPLEX \autocite{cplex-2020-cplex}, Gurobi \autocite{gurobi-2021-gurobi}, and SCIP \autocite{gamrath-2020-scip}, can solve many complex problems. It is therefore -often worthwhile to encode problem as an mixed integer program to find a +often worthwhile to encode problem as a mixed integer program to find a solution. \glspl{csp} can be often be encoded as mixed integer programs. This does, @@ -854,17 +854,17 @@ linear \constraints{} using the \variables{} \(y_{i}\). \begin{example} Let us again consider the N-Queens problem from \cref{ex:back-nqueens}. The - following model shows a integer program of this problem. + following model shows an integer program of this problem. \begin{align} - \text{given} \hspace{2em} & N = {1,\ldots,n} & \\ - \text{maximise} \hspace{2em} & 0 & \\ - \text{subject to} \hspace{2em} & q_{i} \in N & \forall_{i \in N} \\ - & y_{ij} \in \{0,1\} & \forall_{i,j \in N} \\ - \label{line:back-mip-channel} & x_{i} = \sum_{j \in N} j * y_{ij} & \forall_{i \in N} \\ - \label{line:back-mip-row} & \sum_{i \in N} y_{ij} \leq 1 & \forall_{j \in N} \\ - \label{line:back-mip-diag1} & \sum_{i,j \in N. i + j =k} y_{ij} \leq 1 & \forall_{k=3}^{2n-1} \\ - \label{line:back-mip-diag2} & \sum_{i,j \in N. i - j =k} y_{ij} \leq 1 & \forall_{k=2-n}^{n-2} + \text{given} \hspace{2em} & N = {1,\ldots,n} & \\ + \text{maximise} \hspace{2em} & 0 & \\ + \text{subject to} \hspace{2em} & q_{i} \in N & \forall_{i \in N} \\ + & y_{ij} \in \{0,1\} & \forall_{i,j \in N} \\ + \label{line:back-mip-channel} & x_{i} = \sum_{j \in N} j * y_{ij} & \forall_{i \in N} \\ + \label{line:back-mip-row} & \sum_{i \in N} y_{ij} \leq 1 & \forall_{j \in N} \\ + \label{line:back-mip-diag1} & \sum_{i,j \in N. i + j =k} y_{ij} \leq 1 & \forall_{k=3}^{2n-1} \\ + \label{line:back-mip-diag2} & \sum_{i,j \in N. i - j =k} y_{ij} \leq 1 & \forall_{k=2-n}^{n-2} \end{align} @@ -907,7 +907,7 @@ instances of the problem with thousands of \variables{} and clauses. Many real world problems modelled in \cmls\ directly correspond to \gls{sat}. However, even problems that contain \variables{} with types other than Boolean -can often be encoded as a \gls{sat} problem. Depending of the problem, using a +can often be encoded as a \gls{sat} 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. @@ -917,13 +917,13 @@ efficient way to solve the problem. following. \begin{align} - \text{given} \hspace{2em} & N = {1,\ldots,n} & \\ - \text{find} \hspace{2em} & q_{ij} \in \{\text{true}, \text{false}\} & \forall_{i,j \in N} \\ - \label{line:back-sat-at-least}\text{subject to} \hspace{2em} & \exists_{j \in N} q_{ij} & \forall_{i \in N} \\ - \label{line:back-sat-row}& \neg q_{ij} \lor \neg q_{ik} & \forall_{i,j \in N} \forall_{k=j}^{n}\\ - \label{line:back-sat-col}& \neg q_{ij} \lor \neg q_{kj} & \forall_{i,j \in N} \forall_{k=i}^{n}\\ - \label{line:back-sat-diag1}& \neg q_{ij} \lor \neg q_{(i+k)(j+k)} & \forall_{i,j \in N} \forall_{k=1}^{min(n-i, n-j)}\\ - \label{line:back-sat-diag2}& \neg q_{ij} \lor \neg q_{(i+k)(j-k)} & \forall_{i,j \in N} \forall_{k=1}^{min(n-i, j)} + \text{given} \hspace{2em} & N = {1,\ldots,n} & \\ + \text{find} \hspace{2em} & q_{ij} \in \{\text{true}, \text{false}\} & \forall_{i,j \in N} \\ + \label{line:back-sat-at-least}\text{subject to} \hspace{2em} & \exists_{j \in N} q_{ij} & \forall_{i \in N} \\ + \label{line:back-sat-row} & \neg q_{ij} \lor \neg q_{ik} & \forall_{i,j \in N} \forall_{k=j}^{n} \\ + \label{line:back-sat-col} & \neg q_{ij} \lor \neg q_{kj} & \forall_{i,j \in N} \forall_{k=i}^{n} \\ + \label{line:back-sat-diag1} & \neg q_{ij} \lor \neg q_{(i+k)(j+k)} & \forall_{i,j \in N} \forall_{k=1}^{\min(n-i, n-j)} \\ + \label{line:back-sat-diag2} & \neg q_{ij} \lor \neg q_{(i+k)(j-k)} & \forall_{i,j \in N} \forall_{k=1}^{\min(n-i, j)} \end{align} The encoding of the problem uses a Boolean \variable{} for every position of @@ -938,18 +938,18 @@ efficient way to solve the problem. A variation on \gls{sat} is the \gls{maxsat} problem. Where in a \gls{sat} problem all clauses need to be satisfied, this is not the case in a \gls{maxsat} -problem. Instead clauses are given individual weights. The higher the weight, +problem. Instead, clauses are given individual weights. 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 a assignment for Boolean \variables{} that +\gls{maxsat} problem is then to find an assignment for Boolean \variables{} that maximises the cumulative weights of the satisfied clauses. The \gls{maxsat} problem is analogous to a \gls{cop}. Like a \gls{cop}, the aim of \gls{maxsat} is to find the optimal solution to the problem. The difference is that the weights are given to the \constraints{} instead of the \variables{} or a function over them. It is, again, often possible to encode a \gls{cop} as a -\gls{maxsat} problem. A naive approach approach to encode an integer objective -is, for example, to encode each value in the domain as a Boolean variable and -assign that same value to a clause containing just that Boolean variable. +\gls{maxsat} problem. A naive approach to encode an integer objective is, for +example, to encode each value in the domain as a Boolean variable and assign +that same value to a clause containing just that Boolean variable. For many problems the use of \gls{maxsat} \solvers{} can offer a very successful method to find the optimal solution to a problem. @@ -962,11 +962,11 @@ 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 can be adapted to these languages. -We will now discuss some of the other prominent \cmls{} and will compare them to -\minizinc\ to indicate to the reader where techniques might have to be adjusted +We will now discuss some other prominent \cmls{} and will compare them to +\minizinc{} to indicate to the reader where techniques might have to be adjusted to fit other languages. -A notable difference between all these these languages and \minizinc\ is that +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. @@ -1065,7 +1065,7 @@ scheduled. \begin{example} For example the \variable{} declarations and \constraints{} - for a jobshop problem would look like this in an \gls{opl} model: + for a job shop problem would look like this in an \gls{opl} model: \begin{plain} ScheduleHorizon = sum(j in Jobs, t in Tasks) duration[j, t]; @@ -1163,16 +1163,16 @@ cherished for its adoption of high-level \variable{} types. In addition to all variable types that are contained in \minizinc{}, \gls{essence} also contains: \begin{itemize} - \item finite sets of non-iteger types, - \item finite multisets of any type, + \item Finite sets of non-integer types, + \item finite multi-sets of any type, \item finite (partial) functions, \item and (regular) partitions of finite types. \end{itemize} -Since sets, multisets, and functions can be defined on any other type, these +Since sets, multi-sets, and functions can be defined on any other type, these types can be arbitrary nested and the modeller can define, for example, a -\variable{} that is a set of set of integers. Partitions can be defined for -finite types. These types in \gls{essence} are restricted to Booleans, +\variable{} that is a sets of sets of integers. Partitions can be defined for +finite types. These types in \gls{essence} are restricted to Boolean, enumerated types, or a restricted set of integers. \begin{example} @@ -1245,7 +1245,7 @@ the targeted solver. At the heart of the flattening process lies a \gls{trs}. A \gls{trs} \autocite{baader-1998-term-rewriting} describes a computational model the full -process can be describe as the application of rules +process can be described as the application of rules \(l \rightarrow r_{1}, \ldots r_{n}\), that replace a \gls{term} \(l\) with one or more \glspl{term} \(r_{1}, \ldots r_{n}\). A \gls{term} is an expression with nested sub-expressions consisting of \emph{function} and \emph{constant} @@ -1259,9 +1259,9 @@ sub-expression. rewrite logical and operations: \begin{align*} - (r_{1}):\hspace{5pt}& 0 \land x \rightarrow 0 \\ - (r_{2}):\hspace{5pt}& 1 \land x \rightarrow x \\ - (r_{3}):\hspace{5pt}& x \land y \rightarrow y \land x + (r_{1}):\hspace{5pt} & 0 \land x \rightarrow 0 \\ + (r_{2}):\hspace{5pt} & 1 \land x \rightarrow x \\ + (r_{3}):\hspace{5pt} & x \land y \rightarrow y \land x \end{align*} From these rules it follows that @@ -1306,9 +1306,9 @@ models: \gls{clp} and \gls{chr}. \glsreset{clp} \gls{clp} \autocite{marriott-1998-clp} can be seen as a predecessor of \cmls{} -like \minizinc. A constraint logic program describes the process in which a high +like \minizinc{}. A constraint logic program describes the process in which a high level constraint model is eventually rewritten into a solver level constraints -and added to a \solver{}. Like in \minizinc, can define \constraint{} predicates +and added to a \solver{}. Like in \minizinc{}, can define \constraint{} predicates to use in the definition of the \constraint{} model. Different from \minizinc{}, constraint predicates in \gls{clp} can be rewritten in multiple ways. The goal of a constraint logic program is to rewrite all \constraints{} in such a way @@ -1316,11 +1316,11 @@ that the solver level \glspl{constraint} are all satisfied. Variables are another notable difference between \cmls\ and \gls{clp}. In \gls{clp}, like in a conventional \gls{trs}, a variable is merely a name. The -symbol might be replace or equated with a constant symbol, but, different from +symbol might 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 -a instantiated solution is required, a special \mzninline{labeling} constraint +an instantiated solution is required, a special \mzninline{labeling} constraint can be used to force a variable to take a constant value. Similarly, there is a \mzninline{minimize} that can be used to find the optimal value for a variable. @@ -1332,7 +1332,7 @@ all constraints are rewritten and no inconsistency is detected between the solver level constraints that are produced. If all the possible ways of rewriting the program are tried, but all of them prove to be inconsistent, then the program itself can be said to be unsatisfiable. Even when a correct -rewriting is found, it is possible to continue the process. This ways you can +rewriting is found, it is possible to continue the process. This way you can find all possible correct ways to rewrite the program. To implement this mechanism there is a tight integration between the \solver{}, @@ -1385,12 +1385,12 @@ apply the rule. \item The first rules states that if \texttt{X = Y}, then \texttt{X -> Y} is logically true. This rule removes the term \texttt{X -> Y}. Since the constraint is said to be logically true, nothing gets added. \texttt{X - = Y} functions as a guard. This \solver{} builtin \constraint{} is + = Y} functions as a guard. This \solver{} built-in \constraint{} is required for the rewriting rule to apply. \item The second rule implements the anti-symmetry of logical implications; the two implications, \texttt{X -> Y} and \texttt{Y -> X}, are - replaced by a \solver{} builtin, \texttt{X = Y}. + replaced by a \solver{} built-in, \texttt{X = Y}. \item Finally, the transitivity rule introduces a derived constraint. When it finds constraints \texttt{X -> Y} and \texttt{Y -> Z}, then it adds @@ -1404,21 +1404,21 @@ apply the rule. \end{example} The rules in a \gls{chr} system can be categorised into three different -categories: simplification, propagation, simpagation. The first two rules in the -previous example are simplification rules: they replace some constraint atoms by -others. The final rule in the example was a propagation rule: based on the -existence of certain constraints, new constraints can be introduced. Simpagation -rules are a combination of both types of rules in the form: +categories: simplification, propagation, and simpagation. The first two rules in +the previous example are simplification rules: they replace some constraint +atoms by others. The final rule in the example was a propagation rule: based on +the existence of certain constraints, new constraints can be introduced. +Simpagation rules are a combination of both types of rules in the form: \[ H_{1}, \ldots H_{l} \backslash H_{l+1}, \ldots, H_{n} \texttt{<=>} G_{1}, \ldots{}, G_{m} | B_{1}, \ldots, B_{o} \] It is possible to rewrite using a simpagation rule when there are terms matching -\(H_{1}, \ldots, H_{n}\) and there are \solver{} built-ins -\(G_{1}, \ldots{}, G_{m}\). When the simpagation rule is applied, the terms -\(H_{l+1}, \ldots, H_{n}\) are replaced by the terms \(B_{1}, \ldots, B_{o}\). -The terms \(H_{1}, \ldots H_{l}\) are kept in the system. Since simpagation -rules incorporate both the elements of simplication and propagation rules, it is -possible to formulate all rules as simpagation rules. +\(H_{1}, \ldots, H_{n}\) and there are \solver{} built-ins \(G_{1}, \ldots{}, +G_{m}\). When the simpagation rule is applied, the terms \(H_{l+1}, \ldots, +H_{n}\) are replaced by the terms \(B_{1}, \ldots, B_{o}\). The terms \(H_{1}, +\ldots H_{l}\) are kept in the system. Since simpagation rules incorporate both +the elements of simplification and propagation rules, it is possible to +formulate all rules as simpagation rules. \subsection{ACD Term Rewriting}% \label{subsec:back-acd} @@ -1525,7 +1525,7 @@ flattening of the expression is merely a calculation to find the value of the literal to be put in its place. If, however, the expression contains a \variable{}, then this calculation cannot be performed during the flattening process. Instead, a new \variable{} must be created to represent the value of -the sub-expression and it must be constrained to take the value corresponding to +the sub-expression, and it must be constrained to take the value corresponding to the expression. The creation of this new \variable{} and defining \constraints{} happens in one of two ways: @@ -1562,7 +1562,7 @@ happens in one of two ways: \begin{mzn} function var int: max(var int: x, var int: y) :: promise_total = - let { + let { var max(lb(x),lb(y))..max(ub(x),ub(y)): m ::is_defined_var; constraint int_max(x,y,m) ::defines_var(m); } in m; @@ -1579,14 +1579,14 @@ the utmost importance. A \flatzinc\ containing extra \variables{} and \constraints{} that do not add any information to the solving process might exponentially slow down the solving process. Therefore, the \minizinc\ flattening process is extended using many techniques to help improve the quality -of the flattened model. In \crefrange{subsec:back-cse}{subsec:back-delayed-rew} -we will discuss the most important techniques used to improved the flattening +of the flattened model. In \crefrange{subsec:back-cse}{subsec:back-delayed-rew}, +we will discuss the most important techniques used to improve the flattening process. \subsection{Common Sub-expression Elimination}% \label{subsec:back-cse} -Because the evaluation of a \minizinc\ expression cannot have any side-effects, +Because the evaluation of a \minizinc{} expression cannot have any side effects, it is possible to reuse the same result for equivalent expressions. This simplification is a well understood technique that originates from compiler optimisation \autocite{cocke-1970-cse} and has proven to be very effective in @@ -1601,7 +1601,7 @@ discrete optimisation \autocite{marinov-2005-sat-optimisations, constraint (abs(x)*2 >= 20) \/ (abs(x)+5 >= 15); \end{mzn} - the expression \mzninline{abs(x)} is occurs twice. There is however no need to + 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}. The same \variable{} can be used to represent the \mzninline{abs(x)} in both sides of the disjunction. @@ -1616,7 +1616,7 @@ following example. \begin{mzn} function var float: pythagoras(var float: a, var float: b) = - let { + let { var float: x = pow(a, 2); var float: y = pow(b, 2); } in sqrt(x + y); @@ -1641,7 +1641,7 @@ normal to evaluate \mzninline{x = pow(i, 2)}. However, the expression defining \mzninline{y}, \mzninline{pow(i, 2)}, will be found in the \gls{cse} table and replaced by the earlier stored result: \mzninline{y = x}. -\gls{cse} also has an important interaction with the occurence of reified +\gls{cse} also has an important interaction with the occurrence of reified constraints. \Glspl{reification} of a \constraint{} are often defined in the library in terms of complicated decompositions into simpler constraints, or require specialised algorithms in the target solvers. In either case, it can be @@ -1693,14 +1693,14 @@ be proven \mzninline{true} or \mzninline{false}. This principle also applies during the flattening 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 constraint -does not need to be added at all and that constricting the domain is enough. +\gls{domain} of a \variable{}. Sometimes this might mean that the \constraint{} +does not need to be added at all and that constricting the \gls{domain} is enough. Tight domains can also allow us to avoid the creation of reified constraints -when the truth-value of a reified constraints can be determined from the +when the truth-value of a reified \constraint{} can be determined from the \glspl{domain} of variables. \begin{example}% -\label{ex:back-adj-dom} + \label{ex:back-adj-dom} Consider the following \minizinc\ model: \begin{mzn} @@ -1716,7 +1716,7 @@ when the truth-value of a reified constraints can be determined from the If we however consider the first \constraint{}, then we deduce that \mzninline{a} must always take a value that is 4 or lower. When the compiler - adjust the domain of \mzninline{a} while flattening the first \constraint{}, + adjusts the domain of \mzninline{a} while flattening the first \constraint{}, then the second \gls{constraint} can be simplified. The expression \mzninline{a > 5} is known to be \mzninline{false}, which means that the constraint can be simplified to \mzninline{true}. @@ -1754,13 +1754,13 @@ operators. For example the evaluation of the linear constraint \mzninline{x + This \flatzinc\ model is correct, but, at least for pure \gls{cp} solvers, the existence of the intermediate variables is likely to have a negative impact on the \solver{}'s performance. These \solvers{} would likely perform better had -they received the equivalent linear constraint +they directly received the equivalent linear \constraint{}: \begin{mzn} -constraint int_lin_le([1,2,-1], [x,y,z], 0) + constraint int_lin_le([1,2,-1], [x,y,z], 0) \end{mzn} -directly. Since many solvers support linear constraints, it is often an +Since many solvers support linear constraints, it is often an additional burden to have intermediate values that have to be given a value in the solution. @@ -1778,7 +1778,7 @@ aggregated constraint, the compiler will not flatten the expression. The compiler will instead perform a search of its sub-expression to collect all other expressions to form an aggregated constraint. The flattening process continues by flattening this aggregated constraint, which might still contain -unflattened arguments. +non-flat arguments. \subsection{Delayed Rewriting}% \label{subsec:back-delayed-rew} @@ -1818,15 +1818,15 @@ not always clear which order of evaluation is best. The same problem occurs with \glspl{reification} that are produced during flattening. Other constraints could fix the domain of the reified \variable{} -and make the \gls{reification} unnecessary. Instead the constraint (or its +and make the \gls{reification} unnecessary. Instead, the constraint (or its negation) can be flattened in root context. This could avoid the use of a big decomposition or an expensive propagator. To tackle this problem, the \minizinc\ compiler employs \gls{del-rew}. When a linear \constraint{} is aggregated or a relational \gls{reification} -\constraint{} is introduced it is not directly flattened. Instead these +\constraint{} is introduced it is not directly flattened. Instead, these constraints are appended to the end of the current \gls{ast}. All other -constraints currently still unflattened, that could change the relevant +not yet flattened constraints, that could change the relevant \glspl{domain}, will be flattened first. Note that this heuristic does not guarantee that \variables{} have their @@ -1837,9 +1837,9 @@ the \glspl{domain} of \variables{} used by other delayed \constraints{}. \label{subsec:back-fzn-optimisation} After the compiler is done flattening the \minizinc\ instance, it enters the -optimisation phase. This phase occurs at the same stage as the as the solver -input language. Depending on the targeted \solver{}, the \minizinc\ flattener -might still understand the meaning of certain constraints. In these cases, +optimisation phase. This phase occurs at the same stage as the solver input +language. Depending on the targeted \solver{}, the \minizinc\ flattener might +still understand the meaning of certain constraints. In these cases, \gls{propagation} methods (as discussed in \cref{subsec:back-cp}) can be used to eliminate values from variable \glspl{domain} and simplify \constraints{}. diff --git a/latexindent.yaml b/latexindent.yaml new file mode 100644 index 0000000..a60a90f --- /dev/null +++ b/latexindent.yaml @@ -0,0 +1,6 @@ +# verbatim environments specified +# in this field will not be changed at all! +verbatimEnvironments: + mzn: 1 + nzn: 1 + plain: 1