From 87ff8426f3f9355a71b319386836e26b201723f4 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Mon, 26 Apr 2021 16:41:38 +1000 Subject: [PATCH] Add more about the MiniZinc structure --- assets/glossary.tex | 10 +- chapters/2_background.tex | 210 ++++++++++++++++++++----------- chapters/A1_minizinc_grammar.tex | 2 +- 3 files changed, 146 insertions(+), 76 deletions(-) diff --git a/assets/glossary.tex b/assets/glossary.tex index c578092..8fa99c4 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -69,11 +69,6 @@ description={}, } -\newglossaryentry{variable}{ - name={decision variable}, - description={}, -} - \newglossaryentry{domain}{ name={domain}, description={}, @@ -200,6 +195,11 @@ description={}, } +\newglossaryentry{variable}{ + name={decision variable}, + description={}, +} + \newglossaryentry{zinc}{ name={Zinc}, description={}, diff --git a/chapters/2_background.tex b/chapters/2_background.tex index 333ab74..c5a4663 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -13,7 +13,7 @@ Freuder states that the ``Holy Grail'' of programming languages would be where the user merely states the problem, and the computer solves it and that \gls{constraint-modelling} is one of the biggest steps towards this goal to this day \autocite*{freuder-1997-holygrail}. Different from imperative (and even -other declarative) languages, in a \cml\ the modeller does not describe how to +other declarative) languages, in a \cml{} the modeller does not describe how to solve the problem, but rather provides the problem requirements. You could say that a constraint model actually describes the solution to the problem. @@ -23,14 +23,12 @@ already know, the \glspl{parameter}, what we wish to know, the \glspl{variable}, and the relationships that should exist between them, the \glspl{constraint}. This type of combinatorial problem is typically called a \gls{csp}. Many \cmls\ -also support the modelling of \gls{cop}, where a \gls{csp} is augmented with an -\gls{objective} \(z\). In this case the goal is to find an solution that +also support the modelling of \gls{cop}, where a \gls{csp} is augmented with a +\gls{objective} \(z\). In this case the goal is to find a solution that satisfies all \glspl{constraint} while minimising (or maximising) \(z\). Although a constraint model does not contain any instructions to find a suitable -solution, dedicated solving programs exist - -these models can generally be given to a dedicated solving program, or +solution, these models can generally be given to a dedicated solving program, or \gls{solver} for short, that can find a solution that fits the requirements of the model. @@ -59,7 +57,7 @@ the model. knapsack problem} \autocite[13--67]{silvano-1990-knapsack}. A commonly used solution to this problem is based on dynamic programming. An implementation of this approach is shown in \cref{lst:2-dyn-knapsack}. The use of dynamic - programming avoid the exponential growth of the problem when increasing the + programming avoids the exponential growth of the problem when increasing the number of toys. Although expert knowledge can sometimes bring you an efficient solution to a @@ -92,13 +90,13 @@ the model. the \gls{parameter} \(C\) is that depicts the total space that is left in the car before packing the toys. - This constraint model gives a abstract mathematical definition of the + This constraint model gives an abstract mathematical definition of the \gls{cop} that would be easy to adjust to changes in the requirements. To solve instances of this problem, however, these instances have to be - transformed into input accepted by a \gls{solver}. \cmls\ are designed to - allow the modeller to express combinatorial problems in a similar fashion to - the above mathematical definition and generate a definition that can be used - by dedicated solvers. + transformed into input accepted by a \gls{solver}. \cmls{} are designed to + allow the modeller to express combinatorial problems similar to the above + mathematical definition and generate a definition that can be used by + dedicated solvers. \end{example} @@ -114,7 +112,7 @@ and \gls{clp}. \section{\glsentrytext{minizinc}}% \label{sec:back-minizinc} -\minizinc\ is a high-level, solver- and data-independent modelling language for +\minizinc{} is a high-level, solver- and data-independent modelling language for discrete satisfiability and optimisation problems \autocite{nethercote-2007-minizinc}. Its expressive language and extensive library of constraints allow users to easily model complex problems. @@ -143,21 +141,21 @@ library of constraints allow users to easily model complex problems. The model then declares its \glspl{variable}. \Lref{line:back:knap:sel} declares the main \gls{variable} \mzninline{selection}, which represents the selection of toys to be packed. \(S\) in our earlier model. 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 \gls{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. Finally, the model contains a constraint, on \lref{line:back:knap:con}, to ensure we do not exceed the given capacity and states the goal for the solver: - to maximise the value of the variable \mzninline{total_joy}. + to maximise the value of the \gls{variable} \mzninline{total_joy}. \end{example} One might note that, although more textual and explicit, the \minizinc\ model definition is very similar to our earlier mathematical definition. Given ground assignments to input \glspl{parameter}, a \minizinc\ model is -translated (via a process called \emph{flattening}) into a set of variables and -primitive constraints. +translated (via a process called \emph{flattening}) into a set of +\glspl{variable} and primitive constraints. Given the assignments @@ -181,29 +179,103 @@ solve maximize total_joy; \end{mzn} This \emph{flat} problem will be passed to some \gls{solver}, which will attempt -to determine an assignment to each decision variable \mzninline{solection_i} and +to determine an assignment to each \gls{variable} \mzninline{solection_i} and \mzninline{total_joy} that satisfies all constraints and maximises \mzninline{total_joy}, or report that there is no such assignment. \subsection{Model Structure}% \label{subsec:back-mzn-structure} +As we have seen in \cref{ex:back-mzn-knapsack}, a \minizinc\ model generally +contains value declarations, both for \glspl{variable} and input +\glspl{parameter}, \glspl{constraint}, and a solving goal. More complex models +might also include definitions for custom types, user defined functions, and a +custom output format. In \minizinc\ these items are not constrained to occur in +any particular order. We will briefly discuss the most important model items. +For a detailed overview of the structure of \minizinc\ models you can consult +the full syntactic structure of \minizinc\ 2.5.5 in \cref{ch:minizinc-grammar}. +Nethercote et al.\ and Mariott et al.\ offer a detailed discussion of the +\minizinc\ and \zinc\ language, its predecessor, respectively +\autocite*{nethercote-2007-minizinc,marriott-2008-zinc}. +Values in \minizinc\ are declared in the form \mzninline{@\(T\)@: @\(I\)@ = +@\(E\)@;}. \(T\) is the type of the declared value, \(I\) is a new identifier +used to reference the declared value, and, optionally, the modeller can +functionally define the value using an expression \(E\). The identifier used in +a top-level value definition must be unique. Two declarations with the same +identifier will result in an error during the flattening process. -\subsection{MiniZinc Types}% -\label{subsec:back-mzn-type} +The main types used in \minizinc\ are Boolean, integer, floating point numbers, +sets of integers, and (user-defined) enumerated types. These types can be used +both as normal \glspl{parameter} and as \glspl{variable}. To better structure +models, \minizinc\ allows collections of these types to be contained in arrays. +Unlike other languages, arrays can have a user defined index set, which can +start at any value, but has to be a continuous range. For example, an array +going from 5 to 10 of new boolean \glspl{variable} might be declared as -\jip{TODO:\@ Here we talk about the different types in \minizinc. The main types - used in \minizinc\ are Booleans, integers, floating point numbers, sets of - integers, enumerated types. These types can be used both as normal - \glspl{parameter} and as \glspl{variable}. \minizinc\ is allows all these - types to be contained in arrays. Unlike other languages, arrays can have a - user defined index set. Although the index can start at any value the set is - forced to be a range. \minizinc\ also has an annotation type, annotations can - be either a declared name or a function call. These annotations can be - attached to \minizinc\ expressions, declarations, or constraints. } +\begin{mzn} + array[5..10] of var bool: bs; +\end{mzn} -\jip{This should explain array types} +The type in a declaration can, however, be more complex when the modeller uses a +type expression. These expressions constrain a declaration, not just to a +certain type, but also to a set of value. This set of values is generally +referred to as the \gls{domain} of a \gls{variable}. In \minizinc\ any +expression that has a set type can be used as a type expression. For example, +the following two declarations + +\begin{mzn} + var 3..5: x; + var {1,3,5}: y; +\end{mzn} + +declare two integer \glspl{variable} that can take the values from three to five and +one, three, and five respectively. + +If the declaration includes an expression to functionally define the value, then +the identifier can be used as a name for this expression. If, however, the type +of the declaration is given as a type expression, then this places an implicit +\gls{constraint} on the expression, forcing the result of the expression to take +a value according to the type expression. + +\gls{constraint} items, \mzninline{constraint @\(E\)@;} contain the top-level +constraint of the \minizinc\ model. A constraint item contains only a single +expression \(E\) of Boolean type. During the flattening of the model the +expressions in constraints are translated into solver level versions of the same +expression. It is important that the solver-level versions of the expressions +are equisatisfiable, meaning they are only satisfied if-and-only-if the original +expression would have been satisfied. + +A \minizinc\ model can contain a single goal item. This item can signal the +solver to do one of three actions: to find an assignment to the \glspl{variable} +that satisfies the constraints, \mzninline{solve satisfy;}, to find an +assignment to the \glspl{variable} that satisfies the constraints and minimises +the value of a \gls{variable}, \mzninline{solve minimize x;}, or similarly +maximises the value of a \gls{variable}, \mzninline{solve maximize x;}. + +Common structures in \minizinc\ can be captured using function declarations. A +user can declare a function \mzninline{function @\(T\)@: @\(I\)@(@\(P\)@) = E;}. +In the function declaration \(T\) is the type of the result of the function, +\(I\) is the identifier for the function, \(P\) is a list types and identifiers +for the parameters of the functions, and finally \(E\) is the expression that +can use the parameters \(P\) and when flattened will give the result of the +function. The \minizinc\ language offers the keywords \mzninline{predicate} and +\mzninline{test} as a shorthand for \mzninline{function var bool} and +\mzninline{function bool} respectively. For example a function that squares an +integer can be defined as follows. + +\begin{mzn} + function int: square(int: a) = a * a; +\end{mzn} + +Function declarations are also the main way in which \gls{solver} libraries are +defined. During flattening all \minizinc\ expressions are (eventually) rewritten +to function calls. A solver can then provide its own implementation for these +functions. It is assumed that the implementation of the functions in the +\gls{solver} libraries will ultimately be rewritten into fully relational call. +When a relational constraint is directly supported by a solver the function +should be declared within an expression body. Any call to such function is +directly placed in the flattened model. \subsection{MiniZinc Expressions}% \label{subsec:back-mzn-expr} @@ -211,20 +283,18 @@ to determine an assignment to each decision variable \mzninline{solection_i} and One of the powers of the \minizinc\ language is the extensive expression language that it offers to help modellers create models that are intuitive to read, but are transformed to fit the structure best suited to the chosen -\gls{solver}. We will now briefly discussed the most important \minizinc\ -expressions and the general methods employed when flattening them. For a -detailed overview of all \minizinc\ you can consult the full syntactic structure -of the \minizinc\ expressions in \minizinc\ 2.5.5 can be found in -\cref{sec:mzn-grammar-expressions}. Nethercote et al.\ and Mariott et al.\ offer -a detailed discussion of the expression language of \minizinc\ and its -predecessor \zinc\ respectively +\gls{solver}. We will now briefly discuss the most important \minizinc\ +expressions and the general methods employed when flattening them. A detailed +overview of the full syntactic structure of the \minizinc\ expressions in +\minizinc\ 2.5.5 can be found in \cref{sec:mzn-grammar-expressions}. Nethercote +et al.\ and Mariott et al.\ offer a detailed discussion of the expression +language of \minizinc\ and its predecessor \zinc\ respectively \autocite*{nethercote-2007-minizinc,marriott-2008-zinc}. \Glspl{global} are the basic building blocks in the \minizinc\ language. These -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 - +expressions capture common (complex) relations between \glspl{variable}. +\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, @@ -237,9 +307,9 @@ predicate knapsack( This \gls{global} expresses the knapsack relationship, where the \glspl{parameter} \mzninline{w} are the weights of the items, \mzninline{p} are -the profit for each items, the \glspl{variable} in \mzninline{x} represent the +the profit for each item, the \glspl{variable} in \mzninline{x} represent the amount of time the items are present in the knapsack, and \mzninline{W} and -\mzninline{P}, repectively, represent the weight and profit of the knapsack. +\mzninline{P}, respectively, represent the weight and profit of the knapsack. Note that the usage of this \gls{global} might have simplified the \minizinc\ model in \cref{ex:back-mzn-knapsack}: @@ -252,12 +322,12 @@ The usage of this \gls{global} has the additional benefit that the knapsack structure of the problem is then known to the \gls{solver} which might implement special handling of the relationship. -Although \minizinc\ contains a extensive library of \glspl{global}, many +Although \minizinc\ contains an extensive library of \glspl{global}, many problems contain constraints that aren't covered by a \gls{global}. There are many other expression forms in \minizinc\ that can help modellers express a constraint. -\Gls{operator} symbols in \minizinc\ are used as short hands for \minizinc\ +\Gls{operator} symbols in \minizinc\ are used as a shorthand for \minizinc\ functions that can be used to transform or combine other expressions. For example the constraint @@ -274,19 +344,18 @@ comparison, and Boolean negation functions respectively. Although the different (overloaded) versions of these functions will be used during flattening. For \glspl{parameter} types the result of the function can be directly computed, but when flattening these functions with \glspl{variable} -types a new variable for its result must be introduced and a constraints +types a new \gls{variable} for its result must be introduced and a constraint enforcing the functional relationship. The choice between different expressions can often be expressed using a \gls{conditional} expression, sometimes better known as an ``if-then-else'' expressions. You could, for example, force that the absolute value of \mzninline{a} is bigger than \mzninline{b} using the constraint - \begin{mzn} constraint if b >= 0 then a > b else b < a endif; \end{mzn} -In \minizinc\ the result of an \gls{conditional} expression is, however, not +In \minizinc\ the result of a \gls{conditional} expression is, however, not contained to Boolean types. The condition in the expression, the ``if'', must be of a Boolean type, but as long as the different sides of the \gls{conditional} expression are the same type it is a valid conditional expression. This can be @@ -300,9 +369,9 @@ used to, for example, define an absolute value function for integer When the condition does not contain any \glspl{variable}, then the flattening of a \gls{conditional} expression will result in one of the side of the -expressions. If, however, the condition does contain a \glspl{variable}, then -the result of the condition cannot be defined during the flattening. Instead, -the expression will introduce a new variable for the result of the expression +expressions. If, however, the condition does contain a \gls{variable}, then the +result of the condition cannot be defined during the flattening. Instead, the +expression will introduce a new \gls{variable} for the result of the expression and a constraint to enforce the functional relationship. In \minizinc\ special \mzninline{if_then_else} \glspl{global} are available to implement this relationship. @@ -322,7 +391,7 @@ referenced by expression. \Gls{array} \glspl{comprehension} are expressions can be used to compose \gls{array} objects. This allows modellers to create \glspl{array} that are not -given directly as input to the model or are a declared collection of variables. +given directly as input to the model or are a declared collection of \glspl{variable}. \Gls{generator} expressions, \mzninline{[E | G where F]}, consist of three parts: @@ -336,19 +405,19 @@ parts: when the filtering condition succeeds. \end{description} -The following example composes a array that contains the doubled even values of +The following example composes an \gls{array} that contains the doubled even values of an \gls{array} \mzninline{x}. -\begin{minizinc} +\begin{mzn} [ xi * 2 | xi in x where x mod 2 == 0] -\end{minizinc} +\end{mzn} The evaluated expression will be added to the new array. This means that the type of the array will primarily depend on the type of the expression. However, in recent versions of \minizinc\ both the collections over which we iterate and the filtering condition could have a \gls{variable} type. Since we then cannot -decise during flattening if an element is present in the array, the elements -will be made of an \gls{optional} type. This means that the solver still will +decide during flattening if an element is present in the array, the elements +will be made of a \gls{optional} type. This means that the solver still will decide if the element is present in the array or if it takes a special ``absent'' value (\mzninline{<>}). @@ -358,8 +427,8 @@ provide a list of definitions, flattened in order, that can be used in its resulting definition. There are three main purposes for \glspl{let}: \begin{enumerate} - \item To name an intermediate expression so it can be used multiple times (or - to simplify the expression). For example, the constraint + \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; @@ -390,13 +459,14 @@ resulting definition. There are three main purposes for \glspl{let}: multiplication constraint \mzninline{pred_int_times}. \end{enumerate} -An important detail in flattening \glspl{let} is that any variables that are -introduced might need to be renamed in the resulting solver level model. -Different from top-level definitions, the variables declared in \glspl{let} can -be flattened multiple times when used in loops, function definitions (that are -called multiple times), and \gls{array} \glspl{comprehension}. In these cases the -flattener must assign any variables in the \gls{let} a new name and use this -name in any subsequent definitions and in the resulting expression. +An important detail in flattening \glspl{let} is that any \glspl{variable} that +are introduced might need to be renamed in the resulting solver level model. +Different from top-level definitions, the \glspl{variable} declared in +\glspl{let} can be flattened multiple times when used in loops, function +definitions (that are called multiple times), and \gls{array} +\glspl{comprehension}. In these cases the flattener must assign any +\glspl{variable} in the \gls{let} a new name and use this name in any subsequent +definitions and in the resulting expression. \subsection{Handling Undefined Expressions}% \label{subsec:back-mzn-partial} @@ -408,7 +478,7 @@ Examples of such expressions in \minizinc\ are: \item Division (or modulus) when the divisor is zero: \\ \mzninline{x div 0 = @??@} - \item Array access when the index is outside of the given index set: \\ + \item Array access when the index is outside the given index set: \\ \mzninline{array1d(1..3, [1,2,3])[0] = @??@} \item Finding the minimum or maximum or an empty set: \\ \mzninline{min({}) @@ -419,7 +489,7 @@ Examples of such expressions in \minizinc\ are: \end{itemize} -The existence of undefined expressions can cause confusion in \cmls. There is +The existence of undefined expressions can cause confusion in \cmls{}. There is both the question of what happens when an undefined expression is evaluated and at what point during the process undefined values will be resolved, during flattening or at solving time. diff --git a/chapters/A1_minizinc_grammar.tex b/chapters/A1_minizinc_grammar.tex index 19903d3..9a52e12 100644 --- a/chapters/A1_minizinc_grammar.tex +++ b/chapters/A1_minizinc_grammar.tex @@ -8,7 +8,7 @@ modelling language throughout this thesis. This chapter offers a formal specification of the grammar of the current version \minizinc\ language, corresponding with \minizinc\ version 2.5.3. -For the convinience of the reader the grammar has been split into several parts. +For the convenience of the reader the grammar has been split into several parts. \Cref{sec:mzn-grammar-items} shows the syntax for the top-level structure of a model. \Cref{sec:mzn-grammar-typeinst} shows the syntax of type expressions, used for variable declarations and return types of variables.