From cc5d1fd01634c616ec21763323ef1a2a24f85835 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Sun, 16 May 2021 15:18:41 +1000 Subject: [PATCH] Work on the flattening section --- assets/acronyms.tex | 2 + assets/packages.tex | 2 - chapters/2_background.tex | 352 +++++++++++++++++++++++++------------- 3 files changed, 237 insertions(+), 119 deletions(-) diff --git a/assets/acronyms.tex b/assets/acronyms.tex index a6d45ad..d89125f 100644 --- a/assets/acronyms.tex +++ b/assets/acronyms.tex @@ -49,3 +49,5 @@ \newacronym[see={[Glossary:]{gls-trs}}]{trs}{TRS\glsadd{gls-trs}}{Term Rewriting System} + +\newacronym{tsp}{TSP\glsadd{gls-trs}}{Travelling Salesperson Problem} diff --git a/assets/packages.tex b/assets/packages.tex index 15bf428..071d80c 100644 --- a/assets/packages.tex +++ b/assets/packages.tex @@ -44,8 +44,6 @@ BoldItalicFont=*-BoldItalic, \usepackage{amssymb} \usepackage{unicode-math} -\renewcommand{\thefootnote}{\fnsymbol{footnote}} - % References \usepackage[ style=apa, diff --git a/chapters/2_background.tex b/chapters/2_background.tex index 0716cff..b4d43e8 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -637,6 +637,11 @@ 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 to fit other languages. +A notable difference between all these 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. + \subsection{AMPL}% \label{sub:back-ampl} @@ -660,7 +665,8 @@ has even been extended to allow the usage of certain \glspl{global} when using a \begin{example} - The following + If we consider the well-known \gls{tsp}, then we might model this problem in + \gls{ampl} as follows: \begin{plain} set Cities ordered; @@ -682,6 +688,15 @@ has even been extended to allow the usage of certain \glspl{global} when using a sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (j,i) in Paths} X[j,i] >= 2; \end{plain} + This model shows that the \gls{ampl} syntax has many features similar to + \minizinc{}. Like \minizinc{}, \gls{ampl} has an extensive expression + language, which includes \gls{generator} expressions and a vast collection of + \glspl{operator}. The building block of the model are also similar: + \gls{parameter} declarations, \gls{variable} declarations, \glspl{constraint}, + and a solving goal. + + The same problem can be modelled in \minizinc\ as follows: + \begin{mzn} enum CITIES; array[CITIES, CITIES] of int: cost; @@ -693,8 +708,20 @@ has even been extended to allow the usage of certain \glspl{global} when using a solve minimize sum(i in CITIES) (cost[i, next[CITIES]]); \end{mzn} + Even though the \gls{ampl} is similar to \minizinc{}, the models could not be + more different. The main reason for this difference is the level at which + these models are written. The \gls{ampl} model is written to target a + \gls{mip} solver. In the \gls{ampl} language this means that you can only use + the language functionality that is compatible with the targeted \gls{solver}; + in this case, all expression have to be linear equations. In \minizinc\ the + modeller is not constrained in the same way. The modeller is always encouraged + to create high-level \gls{constraint} models. It is the job of the + \gls{solver}'s \minizinc\ library to transform the high-level constraints into + compatible \gls{solver}-level \glspl{constraint}. \end{example} + + \subsection{OPL}% \label{sub:back-opl} @@ -708,66 +735,71 @@ Resources and activities are separate objects in the \gls{opl}. This allows users express resource scheduling \glspl{constraint} in an incremental and more natural fashion. When solving a scheduling problem, the \gls{opl} makes use of specialised \gls{interval} \glspl{variable}, which represent when a task will be -scheduled. For example the \gls{variable} declarations and \glspl{constraint} -for a jobshop problem would look like this in an \gls{opl} model: +scheduled. -\begin{plain} - ScheduleHorizon = sum(j in Jobs, t in Tasks) duration[j, t]; - Activity task[j in Jobs, t in Tasks] (duration[j,t]); - Activity makespan; - UnaryResource tool[Machines]; +\begin{example} + For example the \gls{variable} declarations and \glspl{constraint} + for a jobshop problem would look like this in an \gls{opl} model: - minimize makespan.end - subject to { - forall (j in Jobs) - task[j,nbTasks] precedes makespan; + \begin{plain} + ScheduleHorizon = sum(j in Jobs, t in Tasks) duration[j, t]; + Activity task[j in Jobs, t in Tasks] (duration[j,t]); + Activity makespan; + UnaryResource tool[Machines]; - forall (j in Jobs) - forall (t in 1..nbTasks-1) - task[j, t] precedes task[j, t+1]; + minimize makespan.end + subject to { + forall (j in Jobs) + task[j,nbTasks] precedes makespan; - forall (j in Jobs) - forall (t in Tasks) - task[j, t] requires tool[resource[j, t]]; - }; -\end{plain} + forall (j in Jobs) + forall (t in 1..nbTasks-1) + task[j, t] precedes task[j, t+1]; -The equivalent declarations and \glspl{constraint} would look like this in -\minizinc{}: + forall (j in Jobs) + forall (t in Tasks) + task[j, t] requires tool[resource[j, t]]; + }; + \end{plain} -\begin{mzn} - int: horizon = sum(j in Jobs, t in Tasks)(duration[j,t]); - var 0..horizon: makespan; - array[JOB,TASK] of var 0..maxt: start; + The equivalent declarations and \glspl{constraint} would look like this in + \minizinc{}: - constraint forall(j in Jobs, t in 1..nbTasks-1) ( - start[j,t] + duration[j,t] <= start[j,t+1] - ); + \begin{mzn} + int: horizon = sum(j in Jobs, t in Tasks)(duration[j,t]); + var 0..horizon: makespan; + array[JOB,TASK] of var 0..maxt: start; - constraint forall(j in Jobs) ( - start[j, nbTasks] + duration[j, nbTasks] <= makespan - ); + constraint forall(j in Jobs, t in 1..nbTasks-1) ( + start[j,t] + duration[j,t] <= start[j,t+1] + ); - constraint forall(m in Machines) ( - disjunctive( - [start[j,t] | j in Jobs, t in Tasks where resource[j,t] == m], - [duration[j,t] | j in Jobs, t in Tasks where resource[j,t] == m], - ) - ); + constraint forall(j in Jobs) ( + start[j, nbTasks] + duration[j, nbTasks] <= makespan + ); - solve minimize makespan; -\end{mzn} + constraint forall(m in Machines) ( + disjunctive( + [start[j,t] | j in Jobs, t in Tasks where resource[j,t] == m], + [duration[j,t] | j in Jobs, t in Tasks where resource[j,t] == m], + ) + ); -Note that the \minizinc{} model does not have explicit Activity variables. It -must instead use \glspl{variable} that represent the start times of the activity -and a \gls{variable} to represent the time at which all activities are finished. -The \gls{opl} model also has the advantage that it can first create resource -objects and then use the \texttt{requires} keyword to force tasks on the same -machine to be mutually exclusive. In \minizinc{} the same requirement is -implemented through the use of \mzninline{disjunctive} constraints. Although -this has the same effect, all mutually exclusive jobs have to be combined in a -single statement in the model. This can make it harder in \minizinc\ to write -the correct \gls{constraint} and its meaning might be less clear. + solve minimize makespan; + \end{mzn} + + Note that the \minizinc{} model does not have explicit Activity variables. It + must instead use \glspl{variable} that represent the start times of the activity + and a \gls{variable} to represent the time at which all activities are finished. + The \gls{opl} model also has the advantage that it can first create resource + objects and then use the \texttt{requires} keyword to force tasks on the same + machine to be mutually exclusive. In \minizinc{} the same requirement is + implemented through the use of \mzninline{disjunctive} constraints. Although + this has the same effect, all mutually exclusive jobs have to be combined in a + single statement in the model. This can make it harder in \minizinc\ to write + the correct \gls{constraint} and its meaning might be less clear. + +\end{example} The \gls{opl} also contains a specialised search syntax that can be used to instruct its solvers \autocite{van-hentenryck-2000-opl-search}. This syntax @@ -797,10 +829,6 @@ search mechanism and that the \gls{solver} reasons about search on the same level as the \gls{opl} model. It is therefore not possible to connect other \glspl{solver} to \gls{opl}. -The \gls{opl} does not allow modellers to create their own (user-defined) -functions. A modeller is restricted to the \gls{global} constraint library -provided by the \gls{opl}'s standard library. - \subsection{Essence}% \label{sub:back-essence} @@ -822,66 +850,69 @@ types can be arbitrary nested and the modeller can define, for example, a finite types. These types in \gls{essence} are restricted to Booleans, enumerated types, or a restricted set of integers. -For example, the Social Golfers Problem, can be modelled in \gls{essence} as -follows: +\begin{example} + Consider, for example, the Social Golfers Problem, can be modelled in + \gls{essence} as follows: -\begin{plain} -language Essence 1.3 + \begin{plain} + language Essence 1.3 -given w, g, s : int(1..) + given w, g, s : int(1..) -letting Golfers be new type of size g * s + letting Golfers be new type of size g * s -find sched : set (size w) of - partition (regular, numParts g, partSize s) from Golfers + find sched : set (size w) of + partition (regular, numParts g, partSize s) from Golfers -such that + such that -forAll g1, g2 : Golfers, g1 < g2 . - (sum week in sched . toInt(together({g1, g2}, week))) <= 1 -\end{plain} + forAll g1, g2 : Golfers, g1 < g2 . + (sum week in sched . toInt(together({g1, g2}, week))) <= 1 + \end{plain} -In \minizinc{} the same problem could be modelled as: + In \minizinc{} the same problem could be modelled as: -\begin{mzn} -include "globals.mzn"; + \begin{mzn} + include "globals.mzn"; -int: g; -int: w; -int: s; + int: g; + int: w; + int: s; -enum: golfers = anon_enum(g * s); + enum: golfers = anon_enum(g * s); -set of int: groups = 1..g; -set of int: rounds = 1..w; -array [rounds, groups] of var set of golfers: group; + set of int: groups = 1..g; + set of int: rounds = 1..w; + array [rounds, groups] of var set of golfers: group; -constraint forall (r in rounds, g in groups) ( - card(group[r, g]) = s -); + constraint forall (r in rounds, g in groups) ( + card(group[r, g]) = s + ); -constraint forall(r in rounds) ( - all_disjoint(g in groups)(group[r, g]) -); + constraint forall(r in rounds) ( + all_disjoint(g in groups)(group[r, g]) + ); -constraint forall (a, b in golfers where a < b) ( - sum (r in rounds, g in groups) ( - {a, b} subset group[r, g] - ) <= 1 -); -\end{mzn} + constraint forall (a, b in golfers where a < b) ( + sum (r in rounds, g in groups) ( + {a, b} subset group[r, g] + ) <= 1 + ); + \end{mzn} -Note that, through the \gls{essence} type system, the first 2 \glspl{constraint} -in the \minizinc{} are implied in the \gls{essence} model. This is an example -where the use of high-level types can help give the modeller create more concise -models. + Note that, through the \gls{essence} type system, the first 2 + \glspl{constraint} in the \minizinc{} are implied in the \gls{essence} model. + This is an example where the use of high-level types can help give the + modeller create more concise models. -These high-level variables are often not directly supported by the -\glspl{solver} that is employed to solve \gls{essence} instances. To solve the -problem, not only do the \glspl{constraint} have to be translated to -\glspl{constraint} supported by the solver, but also all \glspl{variable} have -to be translated to a combination of \glspl{constraint} and \glspl{variable} -compatible with the targeted solver. +\end{example} + +The high-level variables available in \gls{essence} are often not directly +supported by the \glspl{solver} that is employed to solve \gls{essence} +instances. To solve the problem, not only do the \glspl{constraint} have to be +translated to \glspl{constraint} supported by the solver, but also all +\glspl{variable} have to be translated to a combination of \glspl{constraint} +and \glspl{variable} compatible with the targeted solver. \section{Term Rewriting}% \label{sec:back-term} @@ -1135,32 +1166,119 @@ and the call itself is a constraint primitive for the target \gls{solver}. To arrive at a flat model, the flattening process will transverse the declarations, \glspl{constraint}, and the solver goal and flatten any expression -contained in these items. The flattening of an expression is a recursive -process. \Gls{parameter} literals and \gls{variable} identifiers are already -flat. For any other kind of expression, its arguments are first flattened. If -the expression itself is a constraint primitive, then it is ready +contained in these items. During the flattening of an expression, the expression +rewritten into other \minizinc\ expressions according to the decomposition given +in the target \gls{solver}'s \minizinc\ library. Enforced by \minizinc{}'s type +system, at most one rule applies for any given constraint. The flattening of +expressions is performed bottom-up, we flatten any sub-expression before its +parent expression. For instance, in a call each argument is flattened before the +call itself is flattened. -\jip{This should say something about introducing relational reified constraints.} +An exception to this bottom-up approach is the flattening of \gls{generator} +expressions. Expression containing \glspl{generator}, such as array +\glspl{comprehension} and loops, have to be instantiated before their +sub-expression can be flattened. The compiler exhaustively binds the values of +the \gls{generator} to the specified identifiers. For each iteration the +compiler flattens the sub-expression and collects its result. Once the +\gls{generator} is exhausted, the compiler can flatten its surrounding +expression using the collected values. + +The decomposition system in \minizinc\ is defined in terms of functions +declarations. Any call, whose declaration has a function body, will eventually +be replaced by an instantiation of this function body using the arguments to the +call. Calls are, however, not the only type of expression that are decomposed +during the flattening process. Other expression, like \gls{operator} +expressions, variable array access, and if-then-else expressions, might also +have to be decomposed for the targeted \gls{solver}. During the flattening +process, these expressions are rewritten into equivalent call expressions that +will start the decomposition process. + +A notable effect of the flattening is that sub-expression are replaced by +literals or identifiers. If the expression contains only \glspl{parameter}, then +the 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 +\gls{variable}, then this calculation cannot be performed during the flattening +process. Instead, a new \gls{variable} must be created to represent the value of +the sub-expression and it must be constrained to take the value corresponding to +the expression. The creation of this new \gls{variable} and defining +\glspl{constraint} happens in one of two ways: + +\begin{itemize} + + \item For Boolean expressions in a reified context, the new \gls{variable} is + inserted by the flattening process itself. To constrain this + \gls{variable}, the flattener will then add a new reified constraint. + This constraint contains a call a variation of the call that would have + been generated for the expression in root context. The name of the + function is appended with \mzninline{_reif} and an extra Boolean + \gls{variable} argument is added to the call. The definition of this + constraint should implement the reification of the original expression: + setting the additional argument to \mzninline{true} if the constraint is + satisfied, and \mzninline{false} otherwise. For example, the constraint + in \minizinc{} + + \begin{mzn} + constraint b \/ this_call(x, y); + \end{mzn} + + will during flattening be turned into: + + \begin{mzn} + var bool: i1; + constraint this_call_reif(x, y, i1); + constraint b \/ i1 + \end{mzn} + + \item For other expressions, the \gls{variable} and defining + \glspl{constraint} are introduced in the definition of the function + itself. For example, the definition of the \mzninline{max} function in + the standard library, which calculates the maximum of two values, is + defined as: + + \begin{mzn} + function var int: max(var int: x, var int: y) :: promise_total = + 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; + \end{mzn} + + Using a \gls{let} it explicitly creates a new \gls{variable}, constrains + this \gls{variable} to take to correct value, and returns the newly + created \gls{variable}. +\end{itemize} + +These are the basic steps that are followed to flatten \minizinc\ instance. This +is, however, not the complete process. The quality of a \flatzinc\ model is of +the utmost importance. A \flatzinc\ containing extra \glspl{variable} and +\glspl{constraint} 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 the remainder of this section we will discuss the +most important techniques utilised in the flattener. \paragraph{Common Sub-expression Elimination} Because the evaluation of a \minizinc\ expression cannot have any side-effects, -In some cases, it is even possible to not generate definitions in the first -place through the use of \gls{cse}. This simplification is a well understood -technique that originates from compiler optimisation \autocite{cocke-1970-cse} -and has 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}. +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 +discrete optimisation \autocite{marinov-2005-sat-optimisations, + araya-2008-cse-numcsp}, including during the evaluation of \cmls\ +\autocite{rendl-2009-enhanced-tailoring}. -For instance, in the constraint\\ -\begin{mzn} - constraint (abs(x)*2 >= 20) \/ (abs(x)+5 >= 15); -\end{mzn} +\begin{example} + For instance, in the constraint -the expression \mzninline{abs(x)} is occurs twice. There is however no need to -create two separate \glspl{variable} (and defining \glspl{constraint}) to -represent the absolute value of \mzninline{x}. The same \gls{variable} can be -used to represent the \mzninline{abs(x)} in both sides of the disjunction. + \begin{mzn} + 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 + create two separate \glspl{variable} (and defining \glspl{constraint}) to + represent the absolute value of \mzninline{x}. The same \gls{variable} can be + used to represent the \mzninline{abs(x)} in both sides of the disjunction. +\end{example} Seeing that the same expression occurs multiple times is not always easy. Some expressions only become syntactically equal during evaluation, as in the