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

Add more about the MiniZinc structure

Browse Source
This commit is contained in:
Jip J. Dekker 2021-04-26 16:41:38 +10:00
parent d320377c3a
commit 87ff8426f3
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
3 changed files with 146 additions and 76 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
assets/glossary.tex
View File

@ -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={},

210
chapters/2_background.tex
View File

@ -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.

2
chapters/A1_minizinc_grammar.tex
View File

@ -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.