Add description of OPL and Essence
This commit is contained in:
parent
383cfee9fc
commit
aae2191bf0
@ -1,28 +1,48 @@
|
||||
\newacronym[see={[Glossary:]{gls-ampl}}]{ampl}{AMPL\glsadd{gls-cbls}}{A
|
||||
Mathematical Programming Language}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-cbls}}]{cbls}{CBLS\glsadd{gls-cbls}}{Constraint-Based
|
||||
Local Search}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-chr}}]{chr}{CHR\glsadd{gls-chr}}{Constraint
|
||||
Handling Rules}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-clp}}]{clp}{CLP\glsadd{gls-clp}}{Constraint
|
||||
Logic Programming}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-cp}}]{cp}{CP\glsadd{gls-cp}}{Constraint
|
||||
Programming}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-cse}}]{cse}{CSE\glsadd{gls-cse}}{Common
|
||||
Sub-expression Elimination}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-csp}}]{csp}{CSP\glsadd{gls-csp}}{Constraint
|
||||
Satisfaction Problem}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-cop}}]{cop}{COP\glsadd{gls-cop}}{Constraint
|
||||
Optimisation Problem}
|
||||
|
||||
\newacronym{cpu}{CPU}{Central Processing Unit}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-gbac}}]{gbac}{GBAC\glsadd{gls-gbac}}{Generalised
|
||||
Balanced Academic Curriculum}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-lcg}}]{lcg}{LCG\glsadd{gls-lcg}}{Lazy Clause
|
||||
Generation}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-lns}}]{lns}{LNS\glsadd{gls-lns}}{Large
|
||||
Neighbourhood Search}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-mip}}]{mip}{MIP\glsadd{gls-mip}}{Mixed Integer
|
||||
Programming}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-opl}}]{opl}{OPL\glsadd{gls-opl}}{The OPL
|
||||
Optimisation Programming Language}
|
||||
|
||||
\newacronym{ram}{RAM}{Random Access Memory}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-sat}}]{sat}{SAT\glsadd{gls-sat}}{Boolean
|
||||
Satisfiability}
|
||||
|
||||
\newacronym[see={[Glossary:]{gls-trs}}]{trs}{TRS\glsadd{gls-trs}}{Term Rewriting
|
||||
System}
|
||||
|
@ -890,6 +890,27 @@
|
||||
publisher = {MIT Press}
|
||||
}
|
||||
|
||||
@article{van-hentenryck-2000-opl-search,
|
||||
author = {Van Hentenryck, Pascal and Perron, Laurent and Puget,
|
||||
Jean-Fran\c{c}ois},
|
||||
title = {Search and Strategies in OPL},
|
||||
year = 2000,
|
||||
issue_date = {Oct. 2000},
|
||||
publisher = {Association for Computing Machinery},
|
||||
address = {New York, NY, USA},
|
||||
volume = 1,
|
||||
number = 2,
|
||||
issn = {1529-3785},
|
||||
url = {https://doi.org/10.1145/359496.359529},
|
||||
doi = {10.1145/359496.359529},
|
||||
journal = {ACM Trans. Comput. Logic},
|
||||
month = oct,
|
||||
pages = {285–320},
|
||||
numpages = 36,
|
||||
keywords = {search, modeling languages, constraint programming,
|
||||
combinatorial optimization}
|
||||
}
|
||||
|
||||
@book{wallis-2011-combinatorics,
|
||||
title = {Introduction to Combinatorics},
|
||||
author = {Wallis, W.D. and George, J.},
|
||||
|
@ -14,6 +14,16 @@
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{gls-ampl}{
|
||||
name={AMPL: A Mathematical Programming Language},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{annotation}{
|
||||
name={annotation},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{array}{
|
||||
name={array},
|
||||
description={},
|
||||
@ -89,6 +99,11 @@
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{essence}{
|
||||
name={Essence},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{flatzinc}{
|
||||
name={Flat\-Zinc},
|
||||
description={},
|
||||
@ -114,6 +129,11 @@
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{interval}{
|
||||
name={interval},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{knapsack}{
|
||||
name={knapsack problem},
|
||||
description={},
|
||||
@ -210,6 +230,11 @@
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{search-heuristic}{
|
||||
name={search heuristic},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{solver}{
|
||||
name={solver},
|
||||
description={},
|
||||
|
@ -229,6 +229,9 @@ assignment to the \glspl{variable} that satisfies the constraints and minimises
|
||||
the value of a \gls{variable}, \mzninline{solve minimize x;}, or similarly
|
||||
maximises the value of a \gls{variable}, \mzninline{solve maximize x;}.
|
||||
|
||||
\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,
|
||||
@ -548,7 +551,7 @@ following stages:
|
||||
declarations and is allowed in the locations where they are used. \\ In the
|
||||
process of type checking the model, all identifiers and calls are connected to
|
||||
the declaration that they refer to.
|
||||
\item[Flattening] \jip{TODO: This should have something}
|
||||
\item[Flattening] \jip{TODO:\@ This should have something}
|
||||
\item[Optimisation] Given the generated \flatzinc{} model, \texttt{minizinc}
|
||||
will try optimise this model to try and reduce the number of
|
||||
\glspl{constraint} and size of the \glspl{domain} of \glspl{variable} in the
|
||||
@ -557,30 +560,221 @@ following stages:
|
||||
Any solutions found by the \gls{solver} are communicated back to the user.
|
||||
\end{description}
|
||||
|
||||
\jip{TODO: Description of the flattening process}
|
||||
\jip{TODO:\@ Description of the flattening process}
|
||||
|
||||
\jip{TODO: Description of the techniques used during the optimisation phase}
|
||||
\jip{TODO:\@ Description of the techniques used during the optimisation phase}
|
||||
|
||||
\subsection{Propagation}
|
||||
\subsection{Propagation}%
|
||||
\label{sub:back-propagation}
|
||||
|
||||
\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 of the other prominent \cmls{} and will compare them to
|
||||
\minizinc\ to indicate to the reader where techniques might have to be adjusted
|
||||
to fit other languages.
|
||||
|
||||
\subsection{AMPL}%
|
||||
\label{sub:back-ampl}
|
||||
|
||||
\subsection{OPL}%
|
||||
\label{sub:back-}
|
||||
\label{sub:back-opl}
|
||||
|
||||
\glsaccesslong{opl} \autocite{van-hentenryck-1999-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}. 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 \glspl{constraint} in an incremental and more
|
||||
natural fashion. When solving a scheduling problem, the \gls{opl} makes use of
|
||||
specialised \gls{interval} \glspl{variable}, which represent when a task will be
|
||||
scheduled. For example the \gls{variable} declarations and \glspl{constraint}
|
||||
for a jobshop problem would look like this in an \gls{opl} model:
|
||||
|
||||
\begin{minted}[autogobble=true]{text}
|
||||
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{minted}
|
||||
|
||||
The equivalent declarations and \glspl{constraint} 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 \glspl{variable} that represent the start times of the activity
|
||||
and a \gls{variable} to represent the time at which all activities are finished.
|
||||
The \gls{opl} model also has the advantage that it can first create resource
|
||||
objects and then use the \texttt{requires} keyword to force tasks on the same
|
||||
machine to be mutually exclusive. In \minizinc{} the same requirement is
|
||||
implemented through the use of \mzninline{disjunctive} constraints. Although
|
||||
this has the same effect, all mutually exclusive jobs have to be combined in a
|
||||
single statement in the model. This can make it harder in \minizinc\ to write
|
||||
the correct \gls{constraint} and its meaning might be less clear.
|
||||
|
||||
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{minted}[autogobble=true]{text}
|
||||
search {
|
||||
try x < y | y >= x endtry;
|
||||
}
|
||||
\end{minted}
|
||||
|
||||
This search strategy will ensure that we first try and find a solution where the
|
||||
\gls{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 oposite
|
||||
is true. This search specification, like many other imaginable, cannot be
|
||||
enforce using \minizinc\ \gls{search-heuristic} \glspl{annotation}.
|
||||
|
||||
To support \gls{opl}'s dedicated search language, the language is tightly
|
||||
integrated with its dedicated \glspl{solver}. Its search syntax requires that
|
||||
the \gls{opl} process can directly interact with the \gls{solver}'s internal
|
||||
search mechanism and that the \gls{solver} reasons about search on the same
|
||||
level as the \gls{opl} model. It is therefore not possible to connect other
|
||||
\glspl{solver} to \gls{opl}.
|
||||
|
||||
The \gls{opl} does not allow modellers to create their own (user-defined)
|
||||
functions. A modeller is restricted to the \gls{global} constraint library
|
||||
provided by the \gls{opl}'s standard library.
|
||||
|
||||
\subsection{Essence}%
|
||||
\label{sub:back-essence}
|
||||
|
||||
\gls{essence} \autocite{frisch-2007-essence} is another high-level \cml\ is
|
||||
cherished for its adoption of high-level \gls{variable} types. In addition to
|
||||
all variable types that are contained in \minizinc{}, \gls{essence} also
|
||||
contains:
|
||||
|
||||
\begin{itemize}
|
||||
\item finite sets of non-iteger types,
|
||||
\item finite multisets of any type,
|
||||
\item finite (partial) functions,
|
||||
\item and (regular) partitions of finite types.
|
||||
\end{itemize}
|
||||
|
||||
Since sets, multisets, and functions can be defined on any other type, these
|
||||
types can be arbitrary nested and the modeller can define, for example, a
|
||||
\gls{variable} that is a set of set of integers. Partitions can be defined for
|
||||
finite types. These types in \gls{essence} are restricted to Booleans,
|
||||
enumerated types, or a restricted set of integers.
|
||||
|
||||
For example, the Social Golfers Problem, can be modelled in \gls{essence} as
|
||||
follows:
|
||||
|
||||
\begin{minted}[autogobble=true]{text}
|
||||
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{minted}
|
||||
|
||||
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 \glspl{constraint}
|
||||
in the \minizinc{} are implied in the \gls{essence} model. This is an example
|
||||
where the use of high-level types can help give the modeller create more concise
|
||||
models.
|
||||
|
||||
These high-level variables are often not directly supported by the
|
||||
\glspl{solver} that is employed to solve \gls{essence} instances. To solve the
|
||||
problem, not only do the \glspl{constraint} have to be translated to
|
||||
\glspl{constraint} supported by the solver, but also all \glspl{variable} have
|
||||
to be translated to a combination of \glspl{constraint} and \glspl{variable}
|
||||
compatible with the targeted solver.
|
||||
|
||||
\section{Term Rewriting}%
|
||||
\label{sec:back-term}
|
||||
|
||||
At the heart of the flattening process lies a \glsaccesslong{trs}. A \gls{trs}
|
||||
\cite{baader-1998-term-rewriting} describes a computational model the full
|
||||
\autocite{baader-1998-term-rewriting} describes a computational model the full
|
||||
process can be describe as the application of rules \(l \rightarrow r\), that
|
||||
replace a \gls{term} \(l\) with another \gls{term} \(r\). A \gls{term} is an
|
||||
expression with nested sub-expressions consisting of \emph{function} and
|
||||
|
Reference in New Issue
Block a user