From 4562bb685d7e636ea9951d2ac9536cebaafcf956 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Wed, 28 Jul 2021 13:53:53 +1000 Subject: [PATCH] Guido's abstract / intro notes --- chapters/0_abstract.tex | 8 +++---- chapters/1_introduction.tex | 48 ++++++++++++++++++------------------- 2 files changed, 28 insertions(+), 28 deletions(-) diff --git a/chapters/0_abstract.tex b/chapters/0_abstract.tex index 7504c6a..07e07db 100644 --- a/chapters/0_abstract.tex +++ b/chapters/0_abstract.tex @@ -2,7 +2,7 @@ \chapter{Abstract}\label{ch:abstract} %************************************************ -\vspace{-8em} +\vspace{-5em} \noindent{}\Cmls{} are a prominent way to model and solve real world problems. They are used in areas such as scheduling, supply chain management, and transportation, among many others. @@ -27,8 +27,8 @@ The architecture is extended using a range of well-known simplification techniqu In addition, we incorporate new analysis techniques to avoid the use of \glspl{reif} or replace them with \glspl{half-reif}, where possible. The architecture is designed to incorporate incremental \constraint{} modelling in two ways. -Primarily, the \gls{rewriting} process is fully incremental: changes made to the \instance{} through a provided interface require minimal addition \gls{rewriting} effort. +Primarily, the \gls{rewriting} process is fully incremental: changes made to the \instance{} through a provided interface require minimal additional \gls{rewriting} effort. Moreover, we introduce \gls{rbmo}, a way to specify \gls{meta-optimization} algorithms directly in \minizinc{}. -These specifications are executed by a normal \minizinc{} \solver{}, requiring only a slight extension of its capabilities. +These specifications are executed directly by a \minizinc{} \solver{}, using a simple extension. -Together, the functionality of this architecture helps to make \cmls{} a more powerful and attractive approach to solve real world problems. +Together, the functionality of this architecture helps to make constraint modelling a more powerful and attractive approach to solve real world problems. diff --git a/chapters/1_introduction.tex b/chapters/1_introduction.tex index 7d56e77..6fc7b88 100644 --- a/chapters/1_introduction.tex +++ b/chapters/1_introduction.tex @@ -4,7 +4,7 @@ \noindent{}A \gls{dec-prb} is any problem that requires us to make decisions according to a set of rules. Many important and difficult problems in the real world are \glspl{dec-prb}. -We can think, for instance, about the decision on the country's rail timetable or the stand-by locations for ambulances in the region. +We can think, for instance, about the decisions on the country's rail timetable or the stand-by locations for ambulances in the region. Formally, we define a \gls{dec-prb} as a set of \variables{} subject to a set of logical \constraints{}. A \gls{sol} to such a problem is the \gls{assignment} of all \variables{} to values that abide by the logic of the \constraints{}. These problems are also highly computationally complex: even with the fastest computers, finding a solution can take a long time. @@ -16,20 +16,19 @@ Famous classes of decision and \glspl{opt-prb}, such as \gls{sat} \autocite{bier And, over the years, highly specialized \solvers{} have been created to find \glspl{sol} for these classes of problems. Nowadays, most decision and \glspl{opt-prb} are solved by encoding them into one of the above-mentioned classes of problems. -Encoding one problem in terms of another is, however, a difficult problem. +Encoding one problem in terms of another is, however, a difficult task. The problem classes can be restrictive: the input to the \solver{}, the \gls{slv-mod}, can only contain \gls{native} \variables{} and \constraints{}, meaning those that are directly supported by the \solver{}. Furthermore, \constraints{} can only refer to \variables{}, they cannot be (directly) dependent on other \constraints{}. For example, \gls{sat} \solvers{} can only reason about Boolean \variables{}, deciding if something is true or false. \Constraints{} for \gls{sat} \solvers{} have to be in the form of disjunctions of Boolean \variables{}, or their negations. But, not only does the encoding have to be correct, the encoding also has to be performant. -There are often many possible correct encodings of a problem, but there can be a significant difference in how quickly the \solver{} finds a \gls{sol} for them. -The preferred encoding can however differ between \solvers{}. +There are often many possible correct encodings of a problem, but there can be a significant difference in how quickly the \solver{} finds a \gls{sol} for them and the preferred encoding can differ between \solvers{}. Two \solvers{} designed to solve the same problem class can perform very differently. \Cmls{} have been designed to tackle these issues. They serve as a level of abstraction between the modeller and the \solver{}. -The typical process of a \cml{} is visualized in \cref{fig:intro-cml-flow}. +The typical process of using a \cml{} is visualized in \cref{fig:intro-cml-flow}. Instead of providing a flat list of \variables{} and \constraints{}, a modeller creates a \cmodel{} using the more natural syntax of the \cml{}. A \cmodel{} can generally describe a class of problems through the use of \prbpars{}: values assigned by external input. Once given a complete \gls{assignment} of the \prbpars{}, the \cmodel{} forms an \instance{}. @@ -42,23 +41,23 @@ The \gls{rewriting} process of a \cml{} transforms a \cmodel{} into a \gls{slv-m \end{figure} Traditional \cmls{}, such as \emph{\glsxtrshort{ampl}} \autocite{fourer-2003-ampl}, \gls{essence} \autocite{frisch-2007-essence}, and \emph{\glsxtrshort{opl}} \autocite{van-hentenryck-1999-opl}, offer the modeller an expressive language that can be used to target a great variety of \solvers{}. -However, these language lack a certain level of flexibility: the modeller is unable to capture common concepts used throughout a \cmodel{}, and the \solver{} cannot influence their way in which the problem is encoded. +However, these languages lack a certain level of flexibility: the modeller is unable to capture common concepts used throughout a \cmodel{}, and the \solver{} cannot influence their way in which the problem is encoded. This is a stark difference to \gls{clp} languages, such as \gls{sicstus} \autocite{carlsson-1997-sicstus}, which are said to be the precursors to \cmls{}. -In these languages, the modeller is encouraged to create high-level concepts and declare the way in which they are rewritten into \gls{native} \constraints{}. +In these languages, the modeller is encouraged to express high-level concepts by defining custom predicates and functions and declare the way in which they are rewritten into \gls{native} \constraints{}. The downside of \gls{clp} languages is that, because of its search mechanism, the \solver{} is tightly integrated within the \gls{rewriting}. These languages thus lack the \solver{}-independence of \cmls{}. \minizinc{} \autocite{nethercote-2007-minizinc} is a functional \cml{} that operates on a level in between these two types of languages. -Like a traditional \cml{}, it is a \solver{}-independent \cml{}. +Like a traditional \cml{}, it is \solver{}-independent. Like a \gls{clp} language, modellers can declare and reuse common concepts and control the encoding into the \gls{slv-mod} through the use of function definitions. -Fundamentally, in its \gls{rewriting} process \minizinc{} is a functional language. +Fundamentally, in its \gls{rewriting} process \minizinc{} is a functional programming language. It continuously evaluates the calls in a \minizinc{} \instance{} until it reaches \gls{native} \constraints{}. Like other functional languages, \minizinc{} allows recursion; it can be used as a fully Turing complete programming language. Although \minizinc{} is based on this powerful paradigm, its success has made certain problems apparent. -The language was originally designed to target \gls{cp} \solvers{}, where the \glspl{slv-mod} typically contain a few highly complex \constraints{}. -Its use has extended to rewrite for \gls{mip} and \gls{sat} \solvers{}, whose \glspl{slv-mod} often contain large numbers \variables{} and simple \constraints{}, generated by a complex library of \minizinc{} functions. +The language was originally designed to target \gls{cp} \solvers{}, where the \glspl{slv-mod} typically contain only few, highly complex \constraints{}. +Its use has however, over time, extended to rewrite for \gls{mip} and \gls{sat} \solvers{}, whose \glspl{slv-mod} often contain numerous \variables{} and simple \constraints{}, generated by a complex library of \minizinc{} functions. For many applications, \minizinc{} now requires a significant, and sometimes prohibitive, amount of time to rewrite \instances{}. Unlike \gls{clp} \gls{rewriting}, the \minizinc{} \gls{rewriting} process does not consider incremental changes to its \gls{slv-mod}. @@ -68,7 +67,7 @@ The overhead of \gls{rewriting} all these \instances{} separately can be substan In this thesis we revisit the \gls{rewriting} of functional \cmls{} into \glspl{slv-mod}. We design and evaluate an architecture for \cmls{} that can accommodate the modern uses of these languages. -\section{Constraint Modelling Varieties} +\section{Different Ways of Modelling with Constraints} Let us now study the different ways of constraint modelling in more detail, starting with one of the most commonly used \cmls{}: \glsxtrshort{ampl}. @@ -91,7 +90,7 @@ As an \gls{opt-prb}, our goal is to find a schedule that minimizes the finishing In order of occurrence, \lrefrange{line:intro:param:start}{line:intro:param:end} show the declarations of the \prbpars{}. To create an \instance{} of the problem, the modeller provides the number of jobs and machines that are considered, and the duration of each task. \Lrefrange{line:intro:var:start}{line:intro:var:end} show the \variable{} declarations: for each task we decide on its start time. -We also declare the end time of the last task as a \variable{}, to ease the modelling of the problem. +We also declare the end time of the last task as a \variable{}, to make it easier to model the \gls{objective}. This \variable{} is made to be our optimization goal on \lref{line:intro:goal}. Finally, \lrefrange{line:intro:con:start}{line:intro:con:end} express the \constraints{} of our problem in terms of equations bound by logic. @@ -133,7 +132,7 @@ For example, the concepts of one task preceding another and non-overlapping of t The definition of \texttt{non\_overlap} requires that either task A precedes task B, or vice versa. However, unlike the \glsxtrshort{ampl} model, Prolog would not provide this choice to the \solver{}. -Instead, it enforces one, test if this works, and it otherwise enforces the other. +Instead, it enforces one, tests if this works, and it otherwise enforces the other. This is a powerful mechanism where choices are made in the \gls{rewriting} process, and not in the \solver{}. The problem with the mechanism is that it requires a highly incremental interface with the \solver{} that can incrementally post and retract \constraints{}. @@ -161,14 +160,15 @@ For example, a modeller could create the following \minizinc{} function to expre \minizinc{} also determines how an \instance{} is encoded for a \solver{} through function definitions. All functionality in the \minizinc{} language is eventually expressed using function calls. The \solver{}, then, has the decision to choose if this call is a \gls{native} \constraint{}, or how this call is rewritten. -For example, the logical \mzninline{or}-operator, which was only supported for \gls{cp} \solvers{} in \glsxtrshort{ampl}, could be defined for \gls{mip} solvers in \minizinc{} using the following definition. +Each \solver{} supplies its own library of \minizinc{} function definitions for common \constraints{}. +For example, the logical \mzninline{or}-operator, which was only supported for \gls{cp} \solvers{} in \glsxtrshort{ampl}, could be defined in the \minizinc{} library for a \gls{mip} \solver{} using the following definition. \begin{mzn} predicate bool_or(var bool: x, var bool: y) = x + y >= 1; \end{mzn} -\noindent{}Whereas the following definition would mark it as a \gls{native} \constraint{} for a \gls{cp} \solver{}, by not defining a body. +\noindent{}Whereas, the \minizinc{} library of a \gls{cp} \solver{} could include the following definition to mark it as a \gls{native} \constraint{}, by not defining a body. \begin{mzn} predicate bool_or(var bool: x, var bool: y); @@ -177,7 +177,7 @@ For example, the logical \mzninline{or}-operator, which was only supported for \ The functional paradigm employed by \minizinc{} has shown itself to be powerful and flexible for the modeller and \solver{} However, the performance of the functional evaluation of the language can be a limiting factor. -\section{The Problems of Rewriting MiniZinc} +\section{Why Rewriting MiniZinc is Difficult} A \minizinc{} model generally consists of a few loops or \glspl{comprehension}; for a \gls{cp} solver, 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 a \gls{slv-mod} is a somewhat ad-hoc, (mostly) single-pass, recursive unrolling procedure, and many aspects (such as call overloading) are resolved dynamically. @@ -204,7 +204,7 @@ In particular: An important decision that is made during \gls{rewriting} is if a \constraint{} can be enforced directly or if it is dependent on other \constraints{}. In the second case, a \gls{reif} has to be introduced: an often costly form of the \constraint{} that determines whether a \constraint{} holds rather than enforcing the \constraint{} itself. It is possible, however, that further \gls{rewriting} can reveal a \gls{reif} to be unnecessary. - Currently, the current \minizinc{} implementation cannot reverse any \gls{reif} decisions once they are made. + The current \minizinc{} implementation cannot reverse any \gls{reif} decisions once they are made. And, it also does not consider \gls{half-reif}, a cheaper alternative to \gls{reif} that is often applicable. \item Monolithic \gls{rewriting} is wasteful. @@ -218,9 +218,9 @@ In particular: \section{Research Aims and Contributions} Research into \gls{rewriting} of \cmls{}, as well as model transformation in general, has shown that it is difficult to achieve both high performance and generality. -We address these issues by reconsidering the rewriting process from the ground up to make the transformation efficient while accommodating the optimization techniques to achieve the expected result. +We address these issues by reconsidering the rewriting process from the ground up to make the transformation efficient while accommodating the optimization techniques required to produce high-quality \gls{slv-mod}. In order to adapt \cmls{} for modern day requirements, this thesis aims to \textbf{design, implement, and evaluate a modern architecture for functional \cmls{}}. -Crucially, this architecture should allow us to: +Crucially, this architecture will allow us to: \begin{itemize} @@ -258,7 +258,7 @@ Overall, this thesis makes the following contributions. This thesis is arranged into the following chapters. -Succeeding this introductory chapter, \emph{\cref{ch:background}} gives an overview of the area of \cmls{}. +\emph{\Cref{ch:background}} gives an overview of the area of \cmls{}. It introduces the reader to \minizinc{}, how its models are formulated and how they are translated to \glspl{slv-mod}. Then, we review different solving methods such as \gls{sat}, \gls{mip}, and \gls{cp}. This is followed by a comparison of \minizinc{} with other \cmls{}. @@ -276,15 +276,15 @@ We compare the performance of an implementation of the presented architecture ag \emph{\Cref{ch:half-reif}} continues on the path of improving \glspl{slv-mod}. In this chapter, we present a formal analysis technique to reason about \gls{reif}. This analysis can help us decide whether a \constraint{} has to be reified. -In addition, the analysis allows us to determine whether we use \gls{half-reif}. +In addition, the analysis allows us to determine whether to use \gls{half-reif}. We thus present the first implementation of automatic \gls{half-reif}. We conclude this chapter by analysing the impact of \gls{half-reif} for different types of \solvers{}. \emph{\Cref{ch:incremental}} focuses on the development of incremental methods for \cmls{}. -We first present a novel technique that eliminates the need for the incremental \gls{rewriting}. +We first present a novel technique that eliminates the need for incremental \gls{rewriting}. Instead, it integrates a \gls{meta-optimization} specification, written in the \minizinc{} language, into the \gls{slv-mod}. Then, we describe a technique to optimize the \gls{rewriting} process for incremental changes to an \instance{}. -This method prevents the repeated \gls{rewriting} for parts of the \instance{} that remain unchanged. +This method prevents the repeated \gls{rewriting} of parts of the \instance{} that remain unchanged. We conclude this chapter by testing the performance and computational overhead of these two techniques. Finally, \emph{\Cref{ch:conclusions}} is the concluding chapter of the thesis.