Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
This repository has been archived on 2025-03-06. You can view files and clone it, but cannot push or open issues or pull requests.
dekker-phd-thesis/chapters/2_background.tex

1908 lines
91 KiB
TeX
Raw Blame History

%************************************************
\chapter{Background}\label{ch:background}
%************************************************
\input{chapters/2_background_preamble}
\jip{TODO:\ Mention something about LCG.}
\begin{example}%
\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
space left in the car, so we cannot bring all the toys. Since Audrey gets
enjoys playing with some toys more than others, we can now try and pick the
toys that bring Audrey the most amount of joy, but still fit in the car. The
following set of equations describe this knapsack problem as a \gls{cop}:
\begin{equation*}
\text{maximise}~z~\text{subject to}~
\begin{cases}
S \subseteq T \\
z = \sum_{i \in S} joy(i) \\
\sum_{i \in S} space(i) < C \\
\end{cases}
\end{equation*}
In these equations \(S\) is set \variable{}. It contains the selection of
toys that will be packed for the trip. \(z\) is the objective \variable{}
that is maximised to find the optimal selections of toys to pack. The
\parameter{} \(T\) is the set of all the toys. The \(joy\) and \(space\)
functions are \parameters{} used to map toys, \( t \in T\), to a value
depicting the amount of enjoyment and space required respectively. Finally,
the \parameter{} \(C\) is that depicts the total space that is left in the
car before packing the toys.
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 \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}
\begin{listing}
\pyfile{assets/py/2_dyn_knapsack.py}
\caption{\label{lst:2-dyn-knapsack} A Python program that solves a 0-1 knapsack
problem using dynamic programming}
\end{listing}
In the remainder of this chapter we will first, in \cref{sec:back-minizinc} we
introduce \minizinc\ as the leading \cml\ used within this thesis. In
\cref{sec:back-solving} we discuss how \gls{cp} can be used to solve a
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 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}
\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.
\begin{listing}
\mznfile{assets/mzn/back_knapsack.mzn}
\caption{\label{lst:back-mzn-knapsack} A \minizinc\ model describing a 0-1
knapsack problem}
\end{listing}
\begin{example}%
\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
\cref{lst:back-mzn-knapsack}.
The model starts with the declaration of the \parameters{}.
\Lref{line:back:knap:toys} declares an enumerated type that represents all
possible toys, \(T\) in the mathematical model in the example.
\Lrefrange{line:back:knap:joy}{line:back:knap:space} declare arrays mapping
from toys to integer values, these represent the functional mappings \(joy\)
and \(space\). Finally, \lref{line:back:knap:left} declares an integer
\parameter{} to represent the car capacity as an equivalent to \(C\).
The model then declares its \variables{}. \Lref{line:back:knap:sel} declares
the main \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.
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}.
\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 \parameters{}, a \minizinc\ model is
translated (via a process called \emph{flattening}) into a set of \variables{}
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;
\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;
\end{mzn}
This \emph{flat} problem will be passed to some \solver{}, which will attempt to
determine an assignment to each \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 \variables{} and input \parameters{},
\constraints{}, 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 Marriott 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\)@;} or
\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.
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 \parameters{} and as \variables{}. 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 \variables{} might be declared as
\begin{mzn}
array[5..10] of var bool: bs;
\end{mzn}
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 \variable{}. In \minizinc\ any expression
that has a set type can be used as a type expression. For example, the following
two declarations declare two integer \variables{} that can take the values from
three to five and one, three, and five respectively.
\begin{mzn}
var 3..5: x;
var {1,3,5}: y;
\end{mzn}
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
\constraint{} on the expression, forcing the result of the expression to take a
value according to the type expression.
\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 \variables{}
that satisfies the constraints, \mzninline{solve satisfy;}, to find an
assignment to the \variables{} that satisfies the constraints and minimises the
value of a \variable{}, \mzninline{solve minimize x;}, or similarly maximises
the value of a \variable{}, \mzninline{solve maximize x;}. If the model does not
contain a goal item, then it then the problem is assumed to be a satisfaction
problem.
\jip{TODO:\@ add some information about search in \minizinc{}. It's probably
pretty relevant.}
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 \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
\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 a function is
directly placed in the flattened model.
\subsection{MiniZinc Expressions}%
\label{subsec:back-mzn-expr}
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
\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}.
\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
\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,
);
\end{mzn}
This \gls{global} expresses the knapsack relationship, where the \parameters{}
\mzninline{w} are the weights of the items, \mzninline{p} are the profit for
each item, the \variables{} in \mzninline{x} represent the amount of time the
items are present in the knapsack, and \mzninline{W} and \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}:
\begin{mzn}
constraint knapsack(toy_space, toy_joy, set2bool(selection), total_joy, space);
\end{mzn}
The usage of this \gls{global} has the additional benefit that the knapsack
structure of the problem is then known to the \solver{} which might implement
special handling of the relationship.
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 a shorthand for \minizinc\
functions that can be used to transform or combine other expressions. For
example the constraint
\begin{mzn}
constraint not (a + b < c);
\end{mzn}
contains the infix \glspl{operator} \mzninline{+} and \mzninline{<}, and the
prefix \gls{operator} \mzninline{not}.
These \glspl{operator} will be evaluated using the addition, less-than
comparison, and Boolean negation functions respectively. Although the
\gls{operator} syntax for \variables{} and \parameters{} is the same, different
(overloaded) versions of these functions will be used during flattening. For
\parameters{} types the result of the function can be directly computed, but
when flattening these functions with \variables{} types a new \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 a >= 0 then a > b else b < a endif;
\end{mzn}
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
used to, for example, define an absolute value function for integer
\parameter{}:
\begin{mzn}
function int: abs(int: a) =
if a >= 0 then a else -a endif;
\end{mzn}
When the condition does not contain any \variables{}, 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 \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 and a constraint to
enforce the functional relationship. In \minizinc\ special
\mzninline{if_then_else} \glspl{global} are available to implement this
relationship.
For the selection of an element from an \gls{array}, instead of between
different expressions, the \minizinc\ language uses an \gls{array} access syntax
similar to most other languages. The expression \mzninline{a[i]} selects the
element with index \mzninline{i} from the array \mzninline{a}. Note this is not
necessarily the \(\mzninline{i}^{\text{th}}\) element because \minizinc\ allows
modellers to provide a custom index set.
Like the previous expressions, the selector \mzninline{i} can be both a
\parameter{} or a \variable{}. If the expression is a \gls{variable}, then the
expression is flattened to be an \mzninline{element} function. Otherwise, the
flattening will replace the \gls{array} access expression by the element
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{}.
\Gls{generator} expressions, \mzninline{[E | G where F]}, consist of three
parts:
\begin{description}
\item[\mzninline{G}] The generator expression which assigns the values of
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
when the filtering condition succeeds.
\end{description}
The following example composes an \gls{array} that contains the tripled even
values of an \gls{array} \mzninline{x}.
\begin{mzn}
[ xi * 3 | xi in x where x mod 2 == 0]
\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 \variable{} type. Since we then cannot
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{<>}).
Finally, \glspl{let} are the primary scoping mechanism in the \minizinc\
language, together with function definitions. A \gls{let} allows a modeller to
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
%
\begin{mzn}
constraint let { var int: tmp = x div 2; } in tmp mod 2 == 0 \/ tmp = 1;
\end{mzn}
%
constrains that half of \mzninline{x} is even or one.
\item To introduce a scoped \variable{}. For example, the constraint
%
\begin{mzn}
constraint let {var -2..2: slack;} in x + slack = y;
\end{mzn}
%
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}
%
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 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.
\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 \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:
\begin{mzn}
array[1..10] of var 1..15: x;
constraint all_different(x);
solve maximize sum(i in 1..10) (x[i] mod 2 == 0);
\end{mzn}
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 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
reified variables it can set to \mzninline{true}.
\end{example}
When an expression occurs in a position where it can be globally enforced, we
say it occurs in \emph{root context}. Contrarily, an expression that occurs in a
\emph{non-root context} will be reified during the flattening process. In
\minizinc{}, almost all expressions can be used in both contexts.
\subsection{Handling Undefined Expressions}%
\label{subsec:back-mzn-partial}
Some expressions in the \cmls\ do not always have a well-defined result. Part of
the semantics of a \cmls{} is the choice as to how to treat these partial
functions.
\begin{example}\label{ex:back-undef}
Consider, for example, the following ``complex constraint''
\begin{mzn}
constraint i <= 4 -> a[i] * x >= 6;
\end{mzn}
which requires that if \mzninline{i} takes a value less or equal to four, then
the value in the \texttt{i}\(^{th}\) position of array \mzninline{a}
multiplied by \mzninline{x} must be at least 6.
Suppose the array \texttt{a} has index set \mzninline{1..5}, but \texttt{i}
takes the value \texttt{7}. The constraint \mzninline{element(i, a, t1)} will
fail and no solution will be found. However, intuitively if \mzninline{i = 7}
the constraint should be trivially true.
\end{example}
Other examples of \minizinc{} expressions that result in partial functions are:
\begin{itemize}
\item Division (or modulus) when the divisor is zero:
\begin{mzn}
x div 0 = @??@
\end{mzn}
\item Finding the minimum or maximum or an empty set:
\begin{mzn}
min({}) = @??@
\end{mzn}
\item Computing the square root of a negative value:
\begin{mzn}
sqrt(-1) = @??@
\end{mzn}
\end{itemize}
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.
Frisch and Stuckey define three semantic models to deal with the undefinedness
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.
\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.
\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}.
\end{description}
In practice, it is often natural to guard against undefined behaviour using
Boolean logic. Relational semantics therefore often feel the most natural for
the users of constraint modelling languages. This is why the \minizinc\ uses
relational semantics during its evaluation.
For example, one might deal with a zero divisor using a disjunction:
\begin{mzn}
constraint d == 0 \/ a div d < 3;
\end{mzn}
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.
Frisch and Stuckey also show that different \solvers{} often employ different
semantics \autocite*{frisch-2009-undefinedness}. It is therefore important that,
during the flattening process, any potentially undefined expression gets
replaced by an equivalent model that is still valid under a strict semantic.
Essentially eliminating the existence of undefined expressions in the \solver{}
model.
\section{Solving Constraint Models}%
\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
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{}.
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
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 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
\gls{cp} \solvers{} to solve a \constraint{} model.
Throughout the years \minizinc\ has seen the addition of solvers using other
approaches to finding solutions to \constraint{} models. Although these
\solvers{} bring new classes of problems that can be solved using \minizinc{},
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 by \minizinc\ \solver{}
targets and their input language.
\subsection{Constraint Programming}%
\label{subsec:back-cp}
\glsreset{cp}
When given a \gls{csp}, one might wonder what the best way is to find a solution
to the problem. The simplest solution would be to apply ``brute force'': try
every value in the \gls{domain} of 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;
\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 of solving \glspl{csp} by
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 to eliminate any
impossible value using a process called \gls{propagation}. For each
\constraint{} the \solver{} has a chosen algorithm called a \gls{propagator}.
Triggered by changes in the \glspl{domain} of its \variables{}, the
\gls{propagator} will analyse and prune any values that are proven to be
inconsistent.
In the best case scenario, \gls{propagation} will eliminate all impossible
values and all \variables{} have been fixed to a single value. In this case we
have arrived at a solution. Often, \gls{propagation} alone will not be enough to
find a solution to the problem. Instead, when no more \glspl{propagator} are
triggered (we have reached a \gls{fixpoint}), the \solver{} has to make a search
decision. It will fix a \variable{} to a value or add a new \constraint{}. This
search decision is an assumption made by the \solver{} in the hope of finding a
solution. If no solution is found using the search decision, then it needs to
try making the opposite decision: excluding the chosen value or adding the
opposite constraint.
Note that the important difference between values excluded by \gls{propagation}
and making search decisions is that value excluded by a \gls{propagator} are
guaranteed to not occur in any solution, but values excluded by a search
heuristic are merely removed locally and might still be part of a solution. A
\gls{cp} \solver{} is 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 \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
that is made during propagation (after the first search decision), the reverse
change is stored on in a list. Whenever a new search decision is made, the
current position of the list is tagged. If the \solver{} now needs to undo a
search decision (\ie\ \gls{backtrack}), it can apply all changes until it reaches
the change that is tagged with the search decision. Because all changes before
the tagged point on the \gls{trail} were made before the search decision was
made, it is guaranteed that these \gls{domain} changes do not depend on the
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 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.
\begin{mzn}
int: n;
set of int: ROW = 1..n;
set of int: COL = 1..n;
array [ROW] of var COL: q;
constraint all_different(q);
constraint all_different([q[i] + i | i in ROW]);
constraint all_different([q[i] - i | i in ROW]);
\end{mzn}
Since we know that there can only be one queen per row, the decision in the
model left to make is, for every queen, where in the row 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 first search decision.
\Cref{fig:back-nqueens} visualises the domain propagation of placing a queen
on the d3 square of an eight by eight chess board. When the queen it placed
on the board in \cref{sfig:back-nqueens-1}, it fixes the value of row 4 to
the value 3. This implicitly eliminates any possibility of placing another
queen in the row. Now that one queen is placed on the board the propagators
for the \mzninline{all_different} constraints can start propagating. As show
in \cref{sfig:back-nqueens-2}, the first \mzninline{all_different} constraint
can now stop other queens to be placed in the same column. It eliminates the
value 3 from the domains of the queens in the remaining rows. Similarly, the
other \mzninline{all_different} constraints remove all values that correspond
to positions on the same diagonal as the placed queen, shown in
\cref{sfig:back-nqueens-3,sfig:back-nqueens-4}.
The propagation of the first placed queen severely limits the positions where
a second queen can be placed.
\end{example}
\begin{figure}
\centering
\begin{subfigure}[b]{.48\columnwidth}
\centering
\chessboard[
setwhite={Qd3},
pgfstyle=cross,
color=red,
markarea={d1-d2,d4-d8},
]
\caption{\label{sfig:back-nqueens-1} Assign a queen to d3}
\end{subfigure}%
\hspace{0.04\columnwidth}%
\begin{subfigure}[b]{.48\columnwidth}
\centering
\chessboard[
setwhite={Qd3},
pgfstyle=cross,
color=red!35!white,
markareas={d1-d2,d4-d8},
pgfstyle=cross,
color=red,
markareas={a3-c3,e3-h3},
]
\caption{\label{sfig:back-nqueens-2} Propagate rows}
\end{subfigure}
\begin{subfigure}[b]{.48\columnwidth}
\centering
\chessboard[
setwhite={Qd3},
pgfstyle=cross,
color=red!35!white,
markareas={d1-d2,d4-d8,a3-c3,e3-h3},
pgfstyle=cross,
color=red,
markareas={b1-b1,c2-c2,e4-e4,f5-f5,g6-g6,h7-h7},
]
\caption{\label{sfig:back-nqueens-3} Propagate upwards diagonal}
\end{subfigure}%
\hspace{0.04\columnwidth}%
\begin{subfigure}[b]{.48\columnwidth}
\centering
\chessboard[
setwhite={Qd3},
pgfstyle=cross,
color=red!35!white,
markareas={d1-d2,d4-d8,a3-c3,e3-h3,b1-b1,c2-c2,e4-e4,f5-f5,g6-g6,h7-h7},
pgfstyle=cross,
color=red,
markareas={a6-a6,b5-b5,c4-c4,e2-e2,f1-f1},
]
\caption{\label{sfig:back-nqueens-4} Propagate downward diagonal}
\end{subfigure}
\caption{\label{fig:back-nqueens} An example of domain propagation when a
queen gets assigned in the N-Queens problem.}
\end{figure}
In \gls{cp} solving there is a trade-off between the amount of time spend
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, not 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 because the problem is
\gls{np}-hard \autocite{choi-2006-fin-cons}. 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 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}
that enforces all solutions to have a better \gls{objective} value than the
incumbent solution. If the search process finds another solution, then the
incumbent solution is updated and the search process continues. If the search
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}, \gls{gecode} \autocite{gecode-2021-gecode}, and
OR-Tools \autocite{perron-2021-ortools} have long been one of the leading
methods to solve \minizinc\ instances.
\subsection{Mathematical Programming}%
\label{subsec:back-mip}
\glsreset{lp}
\glsreset{mip}
One of the oldest techniques to solve optimisation problems is the use of
\gls{lp} \autocite{schrijver-1998-mip}. A linear program describes a problem
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{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}
\end{align*}
%
\noindent{}where \(V\) and \(C\) represent the number of variables and number of
constraints respectively. The vector \(c\) holds the coefficients of the
objective function and the matrix \(a\) holds the coefficients for the
constraints. The vectors \(l\) and \(u\) respectively contain the lower and
upper bounds of the constraints. Finally, the \variables{} of the linear program
held in the \(x\) vector.
For problems that are in the form of a linear program, there are proven methods
to find the optimal solution. In 1947 Dantzig introduced the simplex method,
that can find the optimal solution of a linear program in worst-case exponential
time. It was questioned whether the same problem could be solved in worst-case
polynomial time, until Khachiyan proved this possible when he introduced the
first of the so-called \emph{interior point} methods.
These methods provide the foundation for a harder problem. In \gls{lp} our
variables must be continuous. If we require that one or more take a discrete
value (\(x_{i} \in \mathbb{N}\)), then the problem suddenly becomes much harder.
The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all}
\variables{} must take a discrete value).
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 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
program where it is less or equal to the value in the solution rounded down to
the nearest discrete value and a version where it is greater or equal to the
value in the solution rounded up. Both versions are solved to find the best
solution. The process is repeated recursively until a discrete solution is
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 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.
Over the years \gls{lp} and \gls{mip} \solvers{} have developed immensely.
\solvers{}, such as \gls{cbc} \autocite{forrest-2020-cbc}, \gls{cplex}
\autocite{cplex-2020-cplex}, \gls{gurobi} \autocite{gurobi-2021-gurobi}, and \gls{scip}
\autocite{gamrath-2020-scip}, can solve many complex problems. It is therefore
often worthwhile to encode problem as a mixed integer program to find a
solution.
To solve a \gls{csp}, it can be encoded as a mixed integer program.
This process is known as linearisation.
It does, however, come with its challenges.
Most \constraints{} in a \minizinc\ model are not linear equations.
The translation of a single \constraint{} can introduce many linear \constraints{} and even new \variables{}.
For example, when a \constraint{} reasons about the value that a variable will take, to encode it we will need to introduce \glspl{indicator-var}.
The \glspl{indicator-var} \(y_{i}\) for a \variable{} \(x\) take the value 1 if \(x = i\) and 0 otherwise.
\constraints{} reasoning about the value of \(x\) can then be rewritten as 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 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}
\end{align}
The encoding of this variable uses only integers.
Like the \gls{cp} model, integer \variables{} \(q\) are used to represent where the queen is located in each column.
To encode the \mzninline{all_different} constraints, the \glspl{indicator-var} \(y\) are inserted to reason about the value of \(q\).
The \cref{line:back-mip-channel} is used to connect the \(q\) and \(y\) \variables{} and make sure that their values correspond.
\Cref{line:back-mip-row} ensures that only one queen is placed in the same column.
Finally, \cref{line:back-mip-diag1,line:back-mip-diag2} constrain all diagonals to contain only one queen.
\end{example}
\subsection{Boolean Satisfiability}%
\label{subsec:back-sat}
\glsreset{sat}
\glsreset{maxsat}
\gls{sat} was the first problem to be proven to be \gls{np}-complete
\autocite{cook-1971-sat}. The problem asks if there is an assignment for the
variables of a given Boolean formula, such that the formula is satisfied. This
problem can be seen as a restriction of the general \gls{csp} where \variables{}
can only be of a Boolean type.
There is a field of research dedicated to solving \gls{sat} problems
\autocite{biere-2021-sat}. In this field a \gls{sat} problem is generally
standardised to be in \gls{cnf}. A \gls{cnf} is formulated in terms of Boolean
literals. These are variables \(x\) or their negations \(\neg x\). These
literals are then used in a conjunction of disjunctive clauses: a Boolean
formula in the form \(\forall_{i \in P} \exists_{b \in C_{i}} b\). To solve the
\gls{sat} problem, the \solver{} has to find an assignment for the \variables{}
where at least one literal is true in every clause.
Even though the problem is proven to be hard to solve, a lot of progress has
been made towards solving even the biggest the most complex \gls{sat} problems.
Modern day \gls{sat} solvers, like Kissat \autocite{biere-2021-kissat} and Clasp
\autocite{gebser-2012-clasp}, can solve 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 on the problem, using a
\gls{sat} \solvers{} to solve the encoded problem can still be the most
efficient way to solve the problem.
\begin{example}
Let us once more consider the N-Queens problem presented in
\cref{ex:back-nqueens}. A possible \gls{sat} encoding for this problem is the
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)}
\end{align}
The encoding of the problem uses a Boolean \variable{} for every position of
the chess board. Each \variable{} represents if a queen will be located on
this position or not. \Cref{line:back-sat-at-least} forces that a queen is
placed on every row of the chess board.
\Cref{line:back-sat-row,line:back-sat-col} ensure that only one queens is
place in each row and column respectively.
\Cref{line:back-sat-diag1,line:back-sat-diag2} similarly constrain each
diagonal to contain only one queen.
\end{example}
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,
the more important the clause is for the overall problem. The goal in the
\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 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.
\section{Other Constraint Modelling Languages}%
\label{sec:back-other-languages}
Although \minizinc\ is the \cml\ that is the primary focus of this thesis, there
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 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 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}
\glsreset{ampl}
One of the most used \cmls\ is \gls{ampl} \autocite{fourer-2003-ampl}. As the
name suggest, \gls{ampl} was designed to allow modellers to express problems
through the use of mathematical equations. It is therefore also described as an
``algebraic modelling language''. Specifically \gls{ampl} was designed to model
linear programs. These days \gls{ampl} has been extended to allow more advanced
\solver{} usage. Depending on the \gls{solver} targeted by \gls{ampl}, the
language can give the modeller access to additional functionality. For
\solvers{} that have a \gls{mip} solving method, the modellers can require
\variables{} to be integers. Different types of \solvers{} can also have access
to different types of constraints, such as quadratic and non-linear constraints.
\gls{ampl} has even been extended to allow the usage of certain \glspl{global}
when using a \gls{cp} \solver{} \autocite{fourer-2002-amplcp}.
\begin{example}
If we consider the well-known \gls{tsp}, then we might model this problem in
\gls{ampl} as follows:
\begin{plain}
set Cities ordered;
set Paths := {i in Cities, j in Cities: ord(i) < ord(j)};
param cost {Paths} >= 0;
var Take {Paths} binary;
param n := card {Cities};
set SubSets := 0 .. (2**n - 1);
set PowerSet {k in SubSets} := {i in Cities: (k div 2**(ord(i)-1)) mod 2 = 1};
minimize TotalCost: sum {(i,j) in Paths} cost[i,j] * Take[i,j];
subj to Tour {i in S}:
sum {(i,j) in Paths} Take[i,j] + sum {(j,i) in Paths} Take[j,i] = 2;
subj to SubtourElimation {k in SubSet diff {0,2**n-1}}:
sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (i,j) in Paths} X[i,j] +
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:
\parameter{} declarations, \variable{} declarations, \constraints{}, and a
solving goal.
The same problem can be modelled in \minizinc\ as follows:
\begin{mzn}
enum CITIES;
array[CITIES, CITIES] of int: cost;
array[CITIES] of var CITIES: next;
constraint circuit(next);
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 \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 \constraint{} models. It is the job of the \solver{}'s
\minizinc\ library to transform the high-level constraints into compatible
\solver{}-level \constraints{}.
\end{example}
\subsection{OPL}%
\label{sub:back-opl}
\glsreset{opl}
\gls{opl} is a \cml\ that has a focus aims to combine the strengths of
mathematical programming languages like \gls{ampl} with the strengths of
\gls{cp} \autocite{van-hentenryck-1999-opl}. The syntax of \gls{opl} is very
similar to the \minizinc\ syntax.
Where the \gls{opl} really shines is when modelling scheduling problems.
Resources and activities are separate objects in the \gls{opl}. This allows
users express resource scheduling \constraints{} in an incremental and more
natural fashion. When solving a scheduling problem, the \gls{opl} makes use of
specialised \gls{interval} \variables{}, which represent when a task will be
scheduled.
\begin{example}
For example the \variable{} declarations and \constraints{}
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];
Activity task[j in Jobs, t in Tasks] (duration[j,t]);
Activity makespan;
UnaryResource tool[Machines];
minimize makespan.end
subject to {
forall (j in Jobs)
task[j,nbTasks] precedes makespan;
forall (j in Jobs)
forall (t in 1..nbTasks-1)
task[j, t] precedes task[j, t+1];
forall (j in Jobs)
forall (t in Tasks)
task[j, t] requires tool[resource[j, t]];
};
\end{plain}
The equivalent declarations and \constraints{} would look like this in
\minizinc{}:
\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, t in 1..nbTasks-1) (
start[j,t] + duration[j,t] <= start[j,t+1]
);
constraint forall(j in Jobs) (
start[j, nbTasks] + duration[j, nbTasks] <= makespan
);
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],
)
);
solve minimize makespan;
\end{mzn}
Note that the \minizinc{} model does not have explicit Activity variables. It
must instead use \variables{} that represent the start times of the activity
and a \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 \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
allows the modellers full programmatic control over how the solver will explore
the search space depending on the current state of the variables. This offers to
modeller more control over the search in comparison to the
\gls{search-heuristic} \glspl{annotation} in \minizinc{}, which only allow
modellers to select predefined \glspl{search-heuristic} already implemented in
the solver. Take, for example, the following \gls{opl} search definition:
\begin{plain}
search {
try x < y | y >= x endtry;
}
\end{plain}
This search strategy will ensure that we first try and find a solution where the
\variable{} \mzninline{x} takes a value smaller than \mzninline{y}, if it does
not find a solution, then it will try finding a solution where the opposite is
true. This search specification, like many others imaginable, cannot be enforced
using \minizinc\ \gls{search-heuristic} \glspl{annotation}.
To support \gls{opl}'s dedicated search language, the language is tightly
integrated with its dedicated \solvers{}. Its search syntax requires that the
\gls{opl} process can directly interact with the \solver{}'s internal search
mechanism and that the \solver{} reasons about search on the same level as the
\gls{opl} model. It is therefore not possible to connect other \solvers{} to
\gls{opl}.
\subsection{Essence}%
\label{sub:back-essence}
\gls{essence} \autocite{frisch-2007-essence} is another high-level \cml\ is
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-integer types,
\item finite multi-sets of any type,
\item finite (partial) functions,
\item and (regular) partitions of finite types.
\end{itemize}
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 sets of sets of integers. Partitions can be defined for
finite types. The base types in \gls{essence} are restricted to Boolean,
enumerated types, or a restricted set of integers.
\begin{example}
Consider, for example, the Social Golfers Problem, can be modelled in
\gls{essence} as follows:
\begin{plain}
language Essence 1.3
given w, g, s : int(1..)
letting Golfers be new type of size g * s
find sched : set (size w) of
partition (regular, numParts g, partSize s) from Golfers
such that
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:
\begin{mzn}
include "globals.mzn";
int: g;
int: w;
int: 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;
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 (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 \constraints{}
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.
\end{example}
The high-level variables available in \gls{essence} are often not directly
supported by the \solvers{} that is employed to solve \gls{essence} instances.
To solve the problem, not only do the \constraints{} have to be translated to
\constraints{} supported by the solver, but also all \variables{} have to be
translated to a combination of \constraints{} and \variables{} compatible with
the targeted solver.
\section{Term Rewriting}%
\label{sec:back-term}
\glsreset{trs}
At the heart of the flattening process, the process as described in
\cref{sec:back-minizinc} that translates a \minizinc{} instance into solver
level \flatzinc{}, lies a \gls{trs}. A \gls{trs} describes a computational model
the full 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}\)
\autocite{baader-1998-term-rewriting}. A \gls{term} is an expression with nested
sub-expressions consisting of \emph{function} and \emph{constant} symbols. An
example of a term is \(F(0 + 1,F(1,0))\), where \(F\) and \(+\) are function
symbols and \(0\) and \(1\) are constant symbols. In a term rewriting rule, a
term can also contain a \emph{term variable} which captures a term
sub-expression.
\begin{example}
Consider the following \gls{trs} consists of some (well-known) rules to
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
\end{align*}
From these rules it follows that
\[ 1 \land 1 \land 0 \rightarrow^{r_{1}} 1 \land 0 \rightarrow^{r_{3}} 0 \land 1 \rightarrow^{r_{2}} 0 \]
Notice that there can be a choice between different rules. In general, a
\gls{trs} can be non-deterministic. We could also have applied the \(r_{1}\)
twice and arrived at the same result.
\end{example}
Two properties of a \gls{trs} that are often studied are \gls{termination} and
\gls{confluence}. A \gls{trs} is said to be terminating if, no-matter what order
the term rewriting rules are applied, you always arrive at a \gls{normal-form}
(\ie, a term where no more rules apply). A \gls{trs} is confluent if, no-matter
what order the term rewriting rules are applied, you always arrive at the same
\gls{normal-form} (if you arrive at a \gls{normal-form}).
It is trivial to see that our previous example is non-terminating, since you can
repeat rule \(r_{3}\) an infinite amount of times. The system, however, is
confluent as, if it arrives at the same \gls{normal-form}: if the term contains
any \(0\), then the result will be \(0\); otherwise, the result will be \(1\).
These properties are also interesting when in the translation process of a
\minizinc{} instance into \flatzinc{}. The confluence of the translation process
will ensure that the same \flatzinc{} is produced independently of the order in
which the \minizinc\ model is processed. This is a desirable quality as it makes
the behaviour of the translation process more predictable.
Many of the techniques used by \solvers{} targeted by \minizinc\ are proven to
be complete. Meaning that they are guaranteed to find a (best) solution to the
problem or prove that there is none. For this quality to hold for the \minizinc\
solving process, it has to be guaranteed that the \minizinc\ translation process
terminates (so the solving process can start).
In the remainder of this section we will discuss two types of \glspl{trs} that
are closely related to \cmls\ and their compilation into solver level constraint
models: \gls{clp} and \gls{chr}.
\subsection{Constraint Logic Programming}%
\label{subsec:back-clp}
\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
level constraint model is eventually rewritten into a solver level constraints
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
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 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
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} \constraint{} that can be used to
find the optimal value for a variable.
The evaluation of a constraint logic program rewrites the list of constraints,
called the goal, in the order given by the programmer. The rewriting of the
constraint predicates is tried in the order in which the different rewriting
rules for the constraint predicates are defined. The process is completed when
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 way you can
find all possible correct ways to rewrite the program.
To implement this mechanism there is a tight integration between the \solver{},
referred to as the \gls{constraint-store}, and the evaluator of the constraint
logic program. In addition to just adding \constraints{}, the program can also
inspect the status of the constraint and retract constraints from the constraint
store. This allows the program to detect when the constraint store has become
inconsistent and then \gls{backtrack} the constraint store to the last decision
(\ie\ restore the \gls{constraint-store} to its state before the last decision
was made) and try the next rewriting rule.
The strength of the \gls{constraint-store} can influence the correctness of a
constraint logic program. Some \solvers{} are incomplete; it is unable to tell
if some of its \constraints{} are satisfied or not. This, for example, happens
with \solvers{} that work with integer \glspl{domain}. In these cases the
programmer must use the \mzninline{labeling} constraint to force constant values
for the variables. Once the variables have been assigned constant values, the
solver will be able to decide if the constraints are satisfied.
\subsection{Constraint Handling Rules}%
\label{sub:back-chr}
\glsreset{chr}
When \constraints{} are seen as terms in a \gls{trs}, then it is not just
possible to define rules to rewrite constraints to the level of a \solver{}. It
is also possible to define rules to simplify, propagate, and derive new
constraints within the solver. \gls{chr} follow from this idea. \gls{chr} are a
language extension (targeted at \gls{clp}) to allow user-defined constraints
within a \solver{}. \constraints{} defined using \gls{chr} are rewritten into
simpler constraints until they are solved.
Different from \gls{clp}, \gls{chr} allows term rewriting rules that are
multi-headed. This means that, for some rules, multiple terms must match, to
apply the rule.
\begin{example}
Consider the following user-defined constraint for logical implication using
\gls{chr}.
\begin{plain}
reflexivity @ X -> Y <=> X = Y | true
anti-symmetry @ X -> Y, Y -> X <=> X = Y
transitivity @ X -> Y, Y -> Z ==> X -> Z
\end{plain}
These definitions specify how \texttt{->} simplifies and propagates as a
constraint. The rules follow the mathematical concepts of reflexivity,
anti-symmetry, and transitivity.
\begin{itemize}
\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{} 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{} 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
another constraint \texttt{X -> Z}. Different from the other rules, no
constraints are removed.
\end{itemize}
Note that the use of multi-headed rewriting rules is essential to define these
rules.
\end{example}
The rules in a \gls{chr} system can be categorised into three different
categories: simplification, propagation, and simpagation. The first two rules in
the previous example are simplification rules: they replace some constraint
atoms by others. The 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 simplification and propagation rules, it is possible to
formulate all rules as simpagation rules.
\subsection{ACD Term Rewriting}%
\label{subsec:back-acd}
\section{Compiling \glsentrytext{minizinc}}%
\label{sec:back-mzn-interpreter}
\jip{This section is the only one here that is not really literature review.
Maybe this should just be a separate chapter. It is ``new'' in the sense that
is the first real description of some parts of the compiler, but it is
relatively short.}
Traditionally the compilation process is split into three sequential parts: the
\emph{frontend}, the \emph{middle-end}, and the \emph{backend}. It is the job of
the frontend to parse the user input, report on any errors or inconsistencies in
the input, and transform it into an internal representation. The middle-end
performs the main translation in a target-independent fashion. It converts the
internal representation at the level of the compiler frontend to another
internal representation as close to the level required by the compilation
targets. The final transformation to the format required by the compilation
target are performed by the backend. When a compiler is separated into these few
steps, then adding support for new language or compilation target only require
the addition of a frontend or backend respectively.
The \minizinc\ compilation process categorised in the same three categories, as
shown in \cref{fig:back-mzn-comp}. In the frontend, a \minizinc\ model is first
parsed together with its data into an \gls{ast}. The process will then analyse
the \gls{ast} to discover the types of all expressions used in the instance. If
an inconsistency is discovered, then an error is reported to the user. Finally,
the frontend will also preprocess the \gls{ast}. This process is used to rewrite
expressions into a common form for the middle-end, \eg\ remove the ``syntactic''
sugar. For instance, replacing the usage of enumerated types by normal integers.
\begin{figure}
\centering
\includegraphics[width=\linewidth]{assets/img/back_compilation_structure}
\caption{\label{fig:back-mzn-comp} The compilation structure of the \minizinc\
compiler.}
\end{figure}
The middle-end contains the most important two processes: the flattening and the
optimisation. During the flattening process the high-level (\minizinc{})
constraint model is rewritten into a solver level (\flatzinc{}) constraint
model. It could be noted that the flattening step depends on the compilation
target to define its solver level constraints. Even though the information
required for this step is target dependent, we consider it part of the
middle-end as the mechanism is the same for all compilation targets. A full
description of this process will follow in \cref{subsec:back-flattening}. Once a
solver level constraint model is constructed, the \minizinc\ compiler will try
to optimise this model: shrink domains of variables, remove constraints that are
proven to hold, and remove variables that have become unused. These optimisation
techniques are discussed in \cref{subsec:back-fzn-optimisation}.
The backend will convert the internal solver level constraint model into a
format that can be used by the targeted \solver{}. Given the formatted artefact,
a solver process, controlled by the backend, can then be started. Whenever the
solver process produces a solution, the backend will reconstruct the solution to
the specification of the original \minizinc{} model.
In this section we will discuss the flattening and optimisation process as
employed by the 2.5.5 version of \minizinc{} \autocite{minizinc-2021-minizinc}.
\subsection{Flattening}%
\label{subsec:back-flattening}
The goal of the flattening process is to arrive at a ``flat'' constraint model:
it only contains constraints that consist of a singular call instruction, all
arguments to calls are \parameter{} literals or \variable{} identifiers, and the
call itself is a constraint primitive for the target \solver{}.
To arrive at a flat model, the flattening process will transverse the
declarations, \constraints{}, and the solver goal and flatten any expression
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 \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.
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 \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 \parameters{}, 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
\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 expression. The creation of this new \variable{} and defining \constraints{}
happens in one of two ways:
\begin{itemize}
\item For Boolean expressions in a non-root context, the new \variable{} is
inserted by the flattening process itself. To constrain this
\variable{}, the flattener will then add the \gls{reification} of the
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
\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 \variable{} and defining \constraints{} 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 \variable{}, constrains
this \variable{} to take to correct value, and returns the newly created
\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 \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 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,
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}.
\begin{example}
For instance, in the constraint
\begin{mzn}
constraint (abs(x)*2 >= 20) \/ (abs(x)+5 >= 15);
\end{mzn}
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.
\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
following example.
\begin{example}
Consider the fragment:
\begin{mzn}
function var float: pythagoras(var float: a, var float: b) =
let {
var float: x = pow(a, 2);
var float: y = pow(b, 2);
} in sqrt(x + y);
constraint pythagoras(i, i) >= 5;
\end{mzn}
Although the expressions \mzninline{pow(a, 2)} and \mzninline{pow(b, 2)} are
not syntactically equal, the function call \mzninline{pythagoras(i,i)} using
the same variable for \mzninline{a} and \mzninline{b} makes them equivalent.
\end{example}
A straightforward approach to ensure that the same instantiation of a function
To ensure that syntactically equal expressions are only evaluated once the
\minizinc\ compiler through the use of memorisation. After the flattening of an
expression, the instantiated expression and its result are stored in a lookup
table, the \gls{cse} table. Then before any consequent expression is flattened
the \gls{cse} table is consulted. If an equivalent expression is found, then the
accompanying result is used; otherwise, the evaluation proceeds as normal.
In our example, the evaluation of \mzninline{pythagoras(i, i)} would proceed as
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 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
very beneficial for the efficiency solving process if we can detect that a
reified constraint is in fact not required.
If a constraint is present in the root context, it means that it must hold
globally. If the same constraint is used in a reified context, it can therefore
be replaced with the constant \mzninline{true}, avoiding the need for
reification (or in fact any evaluation).
We can harness \gls{cse} to store the evaluation context when a constraint is
added, and detect when the same constraint is used in both contexts. Whenever a
lookup in the \gls{cse} table is successful, action can be taken depending on
both the current and stored evaluation context. If the stored expression was in
root context, then the constant \mzninline{true} can be used, independent of the
current context. Otherwise, if the stored expression was in reified context and
the current context is reified, then the stored result variable can be used.
Finally, if the stored expression was in reified context and the current context
is root context, then the previous result can be replaced by the constant
\mzninline{true} and the evaluation will proceed as normal with the root context
constraint.
\begin{example}
Consider the fragment:
\begin{mzn}
function var bool: p(var int: x, var int: y) = q(x) /\ r(y);
constraint b0 <-> q(x);
constraint b1 <-> t(x,y);
constraint b1 <-> p(x,y);
\end{mzn}
If we process the top-level constraints in order we create a reified call to
\mzninline{q(x)} for the original call. Suppose processing the second
constraint we discover \mzninline{t(x,y)} is \mzninline{true}, fixing
\mzninline{b1}. When we then process \mzninline{q(x)} in instantiation of the
call \mzninline{p(x,y)}, we find it is the root context. So \gls{cse} needs to
set \mzninline{b0} to \mzninline{true}.
\end{example}
\subsection{Adjusting Domain}%
\label{subsec:back-adjusting-dom}
As discussed in \cref{subsec:back-cp}, the \glspl{domain} of \variables{} can
sometimes be directly changed because of the addition of a \constraint{}.
Similarly, depending on the \glspl{domain} of \variables{} some constraints can
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 \gls{domain} is enough.
Tight domains can also allow us to avoid the creation of reified constraints
when the truth-value of a reified \constraint{} can be determined from the
\glspl{domain} of variables.
\begin{example}%
\label{ex:back-adj-dom}
Consider the following \minizinc\ model:
\begin{mzn}
var 1..10: a;
var 1..5: b;
constraint a < b;
constraint (a > 5) -> (a + b > 12);
\end{mzn}
Given the \glspl{domain} specified in the model, the second constraint is
flattened using to reified \constraints{} for each side of the implication.
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
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}.
\end{example}
During flattening, the \minizinc\ compiler will actively remove values from the
\gls{domain} when it encounters constraints that trivially reduces it. For
example, constraints with a single comparison expression between a \variable{}
and a \parameter{} (\eg\ \mzninline{x != 5}), constraint with a single
comparison between two \variables{} (\eg\ \mzninline{x >= y}), constraints that
directly change the domain (\eg\ \mzninline{x in 3..5}). It, however, will not
perform more complex \gls{propagation}, like the \gls{propagation} of
\glspl{global}.
\subsection{Constraint Aggregation}%
\label{subsec:back-aggregation}
Complex \minizinc\ expression can sometimes result in the creation of many new
variables that represent intermediate results. This is in particular true for
linear and boolean equations that are generally written using \minizinc\
operators. For example the evaluation of the linear constraint \mzninline{x +
2*y <= z} could result in the following \flatzinc:
\begin{nzn}
var int: x;
var int: y;
var int: z;
var int: i1;
var int: i2;
constraint int_times(y, 2, i1);
constraint int_plus(x, i1, i2);
constraint int_le(i2, z);
\end{nzn}
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 directly received the equivalent linear \constraint{}:
\begin{mzn}
constraint int_lin_le([1,2,-1], [x,y,z], 0)
\end{mzn}
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.
This can be resolved using the \gls{aggregation} of constraints. When we
aggregate constraints we collect multiple \minizinc\ expressions, that would
each have been separately translated, and combine them into a singular structure
that eliminates the need for intermediate \variables{}. For example, the
arithmetic definitions can be combined into linear constraints, Boolean logic
can be combined into clauses, and counting constraints can be combined into
global cardinality constraints.
The \minizinc\ compiler aggregates expressions whenever possible. When the
\minizinc\ compiler reaches an expression that could potentially be part of an
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
non-flat arguments.
\subsection{Delayed Rewriting}%
\label{subsec:back-delayed-rew}
Adjusting the \glspl{domain} of variables during flattening means that the
system becomes non-confluent, and some orders of execution may produce
``better'', \ie\ more compact or more efficient, \flatzinc{}.
\begin{example}
The following example is similar to code found in the \minizinc\ libraries of
\gls{mip} solvers.
\begin{mzn}
function var int: lq_zero_if_b(var int: x, var bool: b) =
x <= ub(x)*(1-b);
\end{mzn}
This predicate expresses the constraint \mzninline{b -> x<=0}, using a
well-known method called ``big-M transformation''. The expression
\mzninline{ub(x)} returns a valid upper bound for \mzninline{x}, \ie\ a fixed
value known to be greater than or equal to \mzninline{x}. This could be the
initial upper bound \mzninline{x} was declared with or the current value
adjusted by the \minizinc\ compiler. If \mzninline{b} takes the value 0, the
expression \mzninline{ub(x)*(1-b)} is equal to \mzninline{ub(x)}, and the
constraint \mzninline{x <= ub(x)} holds trivially. If \mzninline{b} takes the
value 1, \mzninline{ub(x)*(1-b)} is equal to 0, enforcing the constraint
\mzninline{x <= 0}.
\end{example}
For \gls{mip} solvers, it is quite important to enforce tight bounds in order to
improve efficiency and sometimes even numerical stability. It would therefore be
useful to rewrite the \mzninline{lq_zero_if_b} predicate only after the
\glspl{domain} of the involved variables has been reduced as much as possible,
in order to take advantage of the tightest possible bounds. On the other hand,
evaluating a predicate may also \emph{impose} new bounds on variables, so it is
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
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
constraints are appended to the end of the current \gls{ast}. All other
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
tightest possible \gls{domain}. One delayed \constraint{} can still influence
the \glspl{domain} of \variables{} used by other delayed \constraints{}.
Delaying the rewriting of constraints might, however, interfere with the
constraint aggregation. Since aggregation is eagerly performed only when a
\constraint{} is first encountered, it cannot aggregate any constraints that
follow from delayed values. For example, if when aggregating Boolean clauses
comes across an expression that needs to be reified, then a new Boolean
\variable{} is created and the reified \constraint{} is delayed. The problem
is, however, that if the definition of this reified constraint turn out to be
in terms of Boolean clauses as well, then this definition could have been
aggregated as well. Because the flattener does not revisit the aggregation of
variables, this does not happen.
\subsection{FlatZinc Optimisation}%
\label{subsec:back-fzn-optimisation}
After the compiler is done flattening the \minizinc\ instance, it enters the
optimisation phase. This phase occurs at the level at which the targeted
\solver{} operates. Depending on this \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{}.
In the current implementation the main focus of the flattener is to propagate
Boolean \constraints{}. The flattener tries to reduce the number of Boolean
\variables{} and tries to reduce the number of literals in clauses and
conjunctions. The additional propagation might fix the result of the
\gls{reification} of a constraint. If this constraint is not yet rewritten, then
the \solver{} will know to use a direct constraint instead of a reified version.
Even more important than the Boolean \constraints{}, are equality
\constraints{}. The flattening is in the unique position to \gls{unify}
\variables{} when they are found to be equal. Since they both have to take the
same value, only a single \variable{} is required in the \flatzinc\ model to
represent them both. Whenever any (recognisable) equality constraint is found
during the optimisation phase, it is removed and the two \variables{} are
unified. Once initialised, it is not always possible for \solvers{} to
\gls{unify} \variables{} internally.
Reference in New Issue View Git Blame Copy Permalink