284 lines
14 KiB
TeX
284 lines
14 KiB
TeX
%************************************************
|
|
\chapter{Review of Literature}\label{ch:background}
|
|
%************************************************
|
|
|
|
A goal shared between all programming languages is to provide a certain level of
|
|
abstraction: an assembly language allows you to abstract from the binary
|
|
instructions and memory positions; Low-level imperial languages, like FORTRAN,
|
|
were the first to allow you to abstract from the processor architecture of the
|
|
target machine; and nowadays writing a program requires little knowledge of the
|
|
actual workings of the hardware.
|
|
|
|
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
|
|
solve the problem, but rather provides the problem requirements. You could say
|
|
that a constraint model actually describes the solution to the problem.
|
|
|
|
In a constraint model, instead of specifying the manner in which we can find the
|
|
solution, we give a concise description of the problem. We describe what we
|
|
already know, the \glspl{parameter}, what we wish to know, the \glspl{variable},
|
|
and the relationships that should exists 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
|
|
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
|
|
\gls{solver} for short, that can find a solution that fits the requirements of
|
|
the model.
|
|
|
|
\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}
|
|
|
|
\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.
|
|
|
|
One way to solve this problem is to try all combinations of toys, but this is
|
|
time intensive and quickly grows with the number of toys considered (which one
|
|
would quickly realise trying to pack a car \(2^{|\text{toys}|}\) different
|
|
ways).
|
|
|
|
An educated reader in optimisation problems might recognise that this is a
|
|
variation on the widely known \gls{knapsack}, more specifically a \textit{0--1
|
|
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
|
|
number of toys.
|
|
|
|
Although expert knowledge can sometimes bring you an efficient solution to a
|
|
known problem, it should be noted that not all problems will easily map to
|
|
well known (and studied) problems. Even when part of a problem finds an
|
|
equivalent in a well studied problem, the overall problem might still contain
|
|
requirements that impair you from using known algorithms to solve the problem.
|
|
For example, if wanted to bring toys with different colours, then the
|
|
algorithm in \cref{lst:2-dyn-knapsack} would have to be drastically changed.
|
|
\Gls{constraint-modelling} can offer a more flexible alternative that requires
|
|
less expert knowledge.
|
|
|
|
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 \gls{variable}. It contains the selection of
|
|
toys that will be packed for the trip. \(z\) is the objective \gls{variable}
|
|
that is maximised to find the optimal selections of toys to pack. The
|
|
\gls{parameter} \(T\) is the set of all the toys. The \(joy\) and \(space\)
|
|
functions are \glspl{parameter} used to map toys, \( t \in T\), to a value
|
|
depicting the amount of enjoyment and space required respectively. Finally,
|
|
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
|
|
\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.
|
|
|
|
\end{example}
|
|
|
|
In the remainder of this chapter we will first, in \cref{sec:back-minizinc}
|
|
introduce \minizinc\ as the leading \cml\ used within this thesis.
|
|
\cref{sec:back-mzn-interpreter} explains the process that the current \minizinc\
|
|
interpreter uses to translate a \minizinc\ model into a solver-level constraint
|
|
model. Then, \cref{sec:back-other-languages} introduces alternative \cmls\ and
|
|
compares their functionality to \minizinc{}. Finally, \cref{sec:back-term} and
|
|
\cref{sec:back-clp} survey the closely related fields of \gls{term-rewriting}
|
|
and \gls{clp}.
|
|
|
|
\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.
|
|
|
|
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}.
|
|
|
|
\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}
|
|
|
|
The model starts with the declaration of the \glspl{parameter}.
|
|
\Lref{line:back:knap:toys} declares an enumerated type that represents all
|
|
possible toys, \(T\) in the mathematical model in the example.
|
|
\Lref{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
|
|
\gls{parameter} to represent the car capacity as an equivalent to \(C\).
|
|
|
|
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.
|
|
|
|
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}.
|
|
|
|
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.
|
|
|
|
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 \gls{solver}, which will attempt
|
|
to determine an assignment to each decision 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}
|
|
|
|
|
|
|
|
\subsection{MiniZinc Types}%
|
|
\label{subsec:back-mzn-type}
|
|
|
|
\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. }
|
|
|
|
\subsection{MiniZinc Expressions}%
|
|
\label{subsec:back-mzn-expr}
|
|
|
|
|
|
\paragraph{Global Constraints}
|
|
\paragraph{Operators}
|
|
\paragraph{Conditional Expressions}
|
|
\paragraph{Array Operations}
|
|
\paragraph{Set Operations}
|
|
\paragraph{Generator Expressions}
|
|
\paragraph{Let Expressions}
|
|
|
|
|
|
\subsection{Handling Undefined Expressions}%
|
|
\label{subsec:back-mzn-partial}
|
|
|
|
Some expressions in the \cmls\ do not always have a well defined result.
|
|
Examples of such expressions in \minizinc\ are:
|
|
|
|
\begin{itemize}
|
|
\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: \\
|
|
\mzninline{array1d(1..3, [1,2,3])[0] = @??@}
|
|
|
|
\item Finding the minimum or maximum or an empty set: \\ \mzninline{min({}) =
|
|
@??@}
|
|
|
|
\item Computing the square root of a negative value: \\ \mzninline{sqrt(-1) = @??@}
|
|
|
|
\end{itemize}
|
|
|
|
The existence of undefined expressions can cause confusion in \cmls. There is
|
|
both the question what happens when a undefined expressions 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 a expressions contains undefined sub-expression, it will only be marked as undefined if the value of the subexpression 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 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. \jip{TODO:\@ This also corresponds to Kleene semantics, maybe I should
|
|
use a different example}
|
|
|
|
Frisch and Stuckey also show that different \glspl{solver} often employ
|
|
different semantical models \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 \gls{solver} model.
|
|
|
|
\section{The Current \glsentrytext{minizinc} Interpreter}%
|
|
\label{sec:back-mzn-interpreter}
|
|
|
|
\section{Other Constraint Modelling Languages}%
|
|
\label{sec:back-other-languages}
|
|
|
|
\section{ACD Term Rewriting}%
|
|
\label{sec:back-term}
|
|
|
|
\section{Constraint Logic Programming}%
|
|
\label{sec:back-clp}
|