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

Add initial section on Essence compilation

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-23 21:58:39 +10:00
parent 88d1fb41af
commit a6be2980b7
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
5 changed files with 110 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
assets/acronyms.tex
View File

@ -20,6 +20,8 @@
\newacronym{cpu}{CPU}{Central Processing Unit}
\newacronym{ess-prime}{Essence'}{Essence Prime}
\newacronym{gbac}{GBAC}{Generalised Balanced Academic Curriculum}
\newacronym[see={[Glossary:]{gls-lcg}}]{lcg}{LCG\glsadd{gls-lcg}}{Lazy Clause Generation}

57
assets/bibliography/references.bib
View File

@ -7,6 +7,39 @@
address = {USA},
}
@phdthesis{akgun-2014-essence,
author = {{\"{O}}zg{\"{u}}r Akg{\"{u}}n},
title = {Extensible automated constraint modelling via refinement of abstract
problem specifications},
school = {University of St Andrews, {UK}},
year = {2014},
url = {http://hdl.handle.net/10023/6547},
timestamp = {Mon, 15 Aug 2016 18:48:06 +0200},
biburl = {https://dblp.org/rec/phd/ethos/Akgun14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@inproceedings{akgun-2013-auto-ess,
author = {Ozgur Akgun and Alan M. Frisch and Ian P. Gent and Bilal Syed
Hussain and Christopher Jefferson and Lars Kotthoff and Ian Miguel
and Peter Nightingale},
editor = {Christian Schulte},
title = {Automated Symmetry Breaking and Model Selection in Conjure},
booktitle = {Principles and Practice of Constraint Programming - 19th
International Conference, {CP} 2013, Uppsala, Sweden, September
16-20, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8124},
pages = {107--116},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-40627-0\_11},
doi = {10.1007/978-3-642-40627-0\_11},
timestamp = {Tue, 14 May 2019 10:00:45 +0200},
biburl = {https://dblp.org/rec/conf/cp/AkgunFGHJKMN13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@inproceedings{araya-2008-cse-numcsp,
author = {Ignacio Araya and Bertrand Neveu and Gilles Trombettoni},
editor = {Peter J. Stuckey},
@ -523,6 +556,15 @@
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@inproceedings{gokberk-2020-ess-incr,
author = {G{\"{o}}kberk Ko{\c{c}}ak and {\"{O}}zg{\"{u}}r Akg{\"{u}}n and
Nguyen Dang and Ian Miguel},
title = {Efficient Incremental Modelling and Solving},
year = {2020},
booktitle = {Proceedings of ModRef'08, the Seventh International Workshop on
Constraint Modelling and Reformulation},
}
@manual{gurobi-2021-gurobi,
author = {{Gurobi Optimization, LLC}},
title = {Gurobi Optimizer Reference Manual},
@ -867,6 +909,21 @@
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@article{nightingale-2017-ess-prime,
author = {Peter Nightingale and {\"{O}}zg{\"{u}}r Akg{\"{u}}n and Ian P. Gent
and Christopher Jefferson and Ian Miguel and Patrick Spracklen},
title = {Automatically improving constraint models in Savile Row},
journal = {Artif. Intell.},
volume = {251},
pages = {35--61},
year = {2017},
url = {https://doi.org/10.1016/j.artint.2017.07.001},
doi = {10.1016/j.artint.2017.07.001},
timestamp = {Fri, 27 Mar 2020 08:45:01 +0100},
biburl = {https://dblp.org/rec/journals/ai/NightingaleAGJM17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@software{perron-2021-ortools,
title = {OR-Tools},
version = {9.0},

2
assets/glossary.tex
View File

@ -219,7 +219,7 @@
\newglossaryentry{essence}{
name={Essence},
description={A \gls{cml} known for its high-level \gls{variable} types. See \cref{sub:back-essence}},
description={A \gls{cml} known for its high-level \gls{variable} types. The rewriting process of Essence first transforms an Essence model into \gls{ess-prime}. A \instance{} formed with an \gls{ess-prime} model is then rewritten into a \gls{slv-mod}. See \cref{sub:back-essence}},
}
\newglossaryentry{eqsat}{

11
assets/listing/back_nqueens.eprime Normal file
View File

@ -0,0 +1,11 @@
language ESSENCE' 1.0
given n : int(1..)
letting ROW be domain int(1..n)
letting COL be domain int(1..n)
find q: matrix indexed by [ COL ] of ROW
such that
allDiff(q),
allDiff([q[i]+i | i : COL]),
allDiff([q[i]-i | i : COL])

50
chapters/2_background.tex
View File

@ -615,7 +615,7 @@ They allow modellers to always use \glspl{global} and depending on the \solver{}
As an example of the \gls{propagation} mechanism, let us consider the N-Queens problem.
Given a chessboard of size \(n \times n\), find a placement for \(n\) queen chess pieces such that no queen can attack another.
This means we can only place one queen per row, one queen per column, and one queen per diagonal.
The problem can be modelled in \minizinc\ as follows.
The problem can be modelled in \minizinc{} as follows.
\begin{mzn}
int: n;
@ -1070,19 +1070,47 @@ Partitions are defined for finite types: Booleans, enumerated types, or a restri
This is an example where the use of high-level types helps the modeller create more concise models.
Apart from syntax and the \variable{} viewpoint, the \constraint{} that enforces that golfers only occur in the same group once is identical.
\begin{listing}
\mznfile{assets/listing/back_sgp.mzn}
\caption{\label{lst:back-mzn-sgp} A \minizinc{} model describing the social golfers problem}
\end{listing}
\end{example}
\begin{listing}
\mznfile{assets/listing/back_sgp.mzn}
\caption{\label{lst:back-mzn-sgp} A \minizinc{} model describing the social golfers problem}
\end{listing}
\Gls{essence} allows the use of many high-level \variable{} types and \constraints{} on these \variables{}.
Since these types of \variables{} are often not \gls{native} to the \solver{}, \gls{rewriting} will translate these types into \gls{native} \variables{} and \constraints{}.
However, along the way there can be many decisions about the representation used for the \solver{}.
There are often multiple ways to represent a high-level \variable{}, or how to enforce its implicit \constraints{}.
Unlike \minizinc{}, \Gls{essence} does not allow modellers or \solvers{} to influence this process directly.
The process is internal to the \gls{essence} compiler.
Since these types of \variables{} are often not \gls{native} to the \solver{}, an extensive \gls{rewriting} process is required to arrive at a \gls{slv-mod}.
Different from the other two languages presented in this section, the implementation of the \gls{essence} toolchain is available open source and has been the subject of published research.
The \gls{rewriting} process of \gls{essence} is split into two steps.
First, an \gls{essence} model is transformed into \gls{ess-prime}.
Then, an \gls{ess-prime} model forms an \instance{}, and is subsequently rewritten into a \gls{slv-mod}.
Compared to \gls{essence}, the \gls{ess-prime} language does not contain the same high-level \variables{}.
As such, the main task of Conjure, the \compiler{} from \gls{essence} to \gls{ess-prime}, is to decide on a representation of these \variables{} in terms of integer and Boolean \variables{} \autocite{akgun-2014-essence}.
However, there are often multiple ways to represent a high-level \variable{}, or how to enforce its implicit \constraints{}.
Although the modeller is able to decide on representation, Conjure has been extended to automatically select among the models it produces \autocite{akgun-2013-auto-ess}.
\paragraph{Essence'}
Once a \cmodel{} is turned into \gls{ess-prime} it is at a very similar level to a \minizinc{} model.
This can be illustrated using the N-Queens problem introduced in \cref{ex:back-nqueens}.
The same problem is modelled in \gls{ess-prime} is shown in \cref{lst:back-ep-nqueens}.
Apart from the syntax used, both languages use the exact same concepts to model the problem.
\begin{listing}
\plainfile{assets/listing/back_nqueens.eprime}
\caption{\label{lst:back-ep-nqueens} A \gls{ess-prime} model describing the N-Queens problem.}
\end{listing}
An \instance{} of a \gls{ess-prime} model can be rewritten by Saville Row into a \gls{slv-mod} for a variety of \solvers{}, including \gls{cp}, \gls{sat}, and \gls{maxsat} \solvers{}.
Savile Row \autocite{nightingale-2017-ess-prime}, and its predecessor Tailor \autocite{rendl-2010-thesis}, have often stood at the forefront of \gls{rewriting} \cmodels{}.
As such, at present many simplification techniques used during \gls{rewriting} are shared between \gls{ess-prime} and \minizinc{}.
At its core, however, the \gls{rewriting} of \gls{ess-prime} works very differently from \minizinc{}.
\Gls{ess-prime} is rewritten using a more traditional \compiler{}.
For all concepts in the language the \compiler{} intrinsically knows how to rewrite it for its target \solver{}.
Recently, \textcite{gokberk-2020-ess-incr} have also presented Savile Row as the basis of a \gls{meta-optimisation} toolchain.
The authors extend Savile Row to bridge the gap between the incremental assumption interface of \gls{sat} \solvers{} and the modelling language and show how this helps to efficiently solve pattern mining and optimisation problems.
Consequently, this research reiterates the use of \gls{meta-optimisation} algorithms in \cmls{} and the need for incremental bridging between the modelling language and the \solver{}.
\section{Term Rewriting}%
\label{sec:back-term}