From 8cfcc7dfe831fe9dec201efaa204c0bedfee0df4 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Fri, 26 Mar 2021 13:28:18 +1100 Subject: [PATCH] Some work on rewriting introduction --- assets/acronyms.tex | 3 + assets/glossary.tex | 25 ++++++++ chapters/1_introduction.tex | 73 +++++++++++++++++++++++ chapters/4_rewriting.tex | 113 +++++++----------------------------- dekker_thesis.tex | 2 +- 5 files changed, 123 insertions(+), 93 deletions(-) diff --git a/assets/acronyms.tex b/assets/acronyms.tex index 8ae5b8a..944524a 100644 --- a/assets/acronyms.tex +++ b/assets/acronyms.tex @@ -1,5 +1,8 @@ +\newacronym[see={[Glossary:]{gls-cbls}}]{cbls}{CBLS}{Constraint-Based Local Search\glsadd{gls-cbls}} \newacronym[see={[Glossary:]{gls-cp}}]{cp}{CP}{Constraint Programming\glsadd{gls-cp}} \newacronym[see={[Glossary:]{gls-cse}}]{cse}{CSE}{Common Subexpression Elimination\glsadd{gls-cse}} \newacronym[see={[Glossary:]{gls-csp}}]{csp}{CSP}{Constraint Satisfaction Problem\glsadd{gls-csp}} \newacronym[see={[Glossary:]{gls-cop}}]{cop}{COP}{Constraint Optimisation Problem\glsadd{gls-cop}} \newacronym[see={[Glossary:]{gls-lns}}]{lns}{LNS}{Large Neighbourhood Search\glsadd{gls-lns}} +\newacronym[see={[Glossary:]{gls-mip}}]{mip}{MIP}{Mixed Integer Programming\glsadd{gls-mip}} +\newacronym[see={[Glossary:]{gls-sat}}]{sat}{SAT}{Boolean Satisfiability\glsadd{gls-sat}} diff --git a/assets/glossary.tex b/assets/glossary.tex index da6c77a..6bb1ecf 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -9,6 +9,13 @@ % program that implements that API}, % } + +\newglossaryentry{gls-cbls}{ + name={constraint-based local search}, + description={\jip{todo}}, +} + + \newglossaryentry{constraint}{ name={constraint}, description={A constraint is a relationship between two or more decision @@ -77,6 +84,13 @@ be described using simpler \glspl{constraint}. \Glspl{solver} sometimes provide dedicated algorithms or rewriting rules to better handle the global constraint}, } +\newglossaryentry{linear-programming}{ + name={linear programming}, + description={Linear programming is a method to optimise an linear objective +function under the condition of a set of constraints which are all in the form +of linear equations}, +} + \newglossaryentry{gls-lns}{ name={large neighbourhood search}, description={Large Neighbourhood Search (LNS) is a meta-search algorithm that @@ -106,6 +120,12 @@ quickly find better solutions to a problem}, extensive library of \glspl{global}}, } +\newglossaryentry{gls-mip}{ + name={Mixed Integer Programming}, + description={A form of \gls{linear-programming} where at least one of the variable +can only take an integer value}, +} + \newglossaryentry{nanozinc}{ name={Nano\-Zinc}, description={TODO}, @@ -130,6 +150,11 @@ maximises or minimises the valuation of the objective} search position and start its search from the beginning}, } +\newglossaryentry{gls-sat}{ + name={boolean satisfiability}, + description={\jip{todo}}, +} + \newglossaryentry{solver}{ name={solver}, description={A solver is a dedicated program or algorithm that can be used to diff --git a/chapters/1_introduction.tex b/chapters/1_introduction.tex index a4e2463..f2b6d85 100644 --- a/chapters/1_introduction.tex +++ b/chapters/1_introduction.tex @@ -1,3 +1,76 @@ %************************************************ \chapter{Introduction}\label{ch:introduction} %************************************************ + +High-level \cmls, like \minizinc, were originally designed as a convenient input +language for \gls{cp} solvers \autocite{marriott-1998-clp}. A user would write a +model consisting of a few loops or comprehensions; given a data file for the +parameters, this would be rewritten into a relatively small set of constraints +which would be fed whole into the solver. The existing process for translating +\minizinc\ into solver-specific constraints is a somewhat ad-hoc, (mostly) +single-pass, recursive unrolling procedure, and many aspects (such as call +overloading) are resolved dynamically. In its original application, this was +acceptable: models (both before and after translation) were small, translation +was fast, and the expected results of translation were obvious. The current +architecture is illustrated in \Cref{sfig:4-oldarch}. + +But over time, the uses of high-level \cmls\ have expanded greatly from this +original vision. It is now used to generate input for wildly different solver +technologies: not just \gls{cp}, but also \gls{mip} \autocite{wolsey-1988-mip}, +\gls{sat} \autocite{davis-1962-dpll} and \gls{cbls} +\autocite{bjordal-2015-fzn2oscarcbls} solvers. Crucially, the same constraint +model can be used with any of these solvers, which is achieved through the use +of solver-specific libraries of constraint definitions. In \minizinc, these +solver libraries are written in the same language. + +\minizinc\ turned out to be much more expressive than expected, so more +and more preprocessing and model transformation has been added to both the core +\minizinc\ library, and users' models. And in addition to one-shot solving, +\minizinc\ is frequently used as the basis of a larger meta-optimisation tool +chain: programmatically generating a model, solving it, then using the results +to generate another slightly different model. + +To a great extent, this is testament to the effectiveness of the language. +However, as they have become more common, these extended uses have revealed +weaknesses of the existing \minizinc\ tool chain. In particular: + +\begin{itemize} + \item The \minizinc\ compiler is inefficient. It does a surprisingly large + amount of work for each expression (especially resolving sub-typing and + overloading), which may be repeated many times --- for example, inside + the body of a comprehension. And as models generated for other solver + technologies (particularly \gls{mip}) can be quite large, the resulting + flattening procedure can be intolerably slow. As the model + transformations implemented in \minizinc\ become more sophisticated, + these performance problems are simply magnified. + \item The generated models often contain unnecessary constraints. During the + transformation, functional expressions are replaced with constraints. + But this breaks the functional dependencies: if the original expression + later becomes redundant (due to model simplifications), \minizinc\ may + fail to detect that the constraint can be removed. + \item Monolithic flattening is wasteful. When \minizinc\ is used for + multi-shot solving, there is typically a large base model common to all + subproblems, and a small set of constraints which are added or removed + in each iteration. But with the existing \minizinc\ architecture, the + whole model must be re-flattened each time. Many use cases involve + generating a base model, then repeatedly adding or removing a few + constraints before re-solving. In the current tool chain, the whole + model must be fully re-flattened each time. Not only does this repeat + all the work done to flatten the base model, This means a large + (sometimes dominant) portion of runtime is simply flattening the core + model over and over again. But it also prevents \emph{the solver} from + carrying over anything it learnt from one problem to the next, closely + related, problem. +\end{itemize} + +In this thesis, we revisit the rewriting of high-level \cmls\ into solver-level +constraint models and describe an architecture that allows us to: + +\begin{itemize} + \item easily integrate a range of \textbf{optimisation and simplification} + techniques, + \item effectively \textbf{detect and eliminate dead code} introduced by + functional definitions, and + \item support \textbf{incremental flattening and solving}, and better + integration with solvers providing native incremental features. +\end{itemize} diff --git a/chapters/4_rewriting.tex b/chapters/4_rewriting.tex index 2c1ed3f..256e3be 100644 --- a/chapters/4_rewriting.tex +++ b/chapters/4_rewriting.tex @@ -2,34 +2,29 @@ \chapter{Rewriting Constraint Modelling Languages}\label{ch:rewriting} %************************************************ -High-level \cmls, like \minizinc, were originally designed as a convenient input -language for \gls{cp} solvers \autocite{marriott-1998-clp}. A user would write a -model consisting of a few loops or comprehensions; given a data file for the -parameters, this would be rewritten into a relatively small set of constraints -which would be fed whole into the solver. The existing process for translating -\minizinc\ into solver-specific constraints is a somewhat ad-hoc, (mostly) -single-pass, recursive unrolling procedure, and many aspects (such as call -overloading) are resolved dynamically. In its original application, this was -acceptable: models (both before and after translation) were small, translation -was fast, and the expected results of translation were obvious. The current -architecture is illustrated in \Cref{sfig:4-oldarch}. +In this chapter We describe a new \textbf{systematic view + of the execution of \cmls}, and build on this to propose a new tool chain. We +show how this tool chain allows us to -But over time, the uses of high-level \cmls\ have expanded greatly from this -original vision. It is now used to generate input for wildly different solver -technologies: not just constraint programming, but also MIP -\autocite{wolsey-1988-mip}, SAT \autocite{davis-1962-dpll} and Constraint-based -Local Search \autocite{bjordal-2015-fzn2oscarcbls} solvers. Crucially, the same -constraint model can be used with any of these solvers, which is achieved -through the use of solver-specific libraries of constraint definitions. In -\minizinc, these solver libraries are written in the same language. +The new architecture is shown in \Cref{sfig:4-newarch}. A constraint model is +first compiled to byte code (called \microzinc), independent of the data. The +byte code is interpreted with the data to produce \nanozinc\ code, an extension +of the existing \flatzinc\ format. The interpreter can even be made incremental: +in \cref{ch:incremental} we discuss how in meta optimisation, no recompilation +is required. -\minizinc\ turned out to be much more expressive than expected, so more -and more preprocessing and model transformation has been added to both the core -\minizinc\ library, and users' models. And in addition to one-shot solving, -\minizinc\ is frequently used as the basis of a larger meta-optimisation tool -chain: programmatically generating a model, solving it, then using the results -to generate another slightly different model. This usage is represented by the -dashed feedback loop in \Cref{sfig:4-oldarch}. +We have developed a prototype of this tool chain, and present experimental +validation of these advantages. The prototype is still very experimental, but +preliminary results suggest the new tool chain can perform flattening much +faster, and produce better models, than the current \minizinc\ compiler. + +This chapter is organised as follows. \Cref{sec:4-micronano} introduces the +\microzinc\ and \nanozinc\ languages, the new intermediate representation we +propose that enables more efficient flattening. \Cref{sec:4-simplification} +describes how we can perform various processing and simplification steps on this +representation, and in \cref{sec:4-experiments} we report on the experimental +results of the prototype implementation. Finally, \Cref{sec:4-conclusion} +presents our conclusions. \begin{figure}[ht] \centering @@ -48,72 +43,6 @@ dashed feedback loop in \Cref{sfig:4-oldarch}. \minizinc\ architecture} \end{figure} -To a great extent, this is testament to the effectiveness of the language. -However, as they have become more common, these extended uses have revealed -weaknesses of the existing \minizinc\ tool chain. In particular: - -\begin{itemize} - \item Flattening is inefficient. The flattener does a surprisingly large - amount of work for each expression (especially resolving sub-typing and - overloading), which may be repeated many times --- for example, inside - the body of a comprehension. And as models generated for other solver - technologies (particularly MIP) can be quite large, the resulting - flattening procedure can be intolerably slow. As the model - transformations implemented in \minizinc\ become more sophisticated, - these performance problems are simply magnified. - \item The generated models often contain unnecessary constraints. During the - transformation, functional expressions are replaced with constraints. - But this breaks the functional dependencies: if the original expression - later becomes redundant (due to model simplifications), \minizinc\ may - fail to detect that the constraint can be removed. - \item Monolithic flattening is wasteful. When \minizinc\ is used for - multi-shot solving, there is typically a large base model common to all - subproblems, and a small set of constraints which are added or removed - in each iteration. But with the existing \minizinc\ architecture, the - whole model must be re-flattened each time. - % Many use cases involve generating a base model, then repeatedly adding - % or removing a few constraints before re-solving. In the current tool - % chain, the whole model must be fully re-flattened each time. Not only - % does this repeat all the work done to flatten the base model, - This means a large (sometimes dominant) portion of runtime is simply - flattening the core model over and over again. But it also prevents - \emph{the solver} from carrying over anything it learnt from one problem - to the next, closely related, problem. -\end{itemize} - -In this chapter, we revisit the rewriting of high-level \cmls, like \minizinc, -into solver-level constraint models. We describe a new \textbf{systematic view - of the execution of \cmls}, and build on this to propose a new tool chain. We -show how this tool chain allows us to: - -\begin{itemize} - \item easily integrate a range of \textbf{optimisation and simplification} - techniques, - \item effectively \textbf{detect and eliminate dead code} introduced by - functional definitions, and - \item support \textbf{incremental flattening and solving}, and better - integration with solvers providing native incremental features. -\end{itemize} - -The new architecture is shown in \Cref{sfig:4-newarch}. The model is first -compiled to byte code (called \microzinc), independent of the data. The byte -code is interpreted with the data to produce \nanozinc\ code, an extension of -the existing \flatzinc\ format. The interpreter can even be made incremental: in -\cref{ch:incremental} we discuss how in meta optimisation, no recompilation is -required. - -We have developed a prototype of this tool chain, and present experimental -validation of these advantages. The prototype is still very experimental, but -preliminary results suggest the new tool chain can perform flattening much -faster, and produce better models, than the current \minizinc\ compiler. - -The rest of the paper is organised as follows. \Cref{sec:4-micronano} introduces -the \microzinc\ and \nanozinc\ languages, the new intermediate representation we -propose that enables more efficient flattening. \Cref{sec:4-simplification} -describes how we can perform various processing and simplification steps on this -representation, and in \cref{sec:4-experiments} we report on the experimental -results of the prototype implementation. Finally, \Cref{sec:4-conclusion} -presents our conclusions. \section{\glsentrytext{microzinc} and \glsentrytext{nanozinc}}\label{sec:4-micronano} diff --git a/dekker_thesis.tex b/dekker_thesis.tex index 8507da9..8e8abce 100644 --- a/dekker_thesis.tex +++ b/dekker_thesis.tex @@ -114,7 +114,7 @@ following publication: % \listoftables{} % \listoflistings{} -\printglossary[type=\acronymtype]{} +\printglossary[nonumberlist,type=\acronymtype]{} \renewcommand{\glsnamefont}[1]{\titlecap{#1}} \printglossary[nonumberlist]{}