From a6be2980b76fae6afcfbbf7ba94ef1bcf4ee6024 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Fri, 23 Jul 2021 21:58:39 +1000 Subject: [PATCH] Add initial section on Essence compilation --- assets/acronyms.tex | 2 ++ assets/bibliography/references.bib | 57 ++++++++++++++++++++++++++++++ assets/glossary.tex | 2 +- assets/listing/back_nqueens.eprime | 11 ++++++ chapters/2_background.tex | 50 ++++++++++++++++++++------ 5 files changed, 110 insertions(+), 12 deletions(-) create mode 100644 assets/listing/back_nqueens.eprime diff --git a/assets/acronyms.tex b/assets/acronyms.tex index 31201d3..402713b 100644 --- a/assets/acronyms.tex +++ b/assets/acronyms.tex @@ -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} diff --git a/assets/bibliography/references.bib b/assets/bibliography/references.bib index 52bf959..b713421 100644 --- a/assets/bibliography/references.bib +++ b/assets/bibliography/references.bib @@ -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}, diff --git a/assets/glossary.tex b/assets/glossary.tex index 5275747..0c6183f 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -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}{ diff --git a/assets/listing/back_nqueens.eprime b/assets/listing/back_nqueens.eprime new file mode 100644 index 0000000..785e4fb --- /dev/null +++ b/assets/listing/back_nqueens.eprime @@ -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]) diff --git a/chapters/2_background.tex b/chapters/2_background.tex index c760f8b..af96f1a 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -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}