diff --git a/assets/bibliography/references.bib b/assets/bibliography/references.bib index df257c7..787a35f 100644 --- a/assets/bibliography/references.bib +++ b/assets/bibliography/references.bib @@ -265,6 +265,21 @@ year = 2020, } +@article{dantzig-1982-simplex, + author = {George B. Dantzig}, + title = {Reminiscences about the origins of linear programming}, + journal = {Oper. Res. Lett.}, + volume = {1}, + number = {2}, + pages = {43--48}, + year = {1982}, + url = {https://doi.org/10.1016/0167-6377(82)90043-8}, + doi = {10.1016/0167-6377(82)90043-8}, + timestamp = {Sun, 02 Jun 2019 20:50:37 +0200}, + biburl = {https://dblp.org/rec/journals/orl/Dantzig82.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org}, +} + @article{davis-1960-dpll, author = {Davis, Martin and Putnam, Hilary}, title = {A Computing Procedure for Quantification Theory}, @@ -547,6 +562,22 @@ bibsource = {dblp computer science bibliography, https://dblp.org}, } +@inproceedings{jaffar-1987-clp, + author = {Joxan Jaffar and Jean{-}Louis Lassez}, + title = {Constraint Logic Programming}, + booktitle = {Conference Record of the Fourteenth Annual {ACM} Symposium on + Principles of Programming Languages, Munich, Germany, January + 21-23, 1987}, + pages = {111--119}, + publisher = {{ACM} Press}, + year = {1987}, + url = {https://doi.org/10.1145/41625.41635}, + doi = {10.1145/41625.41635}, + timestamp = {Tue, 06 Nov 2018 11:07:43 +0100}, + biburl = {https://dblp.org/rec/conf/popl/JaffarL87.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org}, +} + @book{jaillet-2021-online, title = {Online Optimization}, author = {Jaillet, P. and Wagner, M.R.}, @@ -588,6 +619,21 @@ bibsource = {dblp computer science bibliography, https://dblp.org}, } +@article{karmarkar-1984-interior-point, + author = {Narendra Karmarkar}, + title = {A new polynomial-time algorithm for linear programming}, + journal = {Comb.}, + volume = {4}, + number = {4}, + pages = {373--396}, + year = {1984}, + url = {https://doi.org/10.1007/BF02579150}, + doi = {10.1007/BF02579150}, + timestamp = {Wed, 22 Jul 2020 22:02:37 +0200}, + biburl = {https://dblp.org/rec/journals/combinatorica/Karmarkar84.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org}, +} + @article{kolisch-1997-psplib, title = {PSPLIB - A project scheduling problem library: OR Software - ORSEP Operations Research Software Exchange Program}, diff --git a/assets/mzn/back_knapsack.mzn b/assets/mzn/back_knapsack.mzn index 7f7f65c..1947973 100644 --- a/assets/mzn/back_knapsack.mzn +++ b/assets/mzn/back_knapsack.mzn @@ -9,7 +9,7 @@ var set of TOYS: selection;@\Vlabel{line:back:knap:sel}@ var int: total_joy = sum(toy in selection)(toy_joy[toy]);@\Vlabel{line:back:knap:tj}@ % Constraints -constraint sum(toy in selection)(toy_space[toy]) < total_space;@\Vlabel{line:back:knap:con}@ +constraint sum(toy in selection)(toy_space[toy]) <= total_space;@\Vlabel{line:back:knap:con}@ % Goal solve maximize total_joy;@\Vlabel{line:back:knap:obj}@ diff --git a/assets/shorthands.tex b/assets/shorthands.tex index efdf7b6..6f714ed 100644 --- a/assets/shorthands.tex +++ b/assets/shorthands.tex @@ -2,43 +2,43 @@ \renewcommand*{\implies}{\rightarrow} % Academic writing -\newcommand*{\eg}{e.g.,\xspace{}} -\newcommand*{\ie}{i.e.,\xspace{}} +\newcommand*{\eg}{e.g.,\xspace} +\newcommand*{\ie}{i.e.,\xspace} % Glossary entries \newcommand*{\Cmls}{\Glspl{cml}} \newcommand*{\cmls}{\glspl{cml}} \newcommand*{\cml}{\gls{cml}} -\newcommand*{\compiler}{\gls{compiler}\xspace{}} -\newcommand*{\constraint}{\gls{constraint}\xspace{}} -\newcommand*{\Constraint}{\Gls{constraint}\xspace{}} -\newcommand*{\constraints}{\glspl{constraint}\xspace{}} -\newcommand*{\Constraints}{\Glspl{constraint}\xspace{}} -\newcommand*{\domain}{\gls{domain}\xspace{}} -\newcommand*{\domains}{\glspl{domain}\xspace{}} -\newcommand*{\flatzinc}{\gls{flatzinc}\xspace{}} -\newcommand*{\interpreter}{\gls{interpreter}\xspace{}} -\newcommand*{\instance}{\gls{instance}\xspace{}} -\newcommand*{\instances}{\glspl{instance}\xspace{}} -\newcommand*{\microzinc}{\gls{microzinc}\xspace{}} -\newcommand*{\minisearch}{\gls{minisearch}\xspace{}} -\newcommand*{\minizinc}{\gls{minizinc}\xspace{}} -\newcommand*{\cmodel}{\gls{model}\xspace{}} -\newcommand*{\cmodels}[0]{\glspl{model}\xspace{}} -\newcommand*{\nanozinc}{\gls{nanozinc}\xspace{}} -\newcommand*{\parameters}{\glspl{parameter}\xspace{}} -\newcommand*{\parameter}{\gls{parameter}\xspace{}} -\newcommand*{\reified}{\gls{reified}\xspace{}} -\newcommand*{\halfreified}{\gls{half-reified}\xspace{}} -\newcommand*{\solvers}{\glspl{solver}\xspace{}} -\newcommand*{\solver}{\gls{solver}\xspace{}} -\newcommand*{\Solvers}{\Glspl{solver}\xspace{}} -\newcommand*{\Solver}{\Gls{solver}\xspace{}} -\newcommand*{\variable}{\gls{variable}\xspace{}} -\newcommand*{\Variable}{\Gls{variable}\xspace{}} -\newcommand*{\variables}{\glspl{variable}\xspace{}} -\newcommand*{\Variables}{\Glspl{variable}\xspace{}} -\newcommand*{\zinc}{\gls{zinc}\xspace{}} +\newcommand*{\compiler}{\gls{compiler}\xspace} +\newcommand*{\constraint}{\gls{constraint}\xspace} +\newcommand*{\Constraint}{\Gls{constraint}\xspace} +\newcommand*{\constraints}{\glspl{constraint}\xspace} +\newcommand*{\Constraints}{\Glspl{constraint}\xspace} +\newcommand*{\domain}{\gls{domain}\xspace} +\newcommand*{\domains}{\glspl{domain}\xspace} +\newcommand*{\flatzinc}{\gls{flatzinc}\xspace} +\newcommand*{\interpreter}{\gls{interpreter}\xspace} +\newcommand*{\instance}{\gls{instance}\xspace} +\newcommand*{\instances}{\glspl{instance}\xspace} +\newcommand*{\microzinc}{\gls{microzinc}\xspace} +\newcommand*{\minisearch}{\gls{minisearch}\xspace} +\newcommand*{\minizinc}{\gls{minizinc}\xspace} +\newcommand*{\cmodel}{\gls{model}\xspace} +\newcommand*{\cmodels}[0]{\glspl{model}\xspace} +\newcommand*{\nanozinc}{\gls{nanozinc}\xspace} +\newcommand*{\parameters}{\glspl{parameter}\xspace} +\newcommand*{\parameter}{\gls{parameter}\xspace} +\newcommand*{\reified}{\gls{reified}\xspace} +\newcommand*{\halfreified}{\gls{half-reified}\xspace} +\newcommand*{\solvers}{\glspl{solver}\xspace} +\newcommand*{\solver}{\gls{solver}\xspace} +\newcommand*{\Solvers}{\Glspl{solver}\xspace} +\newcommand*{\Solver}{\Gls{solver}\xspace} +\newcommand*{\variable}{\gls{variable}\xspace} +\newcommand*{\Variable}{\Gls{variable}\xspace} +\newcommand*{\variables}{\glspl{variable}\xspace} +\newcommand*{\Variables}{\Glspl{variable}\xspace} +\newcommand*{\zinc}{\gls{zinc}\xspace} % Semantic syntax (rewriting) \renewcommand{\phi}{\varphi} diff --git a/chapters/1_introduction.tex b/chapters/1_introduction.tex index 8dadfa1..22ba317 100644 --- a/chapters/1_introduction.tex +++ b/chapters/1_introduction.tex @@ -24,7 +24,7 @@ For example, \gls{sat} \solvers{} can only reason about Boolean \variables{}, de Its \constraints{} 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{} will find a \gls{sol} for them. +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{}. Two \solvers{} designed to solve the same problem class might perform very differently. @@ -33,7 +33,7 @@ They serve as a level of abstraction between the user and the \solver{}. Instead of providing a flat list of \variables{} and \constraints[], the user can create a \cmodel{} using the more natural syntax of the \cml{}. A \cmodel{} can generally describe a class of problems through the use of \parameters{}, values assigned by external input. Once given a complete assignment of the \parameters{}, the \cmodel{} forms an \instance{}. -The language will then create a \gls{slv-mod}, through a process called \gls{rewriting}, and interface with the \solver{} when trying to find an appropriate \gls{sol}. +The language then creates a \gls{slv-mod}, through a process called \gls{rewriting}, and interface with the \solver{} when trying to find an appropriate \gls{sol}. A commonly used \cml{} is \glsxtrshort{ampl} \autocite{fourer-2003-ampl}. \glsxtrshort{ampl} was originally designed as a common interface between different \gls{mip} \solvers{}. @@ -97,7 +97,7 @@ For example, the concepts of one task preceding another and non-overlapping of t The definition of \mzninline{nonoverlap} require that either task A precedes task B, or vice versa. However, unlike the \gls{ampl} model, Prolog would not provide this choice to the \solver{}. -Instead, it will enforce one, test if this works, and otherwise enforce the other. +Instead, it enforces one, test if this works, and otherwise enforce the other. This is a powerful mechanism where any 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{}. @@ -117,7 +117,7 @@ For example, a user could create a \minizinc{} function to express the non-overl \end{mzn} Fundamentally, in its \gls{rewriting} process \minizinc{} is a functional language. -It will continuously evaluate the calls in a \minizinc{} \instance{} until it reaches \gls{native} \constraints{}. +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 computational language. @@ -260,7 +260,7 @@ 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 an formal analysis technique to reason about \gls{reif}. -This analysis can help us decide whether a \constraint{} will have to be reified. +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}. We thus present the first implementation of the usage of automatic \gls{half-reif}. We conclude this chapter by analysing the impact of the usage of \gls{half-reif} for different types of \solvers{}. diff --git a/chapters/2_background.tex b/chapters/2_background.tex index a9d70ec..d58bbf6 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -20,10 +20,10 @@ Consequently, in current times, writing a computer program requires little knowl The modeller does not describe how to solve a problem, but rather formalises the requirements of the problem. It could be said that a \cmodel{} actually describes the answer to the problem. -In a \cmodel{}, instead of specifying the manner in which we can find the \gls{sol}, we give a concise description of the problem. -The elements of a \cmodel include \parameters{}, what we already know; \variables{}, what we wish to know; and \constraints{}, the relationships that should exist between them. -Through the variation of \parameters{}, a \cmodel{} can describe a full class of problems. -A specific problem is captured by a \instance{}, the combination of a \cmodel{} with a complete \gls{parameter-assignment} (\ie{}, a mapping from all parameters to values). +In a \cmodel{}, instead of specifying the manner in which we find a \gls{sol}, we give a concise description of the problem. +The elements of a \cmodel{} include \parameters{}, what we already know; \variables{}, what we wish to know; and \constraints{}, the relationships that should exist between them. +Through the variation of \parameters{}, a \cmodel{} describes a full class of problems. +A specific problem is captured by a \instance{}, the combination of a \cmodel{} with a complete \gls{parameter-assignment} (\ie{} a mapping from all parameters to values). The type of problem described by a \cmodel{} is called a \gls{dec-prb}. The goal of a \gls{dec-prb} is to find a \gls{sol}: an complete \gls{variable-assignment} that satisfy the \constraints{}. @@ -31,6 +31,8 @@ Or, when this is not possible, prove that no such \gls{assignment} exists. Many \cmls{} also support the modelling of \gls{opt-prb}, where a \gls{dec-prb} is augmented with an \gls{objective}. In this case the goal is to find a \gls{sol} that satisfies all \constraints{} while minimising (or maximising) the value of the \gls{objective}. +\todo{figure that visualises how \cmodels{} + assignments becomes \instance{}, and then rewritten to \gls{slv-mod} and given to a solver.} + Although a \cmodel{} does not contain any instructions on how to find a suitable \gls{sol}, \instances{} of \cmodels{} can generally be given to a dedicated \solver{}. The \solver{} uses a dedicated algorithm that finds a \gls{sol} that fits the requirements of the \instance{}. @@ -39,7 +41,7 @@ The \solver{} uses a dedicated algorithm that finds a \gls{sol} that fits the re As an example, let us consider the following scenario: Packing for a weekend trip, I have to decide which toys to bring for my dog, Audrey. We only have a small amount of space left in the car, so we cannot bring all the toys. - Since Audrey enjoys playing with some toys more than others, we can now try and pick the toys that bring Audrey the most amount of joy, but still fit in the car. + Since Audrey enjoys playing with some toys more than others, we try and pick the toys that bring Audrey the most amount of joy, but still fit in the car. The following set of equations describe this knapsack problem as an \gls{opt-prb}: \begin{equation*} @@ -52,13 +54,13 @@ The \solver{} uses a dedicated algorithm that finds a \gls{sol} that fits the re \end{equation*} In these equations \(S\) is a set \variable{}. - It represents the selection of toys that will be packed for the trip. - The \gls{objective} is evaluates the quality of the \gls{sol} through the \variable{} \(z\). + It represents the selection of toys to be packed for the trip. + The \gls{objective} evaluates the quality of the \gls{sol} through the \variable{} \(z\). And, \(z\) is bound to the amount of joy that the selection of toys will bring. This is to be maximised. The \parameter{} \(T\) is the set of all available toys. - The \(joy\) and \(space\) functions are \parameters{} used to map toys, \( t \in T\), to a value depicting the amount of enjoyment and space required respectively. - Finally, the \parameter{} \(C\) depicts the total space that is left in the car before packing the toys. + The \(joy\) and \(space\) functions are \parameters{} used to map toys, \( t \in T\), to a numeric value describing the amount of enjoyment and space required respectively. + Finally, the \parameter{} \(C\) gives the numeric value of the total space that is left in the car before packing the toys. This \cmodel{} gives an abstract mathematical definition of the \gls{opt-prb} that would be easy to adjust to changes in the requirements. To solve \instances{} of this problem, however, these \instances{} have to be rewritten into input accepted by a \solver{}. @@ -73,7 +75,7 @@ The \solver{} uses a dedicated algorithm that finds a \gls{sol} that fits the re \section{\glsentrytext{minizinc}}% \label{sec:back-minizinc} -\minizinc{} is a high-level, solver- and data-independent modelling language for discrete satisfiability and optimisation problems \autocite{nethercote-2007-minizinc}. +\minizinc{} is a high-level, \solver{}- and data-independent \cml{} for discrete decision and \glspl{opt-prb} \autocite{nethercote-2007-minizinc}. Its expressive language and extensive library of \glspl{global} allow users to easily model complex problems. \begin{example}% @@ -83,10 +85,10 @@ Its expressive language and extensive library of \glspl{global} allow users to e A \minizinc{} model encoding this problem is shown in \cref{lst:back-mzn-knapsack}. The model starts with the declaration of the \parameters{}. - \Lref{line:back:knap:toys} declares an enumerated type that represents all possible toys, \(T\) in the mathematical model in the example. - \Lrefrange{line:back:knap:joy}{line:back:knap:space} declare arrays that map toys to integer values. + \Lref{line:back:knap:toys} declares the enumerated type \mzninline{TOYS} that represents all possible toys, \(T\) in the mathematical model in \cref{ex:back-knapsack}. + \Lrefrange{line:back:knap:joy}{line:back:knap:space} declare the arrays \mzninline{toy_joy} and \mzninline{toy_space}, that map toys to integer values. These represent the functional mappings \(joy\) and \(space\). - Finally, \lref{line:back:knap:left} declares an integer \parameter{} to represent the car capacity as an equivalent to \(C\). + Finally, \lref{line:back:knap:left} declares the integer \parameter{} \mzninline{total_space} to represent the remaining car capacity, equivalent to \(C\). The model then declares its \variables{}. \Lref{line:back:knap:sel} declares the main \variable{} \mzninline{selection}, which represents the selection of toys to be packed. @@ -104,14 +106,14 @@ Its expressive language and extensive library of \glspl{global} allow users to e One might note that, although more textual and explicit, the \minizinc\ model definition is very similar to our earlier mathematical definition. -A \minizinc{} model cannot be solved solved directly. +A \minizinc{} model cannot be solved directly. It first need to be transformed into a \gls{slv-mod}: a list of \variables{} and \constraints{} \gls{native} to the \solver{}. Type of \variables{} and \constraints{} are said to be \gls{native} to the \solver{} when they are directly supported as input to the \solver{}. -Given complete \gls{parameter-assignment}, a \minizinc{} model can form a \minizinc{} instance. +Given complete \gls{parameter-assignment}, a \minizinc{} model forms a \minizinc{} instance. The process to transform a \minizinc{} instance into a \gls{slv-mod} is a called \gls{rewriting}. \Glspl{slv-mod} for \minizinc{} \solvers{} are generally represented in \flatzinc{}. -\flatzinc{} can be seen as a strict subset of \minizinc{} specifically chosen to represent \glspl{slv-mod}. +\flatzinc{} is a strict subset of \minizinc{} specifically chosen to represent \glspl{slv-mod}. It is the primary way in which \minizinc{} communicates with \solvers{}. \begin{example} @@ -137,7 +139,7 @@ It is the primary way in which \minizinc{} communicates with \solvers{}. [63,12,100,-1], [selection_0,selection_1,selection_2,total_joy], 0 - ):: defines_var(total_joy); + ); solve maximize total_joy; \end{mzn} @@ -150,7 +152,7 @@ It is the primary way in which \minizinc{} communicates with \solvers{}. \subsection{Model Structure}% \label{subsec:back-mzn-structure} -The structure of a \minizinc{} model can generally be described directly in terms of a \cmodel{}: +The structure of a \minizinc{} model can be described directly in terms of a \cmodel{}: \begin{itemize} \item \variables{} and \parameters{} are found in the form of value declarations, @@ -160,8 +162,8 @@ The structure of a \minizinc{} model can generally be described directly in term More complex models might also include definitions for custom types, user defined functions, and a custom output format. These items are not constrained to occur in any particular order. -We will briefly discuss the most important model items. -Note that these items will already refer to \minizinc{} expressions, which will be discussed in \cref{subsec:back-mzn-expr}. +We briefly discuss the most important model items. +Note that these items already refer to \minizinc{} expressions, which will be discussed in \cref{subsec:back-mzn-expr}. For a detailed overview of the structure of \minizinc{} models the full syntactic structure of \minizinc{} 2.5.5 can be consulted in \cref{ch:minizinc-grammar}. \textcite{nethercote-2007-minizinc} offer a detailed discussion of the \minizinc{}. And, much of its history can be learned by the description of its predecessor, \zinc{} \autocite{marriott-2008-zinc}. @@ -173,17 +175,17 @@ And, much of its history can be learned by the description of its predecessor, \ \item and the modeller can functionally define the value using an expression \(E\). \end{itemize} The syntax \mzninline{= @\(E\)@} is optional. -It can be omitted when a \variable{} has no functional definition, or when a \parameter{} is assigned externally. +It is omitted when a \variable{} has no functional definition, or when a \parameter{} is assigned externally. The identifier used in a top-level value definition must be unique. -Two declarations with the same identifier will result in an error during the \gls{rewriting} process. +Two declarations with the same identifier result in an error during the \gls{rewriting} process. The main types used in \minizinc{} are Boolean, integer, floating point numbers, sets of integers, and (user-defined) enumerated types. The declaration of \parameters{} and \variables{} are distinguishes through their type. The type of a \variable{} is preceded by the \mzninline{var} keyword. -The type of a \parameter{} can similarly be marked by the \mzninline{par} keyword, but this is not required. -These types can be used both as normal \parameters{} and as \variables{}. +The type of a \parameter{} might similarly be marked by the \mzninline{par} keyword, but this is not required. +These types are used both as normal \parameters{} and as \variables{}. To better structure models, \minizinc{} allows collections of these types to be contained in \glspl{array}. -Unlike other languages, \glspl{array} can have a user defined index set, which can start at any value, but has to be a continuous range. +Unlike other languages, \glspl{array} have a user defined index set, which can start at any value, but they have to be a continuous range. For example, an array going from 5 to 10 of new Boolean \variables{} might be declared as \begin{mzn} @@ -195,25 +197,25 @@ These constrain a declaration, not just to a certain type, but also to a set of This set of values is generally referred to as the \gls{domain} of a \variable{}. In \minizinc{} any expression that has a set type can be used as a type expression. For example, the following two declarations declare two integer \variables{}. -The first can take the values from three to five and the second can take the values one, three, and five. +The first takes the values from three to five and the second takes the values one, three, and five. \begin{mzn} var 3..5: x; var {1,3,5}: y; \end{mzn} -If a declaration does include a functional definition, then the identifier can be seen as merely a name given to the expression. +If a declaration does include a functional definition, then the identifier is merely a name given to the expression. However, if the declaration also includes a type expression, then this places an implicit \constraint{} on the expression. It forces the result of the expression to take a value according to the type expression. \paragraph{Constraint Items} \Constraints{} in a \minizinc{} model are specified using the syntax: \mzninline{constraint @\(E\)@}. A \constraint{} item contains only a single expression \(E\) of Boolean type. -During the \gls{rewriting} of the model the expressions in \constraints{} are translated into versions of the same expression that are \gls{native} to the \solver{}. +The \gls{rewriting} of the model translated the expressions in \constraints{} into versions of the same expression that are \gls{native} to the \solver{}. It is important that the \gls{native} expressions are \gls{eqsat}. This means that the \constraints{} in the \solver{} are only \gls{satisfied} if-and-only-if the original \constraint{} would have been \gls{satisfied}. \paragraph{Solving Goal Item} A \minizinc{} model can contain a single solving goal item. -This item can signal the solver to do one of three actions: +This item signals the solver to do one of three actions: \begin{itemize} \item \mzninline{solve satisfy} --- to find an assignment to the \variables{} that satisfies the constraints, @@ -225,7 +227,7 @@ This item can signal the solver to do one of three actions: The other two types of goals are used when the model describes a \gls{opt-prb}. If the model does not contain a goal item, then it then the problem is assumed to be a satisfaction problem. -\paragraph{Function Items} Common structures in \minizinc\ can be captured using function declarations. +\paragraph{Function Items} Common structures in \minizinc\ are captured using function declarations. Functions are declared using the syntax \mzninline{function @\(T\)@: @\(I\)@(@\(P\)@) = E}, where: \begin{itemize} \item \(T\) is the type of its result; @@ -234,33 +236,33 @@ Functions are declared using the syntax \mzninline{function @\(T\)@: @\(I\)@(@\( \item and \(E\) is the body of the function, an expression that can use the arguments \(P\). \end{itemize} -\noindent{}During \gls{rewriting}, a call to the function is replaced by its body instantiated the arguments given in the call. +\noindent{}\Gls{rewriting} replaces a call to a function by its body instantiated the arguments given in the call. The \minizinc{} language allows users to write the keywords \mzninline{predicate} as a shorthand \mzninline{function var bool} and \mzninline{test} as a shorthand for \mzninline{function bool}. -As an example, we can define a function that squares an integer can be defined as follows. +As an example, we can define a function that squares an integer as follows. \begin{mzn} function int: square(int: a) = a * a; \end{mzn} -During \gls{rewriting} all \minizinc{} expressions are (eventually) transformed into function calls. +\Gls{rewriting} (eventually) transforms all \minizinc{} expressions into function calls. As such, the usage of function declarations is the primary method for \solvers{} to specify how to rewrite a \minizinc{} model into a \gls{slv-mod}. The collection of functions declarations to rewrite for a \solver{} is generally referred to as a \solver{} library. In this library, functions might be declared without a function body. -This marks them as \gls{native} to the solver. -Calls to these functions can be directly placed in the \gls{slv-mod}. -For non-\gls{native} functions, a \solver can provide a function body that rewrites calls into (or towards) \gls{native} functions. -\solver{} implementers are, however, not forced to provide a definition for all functions in \minizinc{}'s extensive library. -Instead, they can rely on a set of standard declaration, known as the standard library, that rewrite functions into a minimal subset of \gls{native} functions, known as the \flatzinc built-ins. +This marks them as \gls{native} to the \solver{}. +Calls to these functions are directly placed in the \gls{slv-mod}. +For non-\gls{native} functions, a \solver{} provides a function body that rewrites calls into (or towards) \gls{native} functions, a \gls{decomp}. +\Solver{} implementers are, however, not forced to provide a definition for all functions in \minizinc{}'s extensive library. +Instead, they might rely on a set of standard declaration, known as the standard library, that rewrite functions into a minimal subset of \gls{native} functions, known as the \flatzinc{} built-ins. \subsection{MiniZinc Expressions}% \label{subsec:back-mzn-expr} One of the powers of the \minizinc{} language is the extensive expression language. -It can help modellers create \cmodels{} that are intuitive to read, but are transformed to fit the structure best suited to the chosen \solver{}. -We will now briefly discuss the most important type of expression in \minizinc{} and the general methods employed when \gls{rewriting} them. +It helps modellers create \cmodels{} that are intuitive to read, but are transformed to fit the structure best suited to the chosen \solver{}. +We now briefly discuss the most important type of expression in \minizinc{} and the possible methods employed when \gls{rewriting} them. -\paragraph{Global Constraints} It could be said that the basic building blocks of the \minizinc{} language are \Glspl{global}. +\paragraph{Global Constraints} It could be said that the basic building blocks of the \minizinc{} language are \glspl{global}. These expressions capture common (complex) relations between \variables{}. \Glspl{global} in the \minizinc{} language are used as function calls. An example of a \gls{global} is @@ -286,14 +288,15 @@ This \gls{global} expresses the knapsack relationship, where the argument: Note that the usage of this \gls{global} might have simplified the \minizinc{} model in \cref{ex:back-mzn-knapsack}: \begin{mzn} - constraint knapsack(toy_space, toy_joy, set2bool(selection), total_joy, space); + var 0..total_space: space_used; + constraint knapsack(toy_space, toy_joy, set2bool(selection), space_used, total_joy); \end{mzn} -\noindent{}This would have the additional benefit that the knapsack structure of the problem is then known to the \solver{}. -It might then use special handling for this relationship. +\noindent{}This has the additional benefit that the knapsack structure of the problem is then known. +The \constraint{} can be rewritten using specialised \gls{decomp} provided by the \solver{} or it might even be marked as \gls{native} \constraint{}. Although \minizinc{} contains an extensive library of \glspl{global}, many problems contain structures that are not covered by a \gls{global}. -There are many other types of expressions in \minizinc{} that can help modellers express complex \constraints{}. +There are many other types of expressions in \minizinc{} that help modellers express complex \constraints{}. \paragraph{Operators} When we express a mathematical formula, we generally do this through the use of \gls{operator} symbols. \minizinc{} includes \glspl{operator} for many mathematical, logic, and set operations. @@ -306,13 +309,13 @@ For example the constraint \noindent{}contains the infix \glspl{operator} \mzninline{+} and \mzninline{<}, and the prefix \gls{operator} \mzninline{not}. \Gls{operator} symbols in \minizinc{} are a shorthand for \minizinc{} functions. -The \glspl{operator} in the above expression will be evaluated using the addition, less-than comparison, and Boolean negation functions respectively. -Although the \gls{operator} syntax for \variables{} and \parameters{} is the same, different (overloaded) versions of these functions will be used during \gls{rewriting}. +The \glspl{operator} in the above expression are evaluated using the addition, less-than comparison, and Boolean negation functions respectively. +Although the \gls{operator} syntax for \variables{} and \parameters{} is the same, different (overloaded) versions of these functions is used during \gls{rewriting}. If the arguments to a function consist of only \parameters{}, then the result of the function can be computed directly. However, \gls{rewriting} functions with \variable{} as arguments result in a new \variable{} to contain its result. -\paragraph{Conditional Expression} The choice between different expressions can often be expressed using a \gls{conditional} expression, also known as an ``if-then-else'' expressions. -You could, for example, force that the absolute value of \mzninline{a} is bigger than \mzninline{b} using the constraint +\paragraph{Conditional Expression} The choice between different expressions are often expressed using a \gls{conditional} expression, also known as an ``if-then-else'' expression. +You could, for example, force that the absolute value of \mzninline{a} is bigger than \mzninline{b} using the constraint as follows. \begin{mzn} constraint if a >= 0 then a > b else b < a endif; @@ -320,7 +323,7 @@ You could, for example, force that the absolute value of \mzninline{a} is bigger The result of a \gls{conditional} expression is not contained to Boolean types. The condition in the expression, the ``if'', must be of a Boolean type, but as long as the different sides of the \gls{conditional} expression are the same type it is a valid conditional expression. -This can be used to, for example, define an absolute value function for integer \parameter{}: +This can be used to, for example, define an absolute value function for integer \parameter{} as follows. \begin{mzn} function int: abs(int: a) = @@ -332,16 +335,16 @@ If, however, the condition does contain a \variable{}, then the result of the ex Instead, an \gls{ivar} is created and a \constraint{} is added to ensure that it takes the correct value. A special \mzninline{if_then_else} \glspl{global} are available to implement this relationship. -\paragraph{Array access} For the selection of an element from an \gls{array} the \minizinc{} language uses an \gls{array} access syntax similar to most other computer languages. +\paragraph{Array Access} For the selection of an element from an \gls{array} the \minizinc{} language uses an \gls{array} access syntax similar to most other computer languages. The expression \mzninline{a[i]} selects the element with index \mzninline{i} from the array \mzninline{a}. Note this is not necessarily the \(\mzninline{i}^{\text{th}}\) element because \minizinc{} allows modellers to provide a custom index set. The selection of an element from an \gls{array} is in many way similar to the choice in a \gls{conditional} expression. Like a \gls{conditional} expression, the selector \mzninline{i} can be both a \parameter{} or a \variable{}. If the expression is a \gls{variable}, then the expression is rewritten to an \gls{ivar} and an \mzninline{element} \constraint{}. -Otherwise, the \gls{rewriting} will replace the \gls{array} access expression by the chosen element of the \gls{array}. +Otherwise, the \gls{rewriting} replaces the \gls{array} access expression by the chosen element of the \gls{array}. -\paragraph{Comprehensions} \Gls{array} \glspl{comprehension} are expressions can be used to compose \gls{array} objects. +\paragraph{Comprehensions} \Gls{array} \glspl{comprehension} are expressions which are used to compose \gls{array} objects. The generation of new \gls{array} structures allows modellers adjust, combine, filter, or order values from within the \minizinc{} model. \Gls{generator} expressions, \mzninline{[@\(E\)@ | @\(G\)@ where @\(F\)@]}, consist of three parts: @@ -349,7 +352,7 @@ The generation of new \gls{array} structures allows modellers adjust, combine, f \begin{description} \item[\(G\)] The generator expression which assigns the values of collections to identifiers, \item[\(F\)] an optional filtering condition, which has to evaluate to \mzninline{true} for the iteration to be included in the array, - \item[\(E\)] and the expression that is evaluation for each iteration when the filtering condition succeeds. + \item[\(E\)] and the expression that is evaluated for each iteration when the filtering condition succeeds. \end{description} The following example composes an \gls{array} that contains the tripled even values of an \gls{array} \mzninline{x}. @@ -358,20 +361,20 @@ The following example composes an \gls{array} that contains the tripled even val [ xi * 3 | xi in x where x mod 2 == 0] \end{mzn} -During \gls{rewriting}, the instantiation of the expression with current generator values will be added to the new \gls{array}. -This means that the type of the \gls{array} will primarily depend on the type of the expression. +During \gls{rewriting}, the instantiation of the expression with current generator values is added to the new \gls{array}. +This means that the type of the \gls{array} primarily depends on the type of the expression. However, in recent versions of \minizinc{} both the collections over which we iterate and the filtering condition could have a \variable{} type. -Since we then cannot decide during \gls{rewriting} if an element is present in the array, the elements will be made of an \gls{optional} type. +Since we then cannot decide during \gls{rewriting} if an element is present in the array, the elements are made of an \gls{optional} type. This means that the \solver{} still will decide if the element is present in the array or if it takes a special ``absent'' value (\mzninline{<>}). \paragraph{Let Expressions} Together with function definitions, \glspl{let} are the primary scoping mechanism in the \minizinc{} language. A \gls{let} allows a modeller to provide a list of declarations, that can only be used in its resulting expression. -Additionally, a \gls{let} can contain \constraints{} to constrain the declared values. +Additionally, a \gls{let} might contain \constraints{} to constrain the declared values. There are three main purposes for \glspl{let}: \begin{enumerate} - \item To name an intermediate expression, so it can be used multiple times or to simplify the expression. + \item To name an intermediate expression, for it to be used multiple times or to simplify the expression. For example, the \constraint{} \begin{mzn} @@ -403,29 +406,29 @@ There are three main purposes for \glspl{let}: \end{enumerate} An important detail in \gls{rewriting} \glspl{let} is that any \variables{} that are introduced might need to be renamed in the resulting \gls{slv-mod}. -Different \variables{} declared directly in declaration items, the \variables{} declared in \glspl{let} can be flattened multiple times when used in loops, function definitions (that are called multiple times), and \gls{array} \glspl{comprehension}. +Different \variables{} declared directly in declaration items, the \variables{} declared in \glspl{let} might be flattened multiple times when used in loops, function definitions (that are called multiple times), and \gls{array} \glspl{comprehension}. The \gls{rewriting} process must assign any \variables{} in the \gls{let} a new name and use this name in any subsequent definitions and in the resulting expression. -\paragraph{Annotations} Although \minizinc{} does not typically prescribe a way to find the \gls{sol} for an \instance{}, it does provide the modeller a way to give hints to the \solver{}. +\paragraph{Annotations} Although \minizinc{} does not typically prescribe a way to find the \gls{sol} for an \instance{}, it does provide the modeller a way to give ``hints'' to the \solver{}. It does this through the use of \glspl{annotation}. Any item or expression can be annotated. An annotation is indicated by the \mzninline{::} \gls{operator} followed by an identifier or function call. The same syntax can be repeated to place multiple \glspl{annotation} on the same item or expression. A common use of \glspl{annotation} in \minizinc{} is to provide a search heuristic. -Through the use of an \gls{annotation} on the solving goal item, the modeller can express an order in which they think values should be tried for the \variables{} in the model. +Through the use of an \gls{annotation} on the solving goal item, the modeller can express an order in which they think values should be tried for an arrangement of \variables{} in the model. \subsection{Reification}% \label{subsec:back-reif} -With the rich expression language in \minizinc{}, \constraints{} can consist of complex expressions that do result in a single \constraint{} in the \gls{slv-mod}. -Instead, different parts of a complex expression will be rewritten into different \constraints{}. -Not all of these \constraints{} will be globally enforced by the solver. -\constraints{} stemming for sub-expressions will typically be \reified{} into a Boolean variable. +With the rich expression language in \minizinc{}, \constraints{} can consist of complex expressions that cannot be rewritten into a single \constraint{} in the \gls{slv-mod}. +Different parts of a complex expression are rewritten into different \constraints{}. +However, not all part of the expression are autonomous \constraints{} that can be directly enforced by the solver. +Some parts might have to be \reified{} into a Boolean variable. The \gls{reif} of a \constraint{} \(c\) creates an \gls{ivar} \mzninline{b} constrained to be the truth-value of this \constraint{}: \(\texttt{b} \leftrightarrow{} c\). \begin{example} - Consider the \minizinc\ model: + Consider the following \minizinc{} model. \begin{mzn} array[1..10] of var 1..15: x; @@ -436,17 +439,17 @@ The \gls{reif} of a \constraint{} \(c\) creates an \gls{ivar} \mzninline{b} cons This model maximises the number of even numbers taken by the elements of the array \mzninline{x}. In this model the expression \mzninline{x[i] mod 2 == 0} has to be reified. Since the elements have a domain from 1 to 15 and are constrained to take different values, not all elements of \mzninline{x} can take even values. - Instead, the solver is tasked to maximise the number of reified variables it can set to \mzninline{true}. + Instead, the solver is tasked to maximise the number of reified variables it sets to \mzninline{true}. \end{example} -When an expression occurs in a position where it can be globally enforced, we say it occurs in \rootc{}. -Contrarily, an expression that occurs in non-\rootc{} will be reified during the \gls{rewriting} process. +When an expression occurs in a position where it can be directly enforced, we say it occurs in \rootc{} context. +Contrarily, an expression that occurs in non-\rootc{} is reified during the \gls{rewriting} process. In \minizinc{}, almost all expressions can be used in both \rootc{} and non-\rootc{} contexts. \subsection{Handling Undefined Expressions}% \label{subsec:back-mzn-partial} -In this section we will discuss the handling of partial expressions in \cmls{} as studied by Frisch and Stuckey \autocite*{frisch-2009-undefinedness}. +In this subsection we discuss the handling of partial expressions in \cmls{} as studied by \textcite{frisch-2009-undefinedness}. Some expressions in \cmls{} do not have well-defined results. Part of the semantics of a \cml{} is the choice as to how to treat these partial functions. @@ -461,7 +464,7 @@ Part of the semantics of a \cml{} is the choice as to how to treat these partial \noindent{}which requires that if \mzninline{i} takes a value less or equal to four, then the value in the \texttt{i}\(^{th}\) position of array \mzninline{a} multiplied by \mzninline{x} must be at least 6. Suppose the array \texttt{a} has index set \mzninline{1..5}, but \texttt{i} takes the value \texttt{7}. - The expression \mzninline{a[i]} will fail and no \gls{sol} will be found. + The expression \mzninline{a[i]} fails and no \gls{sol} is found. However, intuitively if \mzninline{i = 7} the constraint should be trivially true. \end{example} @@ -489,7 +492,7 @@ Other examples of \minizinc{} expressions that result in partial functions are: \end{itemize} The existence of undefined expressions can cause confusion in \cmls{}. -There is both the question of what happens when an undefined expression is evaluated and at what point during the process undefined values will be resolved, during \gls{rewriting} or by the \solver{}. +There is both the question of what happens when an undefined expression is evaluated and at what point during the process undefined values are resolved, during \gls{rewriting} or by the \solver{}. Frisch and Stuckey define three semantic models to deal with the undefinedness in \cmls: @@ -497,18 +500,18 @@ Frisch and Stuckey define three semantic models to deal with the undefinedness i \item[Strict] \Cmls{} employing a \gls{strict-sem} do not allow any undefined behaviour during the evaluation of the \cmodel{}. If during the \gls{rewriting} or solving process an expression is found to be undefined, then any expressions in which it is used is also marked as undefined. - Consequently, this means that the occurrence of a single undefined expression will cause the full \instance{} to be undefined. + Consequently, this means that the occurrence of a single undefined expression causes the full \instance{} to be undefined. \item[Kleene] The \gls{kleene-sem} treats undefined expressions as expressions for which not enough information is available. - If an expression contains undefined sub-expression, then it will only be marked as undefined if the value of the sub-expression is required to compute its result. + If an expression contains undefined sub-expression, then it is only marked as undefined if the value of the sub-expression is required to compute its result. Take for example the expression \mzninline{false -> @\(E\)@}. - When \(E\) is undefined the result of the expression can still be said to be \mzninline{true}, since the value of \(E\) does not influence the result of the expression. + When \(E\) is undefined the result of the expression is still be said to be \mzninline{true}, since the value of \(E\) does not influence the result of the expression. However, if we take the expression \mzninline{true /\ @\(E\)@}, then when \(E\) is undefined the overall expression is also undefined since the value of the expression cannot be determined. \item[Relational] The \gls{rel-sem} follows from all expressions in a \cml{} eventually becoming part of a relational \constraint{}. So even though a (functional) expression in itself might not have a well-defined result, we can still decide whether its surrounding relationship holds. - For example, the expression \mzninline{x div 0} is undefined, but the relationship \mzninline{int_div(x, 0, y)} can be said to be \mzninline{false}. - It can be said that the relational semantic will make the closest relational expression that contains an undefined expression \mzninline{false}. + For example, the expression \mzninline{x div 0} is undefined, but the relationship \mzninline{int_div(x, 0, y)} is said to be \mzninline{false}. + It can be said that the relational semantic makes the closest relational expression that contains an undefined expression \mzninline{false}. \end{description} @@ -532,22 +535,22 @@ This essentially eliminates the existence of undefined expressions in the \gls{s \section{Solving Constraint Models}% \label{sec:back-solving} -There are many prominent techniques to solve a \constraint{} model, but none of them will solve a \minizinc{} instance directly. +There are many prominent techniques to solve a \constraint{} model, but none of them solve \minizinc{} instances directly. Instead, a \minizinc{} instance is rewritten into a \gls{slv-mod} containing only \constraints{} and types of \variables{} that are \gls{native} to the \solver{}. \minizinc{} was initially designed as an input language for \gls{cp} \solvers{}. These \glspl{solver} often directly support many of the \glspl{global} in a \minizinc{} model. -For \gls{cp} solvers the amount of \gls{rewriting} required can vary a lot. +For \gls{cp} solvers the amount of \gls{rewriting} required varies a lot. It depends on which \constraints{} are \gls{native} to the targeted \gls{cp} \solver{} and which \constraints{} have to be decomposed. In some ways \gls{cp} \solvers{} work on a similar level as the \minizinc{} language. -Therefore, some techniques used in \gls{cp} \solvers{} can also be used during the \gls{rewriting} process. -The usage of these techniques can shrink the \domains{} of \variables{} and eliminate or simplify \constraint{}. +Therefore, some techniques used in \gls{cp} \solvers{} are also used during the \gls{rewriting} process. +The usage of these techniques shrinks the \domains{} of \variables{} and eliminates or simplifies \constraint{}. \Cref{subsec:back-cp} explains the general method employed by \gls{cp} \solvers{} to solve a \cmodel{}. Throughout the years \minizinc{} has started targeting \solvers{} using different approaches. Although these \solvers{} allow new classes of problems that to be solved using \minizinc{}, they also bring new challenges to the \gls{rewriting} process. -To understand these \gls{rewriting} challenges, the remainder of this section will discuss the other dominant technologies used by \minizinc{} \solver{} and their \glspl{slv-mod}. +To understand these \gls{rewriting} challenges, the remainder of this section discusses the other dominant technologies used by \minizinc{} \solver{} and their \glspl{slv-mod}. \subsection{Constraint Programming}% \label{subsec:back-cp} @@ -567,40 +570,39 @@ It is clear that when the value \mzninline{a} is known, then the value of \mznin Therefore, only that one value for \mzninline{b} has to be tried. \gls{cp} is the idea of solving \glspl{csp} by performing an intelligent search by inferring which values are still feasible for each \variable{} \autocite{rossi-2006-cp}. -A \gls{cp} \solver{} will perform a depth first search. +A \gls{cp} \solver{} performs a depth first search. Using a mechanism called \gls{propagation} the \solver{} removes values from \domains{} that are no longer possible. \Gls{propagation} works through the use of \glspl{propagator}: algorithms dedicated to a specific \constraint{} that prune \domains{} when its contains values that are proven to be inconsistent. This mechanism can be very efficient because a \gls{propagator} only has to be run again if the \domains{} of one of its \variables{} has changed. -In the best case scenario, \gls{propagation} will eliminate all impossible values and all \variables{} have been \gls{fixed} to a single value. +In the best case scenario, \gls{propagation} eliminates all impossible values and all \variables{} have been \gls{fixed} to a single value. In this case we have arrived at a \gls{sol}. -Often, \gls{propagation} alone will not be enough to find a \gls{sol} and we reach a \gls{fixpoint}, where no more \glspl{propagator} are triggered. +Often, \gls{propagation} alone is not enough to find a \gls{sol} and we reach a \gls{fixpoint}, where no more \domain{} reductions are performed. The \solver{} then has to make a search decision. -It will fix a \variable{} to a value or add a new \constraint{}. +It fixes a \variable{} to a value or adds a new \constraint{}. This search decision is an assumption made by the \solver{} in the hope of finding a \gls{sol}. If no \gls{sol} is found using the search decision, then it needs to try making the opposite decision which requires the exclusion of the chosen value or adding the opposite \constraint{}. Note that there is an important difference between values excluded by \gls{propagation} and making search decisions. -Values excluded by propagation are guaranteed to not occur in any \gls{sol} -Whereas, values excluded by a search heuristic are merely removed locally and might still be part of a \gls{sol}. +Values excluded by propagation are guaranteed to not occur in any \gls{sol}, whereas, values excluded by a search heuristic are merely removed locally and might still be part of a \gls{sol}. A \gls{cp} \solver{} is only able to prove that the \instance{} is \gls{unsat} by trying all possible search decisions. \Gls{propagation} is not only used when starting the search, but also after making each search decision. This means that some \gls{propagation} depends on the search decision. Therefore, if the \solver{} needs to reconsider a search decision, then it must also undo all \domain{} changes that were caused by \gls{propagation} dependent on that search decision. -The most common method in \gls{cp} \solvers{} to to keep track of \gls{domain} changes using a \gls{trail}. +The most common method in \gls{cp} \solvers{} to keep track of \gls{domain} changes using a \gls{trail}. Every \domain{} change that is made during \gls{propagation}, after the first search decision, is stored in a list. Whenever a new search decision is made, the current position of the list is tagged. -If the \solver{} now needs to undo a search decision (\ie\ \gls{backtrack}), it can reverse all changes until it reaches the change that is tagged with the search decision. +If the \solver{} now needs to undo a search decision (\ie\ \gls{backtrack}), it reverses all changes until it reaches the change that is tagged with the search decision. Because all changes before the tagged point on the \gls{trail} were made before the search decision was made, it is guaranteed that these \domain{} changes do not depend on the search decision. Furthermore, because \gls{propagation} is performed to a \gls{fixpoint}, it is guaranteed that no duplicate \gls{propagation} is required. The solving method used by \gls{cp} \solvers{} is very flexible. A \solver{} can support many types of \variables{}: they can range from Boolean, floating point numbers, and integers, to intervals, sets, and functions. Similarly, \solvers{} do not all have access to the same \glspl{propagator}. -Therefore, a \gls{slv-mod} for one \solver{} might look very different from a \gls{eqsat} \gls{slv-mod} for a different solver. -\cmls{}, like \minizinc{}, can serve as a standardised form of input for these \solvers{}. +Therefore, a \gls{slv-mod} for one \solver{} might look very different from an \gls{eqsat} \gls{slv-mod} for a different \solver{}. +\cmls{}, like \minizinc{}, serve as a standardised form of input for these \solvers{}. They allow modellers to use always use \glspl{global} and depending on the \solver{} they are either used directly, or they are automatically rewritten using a \gls{decomp}. \begin{example}% @@ -608,7 +610,7 @@ They allow modellers to use always use \glspl{global} and depending on the \solv As an example of the \gls{propagation} mechanism, let us consider as an example 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. Meaning only 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; @@ -621,19 +623,19 @@ They allow modellers to use always use \glspl{global} and depending on the \solv constraint all_different([q[i] - i | i in COL]); \end{mzn} - The \variables{} in the \gls{array} \mzninline{q} decide for each column in which row the queen will be placed. + The \variables{} in the \gls{array} \mzninline{q} decide for each column in which row the queen is placed. This automatically restrict every column to only have a single queen. As such, no queen will be able to attack vertically. The \constraints{} in the model the remaining rules of the problem: no two queens can be placed in the same row, no two queen can be place in the same upward diagonal, and no two queens can be place in the same downward diagonal. This model can be directly used in most \gls{cp} \solvers{}, since integer \variables{} and an \mzninline{all_different} \gls{propagator} are common. When solving the problem, initially no values can be eliminated from the \glspl{domain} of the \variables{}. - The first propagation will happen when the first queen is placed on the board, the first search decision. + The first propagation happens when the first queen is placed on the board, the first search decision. \Cref{fig:back-nqueens} visualises the \gls{propagation} after placing a queen on the d3 square of an eight by eight chessboard. When the queen it placed on the board in \cref{sfig:back-nqueens-1}, it fixes the value of column 4 (d) to the value 3. This implicitly eliminates any possibility of placing another queen in the column. Fixing the \domain{} of the column triggers the \glspl{propagator} of the \mzninline{all_different} \constraints{}. - As show in \cref{sfig:back-nqueens-2}, the first \mzninline{all_different} constraint can now stop other queens to be placed in the same column. + As show in \cref{sfig:back-nqueens-2}, the first \mzninline{all_different} constraint now stops other queens from being placed in the same column. It eliminates the value 3 from the domains of the queens in the remaining columns. Similarly, the other \mzninline{all_different} constraints remove all values that correspond to positions on the same diagonal as the placed queen, shown in \cref{sfig:back-nqueens-3,sfig:back-nqueens-4}. @@ -672,7 +674,7 @@ The golden standard for a \gls{propagator} is to be \gls{domain-con}. A \gls{domain-con} \gls{propagator} leaves only values in the \domains{} when there is at least one possible \gls{variable-assignment} that satisfies its \constraint{}. Designing such a \gls{propagator} is, however, not an easy task. The algorithm might require high computational complexity. -Instead, it can sometimes be better to use a propagator with a lower level of consistency. +Instead, it is sometimes be better to use a propagator with a lower level of consistency. Although it might not eliminate all possible values of the domain, searching the values that are not eliminated might take less time than achieving \gls{domain-con}. This is, for example, the case for integer linear constraints: \[ \sum_{i} c_{i} x_{i} = d\] where \(c_{i}\) and \(d\) are integer \parameters{} and \(x_{i}\) are integer \variable{}. @@ -681,7 +683,7 @@ Instead, \solvers{} generally use a \gls{bounds-con} \gls{propagator}, which gua Thus far, we have only considered finding \glspl{sol} for \glspl{dec-prb}. \gls{cp} solving can, however, also be used to solve \gls{opt-prb} using a method called \gls{bnb}. -The \gls{cp} \solver{} will follow the same method as previously described. +The \gls{cp} \solver{} follows the same method as previously described. However, when it finds a \gls{sol}, it does not yet know if this \gls{sol} is an \gls{opt-sol}. It is merely an incumbent \gls{sol}. The \solver{} must therefore resume its search, but it is no longer interested in just any \gls{sol}, only \glspl{sol} that for which the \gls{objective} returns a better value. @@ -702,9 +704,9 @@ A linear program describes a problem using \constraints{} in the form of linear In general, a linear program can be expressed in the form: \begin{align*} - \text{maximise} \hspace{2em} & \sum_{j=1}^{V} c_{j} x_{j} & \\ - \text{subject to} \hspace{2em} & l_{i} \leq \sum_{j=0}^{V} a_{ij} x_{j} \leq u_{i} & \forall_{i=1}^{C} \\ - & x_{i} \in \mathbb{R} & \forall_{i=1}^{V} + \text{maximise} \hspace{2em} & \sum_{j=1}{V} c_{j} x_{j} & \\ + \text{subject to} \hspace{2em} & l_{i} \leq \sum_{j=0}^{V} a_{ij} x_{j} \leq u_{i} & \forall_{1 \leq{} i \leq{} C} \\ + & x_{i} \in \mathbb{R} & \forall_{1 \leq{} i \leq{} V} \end{align*} \noindent{}where \(V\) and \(C\) represent the number of variables and number of constraints respectively. @@ -713,15 +715,16 @@ The vectors \(l\) and \(u\) respectively contain the lower and upper bounds of t Finally, the \variables{} of the linear program held in the \(x\) vector. For problems that are in the form of a linear program, there are proven methods to find an \gls{opt-sol}. -In 1947 Dantzig introduced the simplex method, that can find the optimal solution of a linear program in worst-case exponential time. -It was questioned whether the same problem could be solved in worst-case polynomial time, until Khachiyan proved this possible when he introduced the first interior point method. +One such method, the simplex method, was first conceived by \textcite{dantzig-1982-simplex} during the second world war. +It finds the optimal solution of a linear program in worst-case exponential time. +It was questioned whether the same problem could be solved in worst-case polynomial time, until \textcite{karmarkar-1984-interior-point} proved this possible through the use of interior point methods. These methods provide the foundation for a harder problem. In \gls{lp} our \variables{} must be continuous. -If we require that one or more take a discrete value (\(x_{i} \in \mathbb{N}\)), then the problem suddenly becomes much harder. +If we require that one or more take a discrete value (\(x_{i} \in \mathbb{Z}\)), then the problem suddenly becomes much harder. The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all} \variables{} must take a discrete value). -Unlike \gls{lp}, there is no algorithm that can solve a mixed integer program in polynomial time. +Unlike \gls{lp}, there is no algorithm that solves a mixed integer program in polynomial time. We can, however, adapt \gls{lp} solving methods to solve a mixed integer program. We do this by treating the mixed integer program as a linear program and find an \gls{opt-sol}. If the integer \variables{} already have discrete values, then we have found an \gls{opt-sol}. @@ -730,23 +733,23 @@ For this \variable{} we create two versions of the linear program: a version whe Both versions are solved to find the best \gls{sol}. The process is repeated recursively until a discrete \gls{sol} is found. -Much of the power of this solving method comes from bounds that can be inferred during the process. +Much of the power of this solving method comes from bounds that are inferred during the process. The \gls{sol} to the linear program provides an upper bound for the solution in the current step of the solving process. Similarly, any discrete \gls{sol} found in an earlier branch of the search process provide a lower bound. -When the upper bound given by the simplex method is lower that the lower bound from an earlier solution, then we know that any discrete \gls{sol} following from the linear program will be strictly worse than the incumbent. +When the upper bound given by the simplex method is lower that the lower bound from an earlier solution, then we know that any discrete \gls{sol} following from the linear program is strictly worse than the incumbent. Over the years \gls{lp} and \gls{mip} \solvers{} have developed immensely. -Modern \solvers{}, such as \gls{cbc} \autocite{forrest-2020-cbc}, \gls{cplex} \autocite{cplex-2020-cplex}, \gls{gurobi} \autocite{gurobi-2021-gurobi}, and \gls{scip} \autocite{gamrath-2020-scip}, can solve many complex problems. +Modern \solvers{}, such as \gls{cbc} \autocite{forrest-2020-cbc}, \gls{cplex} \autocite{cplex-2020-cplex}, \gls{gurobi} \autocite{gurobi-2021-gurobi}, and \gls{scip} \autocite{gamrath-2020-scip}, solve many complex problems. These \solvers{} are therefore prime targets to solve \minizinc{} \instances{}. To solve a \instance{} of a \cmodel{}, it can be encoded as a mixed integer program. This process is known as \gls{linearisation}. It does, however, come with its challenges. Most \constraints{} in a \minizinc{} model are not linear equations. -The translation of a single \constraint{} can introduce many linear \constraints{} and even new \variables{}. -For example, when a \constraint{} reasons about the value that a variable will take, the \gls{linearisation} process introduces indicator variables. +The translation of a single \constraint{} might introduce many linear \constraints{} and even new \variables{}. +For example, when a \constraint{} reasons about the value that a variable takes, the \gls{linearisation} process introduces indicator variables. The indicator variables \(y_{i}\) are \glspl{ivar} that for a \variable{} \(x\) take the value 1 if \(x = i\) and 0 otherwise. -\Constraints{} reasoning about the value of \(x\) can then be rewritten as linear \constraints{} using the \variables{} \(y_{i}\). +\Constraints{} reasoning about the value of \(x\) are then rewritten as linear \constraints{} using the \variables{} \(y_{i}\). \begin{example} @@ -754,14 +757,14 @@ The indicator variables \(y_{i}\) are \glspl{ivar} that for a \variable{} \(x\) The following model shows an integer program of this problem. \begin{align} - \text{given} \hspace{2em} & N = {1,\ldots,n} & \\ - \text{maximise} \hspace{2em} & 0 & \\ - \text{subject to} \hspace{2em} & q_{i} \in N & \forall_{i \in N} \\ - & y_{ij} \in \{0,1\} & \forall_{i,j \in N} \\ + \text{given} \hspace{2em} & N = {1,\ldots,n} & \notag{}\\ + \text{maximise} \hspace{2em} & 0 & \notag{}\\ + \text{subject to} \hspace{2em} & q_{i} \in N & \forall_{i \in N} \notag{}\\ + & y_{ij} \in \{0,1\} & \forall_{i,j \in N} \notag{}\\ \label{line:back-mip-channel} & x_{i} = \sum_{j \in N} j * y_{ij} & \forall_{i \in N} \\ \label{line:back-mip-row} & \sum_{i \in N} y_{ij} \leq 1 & \forall_{j \in N} \\ - \label{line:back-mip-diag1} & \sum_{i,j \in N. i + j =k} y_{ij} \leq 1 & \forall_{k=3}^{2n-1} \\ - \label{line:back-mip-diag2} & \sum_{i,j \in N. i - j =k} y_{ij} \leq 1 & \forall_{k=2-n}^{n-2} + \label{line:back-mip-diag1} & \sum_{i,j \in N: i + j =k} y_{ij} \leq 1 & \forall_{3 \leq{} k \leq{} 2n-1} \\ + \label{line:back-mip-diag2} & \sum_{i,j \in N: i - j =k} y_{ij} \leq 1 & \forall_{2 \leq{} k \leq{} n-2} \end{align} The encoding of this \cmodel{} uses only integers. @@ -781,38 +784,38 @@ The indicator variables \(y_{i}\) are \glspl{ivar} that for a \variable{} \(x\) The study of the \gls{sat} problem might be one of the oldest in computer science. The DPLL algorithm that is used to this day stems from the 60s \autocite{davis-1960-dpll, davis-1962-dpll}, and \gls{sat} was the first problem to be proven to be \gls{np}-complete \autocite{cook-1971-sat}. The problem asks if there is an \gls{assignment} for the \variables{} of a given Boolean formula, such that the formula is \gls{satisfied}. -This problem can be seen as a restriction of the general \gls{dec-prb} where \variables{} can only be of a Boolean type. +This problem is a restriction of the general \gls{dec-prb} where all \variables{} have a Boolean type. There is a field of research dedicated to solving \gls{sat} problems \autocite{biere-2021-sat}. In this field a \gls{sat} problem is generally standardised to be in \gls{cnf}. A \gls{cnf} is formulated in terms of literals. These are Boolean \variables{} \(x\) or their negations \(\neg x\). -These literals are then used in a conjunction of disjunctive clauses: a Boolean formula in the form \(\forall_{i \in P} \exists_{b \in C_{i}} b\). +These literals are then used in a conjunction of disjunctive clauses: a Boolean formula in the form \(\forall \exists b_{i}\). To solve the \gls{sat} problem, the \solver{} has to find an \gls{assignment} for the \variables{} where at least one literal is true in every clause. Even though the problem is proven to be hard to solve, a lot of progress has been made towards solving even the biggest the most complex \gls{sat} problems. -Modern day \gls{sat} solvers, like Clasp \autocite{gebser-2012-clasp}, Kissat \autocite{biere-2021-kissat} and MiniSAT \autocite{een-2003-minisat} , can solve instances of the problem with thousands of \variables{} and clauses. +Modern day \gls{sat} solvers, like Clasp \autocite{gebser-2012-clasp}, Kissat \autocite{biere-2021-kissat} and MiniSAT \autocite{een-2003-minisat} , solve instances of the problem with thousands of \variables{} and clauses. Many real world problems modelled using \cmls{} directly correspond to \gls{sat}. However, even problems that contain \variables{} with types other than Boolean can still be encoded as a \gls{sat} problem. -Depending on the problem, using a \gls{sat} \solvers{} to solve the encoded problem can still be the most efficient way to solve the problem. +Depending on the problem, using a \gls{sat} \solvers{} to solve the encoded problem might still be the most efficient way to solve the problem. \begin{example} Let us once more consider the N-Queens problem presented in \cref{ex:back-nqueens}. A possible \gls{sat} encoding for this problem is the following. \begin{align} - \text{given} \hspace{2em} & N = {1,\ldots,n} & \\ - \text{find} \hspace{2em} & q_{ij} \in \{\text{true}, \text{false}\} & \forall_{i,j \in N} \\ + \text{given} \hspace{2em} & N = {1,\ldots,n} & \notag{}\\ + \text{find} \hspace{2em} & q_{ij} \in \{\text{true}, \text{false}\} & \forall_{i,j \in N} \notag{}\\ \label{line:back-sat-at-least}\text{subject to} \hspace{2em} & \exists_{j \in N} q_{ij} & \forall_{i \in N} \\ - \label{line:back-sat-row} & \neg q_{ij} \lor \neg q_{ik} & \forall_{i,j \in N} \forall_{k=j}^{n} \\ - \label{line:back-sat-col} & \neg q_{ij} \lor \neg q_{kj} & \forall_{i,j \in N} \forall_{k=i}^{n} \\ - \label{line:back-sat-diag1} & \neg q_{ij} \lor \neg q_{(i+k)(j+k)} & \forall_{i,j \in N} \forall_{k=1}^{\min(n-i, n-j)} \\ - \label{line:back-sat-diag2} & \neg q_{ij} \lor \neg q_{(i+k)(j-k)} & \forall_{i,j \in N} \forall_{k=1}^{\min(n-i, j)} + \label{line:back-sat-row} & \neg q_{ij} \lor \neg q_{ik} & \forall_{i,j \in N} \forall_{j \leq{} k \leq{} n} \\ + \label{line:back-sat-col} & \neg q_{ij} \lor \neg q_{kj} & \forall_{i,j \in N} \forall_{i \leq{} k \leq{} n} \\ + \label{line:back-sat-diag1} & \neg q_{ij} \lor \neg q_{(i+k)(j+k)} & \forall_{i,j \in N} \forall_{1 \leq{} k \leq{} \min(n-i, n-j)} \\ + \label{line:back-sat-diag2} & \neg q_{ij} \lor \neg q_{(i+k)(j-k)} & \forall_{i,j \in N} \forall_{1 \leq{} k \leq{} \min(n-i, j)} \end{align} The encoding of the problem uses a Boolean \variable{} for every position of the chessboard. - Each \variable{} represents if a queen will be located on this position or not. + Each \variable{} represents if a queen is located on this position or not. \Cref{line:back-sat-at-least} forces that a queen is placed on every row of the chessboard. \Cref{line:back-sat-row,line:back-sat-col} ensure that only one queens is place in each row and column respectively. \Cref{line:back-sat-diag1,line:back-sat-diag2} similarly constrain each diagonal to contain only one queen. @@ -831,16 +834,16 @@ It is, again, possible to encode a \cmodel{} with an \gls{objective} as a \gls{m A naive approach to encode an integer objective is, for example, to encode each possible result of the \gls{objective} as a Boolean \variable{}. This Boolean \variable{} is then forms a singleton clause with the result value as its weight. -For many problems the use of \gls{maxsat} \solvers{} can offer a very successful method to find the optimal solution to a problem. +For many problems the use of \gls{maxsat} \solvers{} offers a very successful method to find the \gls{opt-sol} to a problem. \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. +Most of the techniques that are discusses in this thesis might be adapted to these languages. -We will now discuss some 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. +We now discuss some other prominent \cmls{} and compare them to \minizinc{} to indicate to the reader where techniques might have to be adjusted to fit other languages. A notable difference between all these languages and \minizinc{} is that only \minizinc{} allows modellers to extend the language using their own (user-defined) functions. In other \cmls{} the modeller is restricted to the expressions and functions provided by the language. @@ -854,14 +857,15 @@ As the name suggest, \gls{ampl} was designed to allow modellers to express probl It is therefore also described as an ``algebraic modelling language''. Specifically \gls{ampl} was designed to model linear programs. These days \gls{ampl} has been extended to allow more advanced \solver{} usage. -Depending on the \gls{solver} targeted by \gls{ampl}, the language can give the modeller access to additional functionality. -For \solvers{} that have a \gls{mip} solving method, the modellers can require \variables{} to be integers. +Depending on the \gls{solver} targeted by \gls{ampl}, the language gives the modeller access to additional functionality. +For \solvers{} that have a \gls{mip} solving method, the modellers is required to use \variables{} of numeric type. Different types of \solvers{} can also have access to different types of \constraints{}, such as quadratic and non-linear constraints. \gls{ampl} has even been extended to allow the usage of certain \glspl{global} when using a \gls{cp} \solver{} \autocite{fourer-2002-amplcp}. \begin{example} - If we consider the well-known travelling salesman problem, then we might model this problem in \gls{ampl} as follows: + \todo{explain what the TSP problem actually is. Probably needs a reference} + If we consider the well-known travelling salesman problem, then we might model this problem in \gls{ampl} as follows. \begin{ampl} set Cities ordered; @@ -883,6 +887,8 @@ Different types of \solvers{} can also have access to different types of \constr sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (j,i) in Paths} X[j,i] >= 2; \end{ampl} + + \todo{extend this paragraph, go over the ampl model, exactly explain what elements related to what part of the \minizinc{} syntax.} This model shows that the \gls{ampl} syntax has many features similar to \minizinc{}. Like \minizinc{}, \gls{ampl} has an extensive expression language, which includes \gls{generator} expressions and a vast collection of \glspl{operator}. The building block of the model are also similar: \parameter{} declarations, \variable{} declarations, \constraints{}, and a solving goal. @@ -903,10 +909,10 @@ Different types of \solvers{} can also have access to different types of \constr Even though the \gls{ampl} is similar to \minizinc{}, the models could not be more different. The main reason for this difference is the level at which these models are written. The \gls{ampl} model is written to target a \gls{mip} solver. - In the \gls{ampl} language this means that you can only use the language functionality that is compatible with the targeted \solver{}; in this case, all expression have to be linear equations. + In the \gls{ampl} language this means that you are required to use the language functionality that is compatible with the targeted \solver{}; in this case, all expression have to be linear equations. In \minizinc{} the modeller is not constrained in the same way. The modeller is always encouraged to create high-level \cmodels{}. - \minizinc{} will then rewrite these models into compatible \glspl{slv-mod}. + \minizinc{} then rewrites these models into compatible \glspl{slv-mod}. \end{example} \subsection{OPL}% @@ -919,10 +925,11 @@ 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 \constraints{} in an incremental and more natural fashion. -When solving a scheduling problem, the \gls{opl} makes use of specialised interval \variables{}, which represent when a task will be scheduled. +When solving a scheduling problem, the \gls{opl} makes use of specialised interval \variables{}, which represent when a task is scheduled. \begin{example} + \todo{explain what the job shop problem actually is. Probably needs a reference} For example the \variable{} declarations and \constraints{} for a job shop problem would look like this in an \gls{opl} model: \begin{plain} @@ -946,6 +953,7 @@ When solving a scheduling problem, the \gls{opl} makes use of specialised interv }; \end{plain} + \todo{extend this paragraph, go over the opl model, exactly explain what elements related to what part of the \minizinc{} syntax.} The equivalent declarations and \constraints{} would look like this in \minizinc{}: \begin{mzn} @@ -973,15 +981,15 @@ When solving a scheduling problem, the \gls{opl} makes use of specialised interv Note that the \minizinc{} model does not have explicit Activity \variables{}. It must instead use \variables{} that represent the start times of the activity and a \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. + The \gls{opl} model also has the advantage that it first states the resource objects and then uses 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 \constraint{} and its meaning might be less clear. + This might make it harder in \minizinc{} to write the correct \constraint{} and its meaning might be less clear. \end{example} -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. +The \gls{opl} also contains a specialised search syntax that is used to instruct its solvers \autocite{van-hentenryck-2000-opl-search}. +This syntax allows the modellers full programmatic control over how the solver explores 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: @@ -991,11 +999,11 @@ Take, for example, the following \gls{opl} search definition: } \end{plain} -This search strategy will ensure that we first try and find a solution where the \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 opposite is true. +This search strategy ensures that we first try and find a solution where the \variable{} \mzninline{x} takes a value smaller than \mzninline{y}, if it does not find a solution, then it tries finding a solution where the opposite is true. This search specification, like many others imaginable, cannot be enforced using \minizinc\ \gls{search-heuristic} \glspl{annotation}. To support \gls{opl}'s dedicated search language, the language is tightly integrated with its dedicated \solvers{}. -Its search syntax requires that the \gls{opl} process can directly interact with the \solver{}'s internal search mechanism and that the \solver{} reasons about search on the same level as the \gls{opl} model. +Its search syntax requires that the \gls{opl} process directly interacts with the \solver{}'s internal search mechanism and that the \solver{} reasons about search on the same level as the \gls{opl} model. It is therefore not possible to connect other \solvers{} to \gls{opl}. \subsection{Essence}% @@ -1012,11 +1020,12 @@ In addition to all variable types that are contained in \minizinc{}, \gls{essenc \item and (regular) partitions of finite types. \end{itemize} -Since sets, multi-sets, and functions can be defined on any other type, these types can be arbitrary nested and the modeller can define, for example, a \variable{} that is a sets of sets of integers. -Partitions can be defined for finite types: Booleans, enumerated types, or a restricted set of integers. +Since sets, multi-sets, and functions can be defined on any other type, these types can be arbitrary nested and the modeller could, for example, define a \variable{} that is a sets of sets of integers. +Partitions are defined for finite types: Booleans, enumerated types, or a restricted set of integers. \begin{example} + \todo{explain what the job shop problem actually is. Probably needs a reference} Consider, for example, the Social Golfers Problem, can be modelled in \gls{essence} as follows: \begin{plain} @@ -1035,6 +1044,7 @@ Partitions can be defined for finite types: Booleans, enumerated types, or a res (sum week in sched . toInt(together({g1, g2}, week))) <= 1 \end{plain} + \todo{extend this paragraph, go over the opl model, exactly explain what elements related to what part of the \minizinc{} syntax.} In \minizinc{} the same problem could be modelled as: \begin{mzn} @@ -1065,13 +1075,14 @@ Partitions can be defined for finite types: Booleans, enumerated types, or a res ); \end{mzn} - Note that, through the \gls{essence} type system, the first 2 \constraints{} 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. + Note that, through the \gls{essence} type system, the first two \constraints{} in the \minizinc{} are implied in the \gls{essence} model. + This is an example where the use of high-level types helps give the modeller create more concise models. \end{example} The high-level \variables{} available in \gls{essence} are often not \gls{native} to \solvers{}. To solve an \instance{}, not only do the \constraints{} have to be translated to \constraints{} \gls{native} to the \solver{}, but also all \variables{} have to be translated to a combination of \constraints{} and \variables{} \gls{native} to the \solver{}. +\todo{This needs a note that though \minizinc{} might also need transformation of the \variables{}, \gls{essence} will need to make more decisions along the way. It is generally easier to turn for example a integer into Booleans than the high-level transformations that they do.} \section{Term Rewriting}% \label{sec:back-term} @@ -1086,7 +1097,7 @@ In a term rewriting rule, a term can also contain a \emph{term variable} which c \begin{example} - Consider the following \gls{trs} consists of some (well-known) rules to rewrite logical and operations: + Consider the following \gls{trs} consists of some (well-known) rules to rewrite logical and operations. \begin{align*} (r_{1}):\hspace{5pt} & 0 \land x \rightarrow 0 \\ @@ -1096,11 +1107,11 @@ In a term rewriting rule, a term can also contain a \emph{term variable} which c From these rules it follows that - \[ 1 \land 1 \land 0 \rightarrow^{r_{1}} 1 \land 0 \rightarrow^{r_{3}} 0 \land 1 \rightarrow^{r_{2}} 0 \] + \[ 1 \land 1 \land 0 \rightarrow^{r_{2}} 1 \land 0 \rightarrow^{r_{3}} 0 \land 1 \rightarrow^{r_{1}} 0. \] - Notice that there can be a choice between different rules. + Notice that there is a choice between different rules. In general, a \gls{trs} can be non-deterministic. - We could also have applied the \(r_{1}\) twice and arrived at the same result. + We could also have applied the \(r_{2}\) twice and arrived at the same result. \end{example} Two properties of a \gls{trs} that are often studied are \gls{termination} and \gls{confluence}. @@ -1108,25 +1119,28 @@ A \gls{trs} is said to be terminating if, no-matter what order the term rewritin A \gls{trs} is confluent if, no-matter what order the term rewriting rules are applied, you always arrive at the same \gls{normal-form} (if you arrive at a \gls{normal-form}). It is trivial to see that our previous example is non-terminating, since you can repeat rule \(r_{3}\) an infinite amount of times. -The system, however, is confluent as, if it arrives at the same \gls{normal-form}: if the term contains any \(0\), then the result will be \(0\); otherwise, the result will be \(1\). +The system, however, is confluent as, if it arrives at the same \gls{normal-form}: if the term contains any \(0\), then the result is \(0\); otherwise, the result is \(1\). These properties are also interesting when in the translation process of a \minizinc{} instance into \flatzinc{}. -The \gls{confluence} of the \gls{rewriting} process will ensure that the same \gls{slv-mod} is produced independently of the order in which the \minizinc{} \instance{} is processed. +The \gls{confluence} of the \gls{rewriting} process ensures that the same \gls{slv-mod} is produced independently of the order in which the \minizinc{} \instance{} is processed. This is a desirable quality as it makes the behaviour of the \gls{rewriting} process more predictable. Many of the techniques used by \solvers{} targeted by \minizinc{} are proven to be complete. Meaning that they are guaranteed to (eventually) find a (optimal) \gls{sol} for the \instance{} or prove that there is none. -For this quality to hold for the overall \minizinc{} solving process, it has to be guaranteed that the \minizinc{} \gls{rewriting} process terminates (so the solving process can start). +For this quality to hold for the overall \minizinc{} solving process, it has to be guaranteed that the \minizinc{} \gls{rewriting} process terminates (so the solving process is able to start). -In the remainder of this section we will discuss two types of \glspl{trs} that are closely related to \cmls{} and the \gls{rewriting} process: \gls{clp} and \gls{chr}. +In the remainder of this section we discuss two types of \glspl{trs} that are closely related to \cmls{} and the \gls{rewriting} process: \gls{clp} and \gls{chr}. \subsection{Constraint Logic Programming}% \label{subsec:back-clp} \glsreset{clp} -\gls{clp} \autocite{marriott-1998-clp} can be seen as a predecessor of \cmls{} like \minizinc{}. +\gls{clp} \autocite{jaffar-1987-clp} is a predecessor of \cmls{} like \minizinc{}. +This subsection provides a brief introduction into the workings a \gls{clp} system. +For a more comprehensive overview on modelling, rewriting, and solving using a \gls{clp} system, we recommend reading ``Programming with constraints: an introduction'' by \textcite{marriott-1998-clp} + A constraint logic program describes the process in which \cmodel{} is eventually rewritten into a \gls{slv-mod} and solved by a \solver{}. -Like in \minizinc{}, can define \constraint{} predicates to use in the definition of the \cmodel{}. +Like in \minizinc{}, the user defines \constraint{} predicates to use in the definition of the \cmodel{}. Different from \minizinc{}, constraint predicates in \gls{clp} can be rewritten in multiple ways. The goal of a constraint logic program is to rewrite all \constraints{} in such a way that all \gls{native} \glspl{constraint} are \gls{satisfied}. @@ -1135,25 +1149,25 @@ In \gls{clp}, like in a conventional \gls{trs}, a variable is merely a name. The symbol might be replaced or equated with a constant symbol, but, different from \cmls{}, this is not a requirement. A variable can remain a name in the solution of a constraint logic program. This means that the solution of a constraint logic program can be a relationship between different variables. -In cases where an instantiated solution is required, a special \mzninline{labeling} \constraint{} can be used to force a variable to take a constant value. -Similarly, there is a \mzninline{minimize} \constraint{} that can be used to find the optimal value for a variable. +In cases where an instantiated solution is required, a special \mzninline{labeling} \constraint{} is used to force a variable to take a constant value. +Similarly, there is a \mzninline{minimize} \constraint{} that is used to find the optimal value for a variable. The evaluation of a constraint logic program rewrites the list of constraints, called the goal, in the order given by the programmer. The \gls{rewriting} of the constraint predicates is tried in the order in which the different \gls{rewriting} rules for the constraint predicates are defined. The process is completed when all constraints are rewritten and no inconsistency is detected between the \gls{native} \constraints{} that are produced. -If all the possible ways of rewriting the program are tried, but all of them prove to be inconsistent, then the program itself can be said to be \gls{unsat}. +If all the possible ways of rewriting the program are tried, but all of them prove to be inconsistent, then the program itself is said to be \gls{unsat}. Even when a correct rewriting is found, it is possible to continue the process. -This way you can find all possible correct ways to rewrite the program. +This way you find all possible correct ways to rewrite the program. To implement this mechanism there is a tight integration between the \solver{}, referred to as the \emph{constraint store}, and the evaluator of the constraint logic program. -In addition to just adding \constraints{}, the program can also inspect the status of the \constraint{} and retract \constraints{} from the constraint store. +In addition to just adding \constraints{}, the program also inspects the status of the \constraint{} and retracts \constraints{} from the constraint store. This allows the program to detect when the constraint store has become inconsistent and then \gls{backtrack} the constraint store to the last decision (\ie\ restore the constraint store to its state before the last decision was made) and try the next rewriting rule. -The strength of the constraint store can influence the correctness of a constraint logic program. +The strength of the constraint store influence the correctness of a constraint logic program. Some \solvers{} are incomplete; it is unable to tell if some of its \constraints{} are \gls{satisfied} or not. This, for example, happens with \solvers{} that work with integer \glspl{domain}. In these cases the programmer must use the \mzninline{labeling} constraint to force constant values for the variables. -Once the variables have been assigned constant values, the \solver{} will always be able to decide if the \constraints{} are \gls{satisfied}. +Once the variables have been assigned constant values, the \solver{} is always able to decide if the \constraints{} are \gls{satisfied}. \subsection{Constraint Handling Rules}% \label{sub:back-chr} @@ -1161,9 +1175,9 @@ Once the variables have been assigned constant values, the \solver{} will always When \constraints{} are seen as terms in a \gls{trs}, then it is not just possible to define rules to rewrite \constraints{} to \gls{native} \constraints{}. It is also possible to define rules to simplify, propagate, and derive new \constraints{} within the \solver{}. -\gls{chr} follow from this idea. +\gls{chr} \autocite{fruhwirth-1998-chr} follow from this idea. \gls{chr} are a language extension (targeted at \gls{clp}) to allow user-defined \constraints{} within a \solver{}. -\constraints{} defined using \gls{chr} are rewritten into simpler \constraints{} until they are solved. +\Constraints{} defined using \gls{chr} are rewritten into simpler \constraints{} until they are solved. Different from \gls{clp}, \gls{chr} allows term rewriting rules that are multi-headed. This means that, for some rules, multiple terms must match, to apply the rule. @@ -1199,9 +1213,9 @@ This means that, for some rules, multiple terms must match, to apply the rule. \end{example} -The rules in a \gls{chr} system can be categorised into three different categories: simplification, propagation, and simpagation. +The rules in a \gls{chr} system are categorised into three different categories: simplification, propagation, and simpagation. The first two rules in the previous example are simplification rules: they replace some \constraint{} atoms by others. -The final rule in the example was a propagation rule: based on the existence of certain \constraints{}, new \constraints{} can be introduced. +The final rule in the example was a propagation rule: based on the existence of certain \constraints{}, new \constraints{} are introduced. Simpagation rules are a combination of both types of rules in the form: \[ H_{1}, \ldots H_{l} \backslash H_{l+1}, \ldots, H_{n} \texttt{<=>} G_{1}, \ldots{}, G_{m} | B_{1}, \ldots, B_{o} \] @@ -1224,9 +1238,9 @@ When a \compiler{} is separated into these few steps, then adding support for ne The \minizinc{} compilation process categorised in the same three categories, as shown in \cref{fig:back-mzn-comp}. In the frontend, a \minizinc{} model is combined with its data into an \instance{}. The instance parsed into an \gls{ast}. -The process will then analyse the \gls{ast} to discover the types of all expressions used in the \instance{}. +The process then analyses the \gls{ast} to discover the types of all expressions used in the \instance{}. If an inconsistency is discovered, then an error is reported to the modeller. -Finally, the frontend will also preprocess the \gls{ast}. +Finally, the frontend also preprocesses the \gls{ast}. This process is used to transform expressions into a common form for the middle-end, \eg\ remove the ``syntactic sugar''. For instance, replacing the usage of enumerated types by normal integers. @@ -1243,14 +1257,14 @@ During the flattening process the \minizinc{} model is rewritten into a \gls{slv It could be noted that the rewriting step depends on the compilation target to define its \gls{native} \constraints{}. Even though the information required for this step is target dependent, we consider it part of the middle-end as the mechanism is the same for all compilation targets. A full description of this process will follow in \cref{subsec:back-rewriting}. -Once a \gls{slv-mod} is constructed, the \minizinc{} \compiler{} will try to optimise this model: shrink \domains{} of \variables{}, remove \constraints{} that are proven to hold, and remove \variables{} that have become unused. +Once a \gls{slv-mod} is constructed, the \minizinc{} \compiler{} tries to optimise this model: shrink \domains{} of \variables{}, remove \constraints{} that are proven to hold, and remove \variables{} that have become unused. These optimisation techniques are discussed in \cref{subsec:back-fzn-optimisation}. -The backend will convert the internal \gls{slv-mod} into a format that can be used by the targeted \solver{}. -Given the formatted artefact, a solver process, controlled by the backend, can then be started. -Whenever the solver process produces a \gls{sol}, the backend will reconstruct the \gls{sol} to the specification of the original \minizinc{} model. +The backend converts the internal \gls{slv-mod} into a format that to be used by the targeted \solver{}. +Given the formatted artefact, a solver process, controlled by the backend, is then be started. +Whenever the solver process produces a \gls{sol}, the backend reconstructs the \gls{sol} to the specification of the original \minizinc{} model. -In this section we will discuss the \gls{rewriting} and optimisation process as employed by the 2.5.5 version of \minizinc{} \autocite{minizinc-2021-minizinc}. +In this section we discuss the \gls{rewriting} and optimisation process as employed by the 2.5.5 version of \minizinc{} \autocite{minizinc-2021-minizinc}. \subsection{Rewriting}% \label{subsec:back-rewriting} @@ -1258,23 +1272,23 @@ In this section we will discuss the \gls{rewriting} and optimisation process as The goal of the \gls{rewriting} process is to arrive at a flat \gls{slv-mod}. An \gls{eqsat} \instance{} that only contains \constraints{} that consist of a singular call instruction, all arguments to calls are \parameter{} literals or \variable{} identifiers, and using only \constraints{} and \variable{} types that are \gls{native} to the target \solver{}. -To arrive at a flat \gls{slv-mod}, the \gls{rewriting} process will transverse the declarations, \constraints{}, and the solver goal and rewrite any expression contained in these items. +To arrive at a flat \gls{slv-mod}, the \gls{rewriting} process transverses the declarations, \constraints{}, and the solver goal and rewrite any expression contained in these items. During the \gls{rewriting} of an expression, the expression rewritten into other \minizinc{} expressions according to the \gls{decomp} given in the target \solver{}'s library. Enforced by \minizinc{}'s type system, at most one rule applies for any given \constraint{}. The \gls{rewriting} of expressions is performed bottom-up, we rewrite any sub-expression before its parent expression. For instance, in a call each argument is rewritten before the call itself is rewritten. An exception to this bottom-up approach is the \gls{rewriting} of \gls{generator} expressions. -Expression containing \glspl{generator}, such as array \glspl{comprehension} and loops, have to be instantiated before their sub-expression can be rewritten. +Expression containing \glspl{generator}, such as array \glspl{comprehension} and loops, have to be instantiated before their sub-expression is rewritten. The compiler exhaustively binds the values of the \gls{generator} to the specified identifiers. For each iteration the compiler rewrites the sub-expression and collects its result. -Once the \gls{generator} is exhausted, the compiler can rewrite its surrounding expression using the collected values. +Once the \gls{generator} is exhausted, the compiler rewrites its surrounding expression using the collected values. The \gls{decomp} system in \minizinc{} is defined in terms of functions declarations. -Any call, whose declaration has a function body, will eventually be replaced by an instantiation of this function body using the arguments to the call. +Any call, whose declaration has a function body, is eventually replaced by an instantiation of this function body using the arguments to the call. Calls are, however, not the only type of expression that are decomposed during the \gls{rewriting} process. Other expression, like \gls{operator} expressions, variable array access, and if-then-else expressions, might also have to be decomposed for the target \solver{}. -During the \gls{rewriting} process, these expressions are rewritten into equivalent call expressions that will start the decomposition process. +During the \gls{rewriting} process, these expressions are rewritten into equivalent call expressions that start the decomposition process. A notable effect of the \gls{rewriting} is that sub-expression are replaced by literals or identifiers. If the expression contains only \parameters{}, then the \gls{rewriting} of the expression is merely a calculation to find the value of the literal to be put in its place. @@ -1285,7 +1299,7 @@ The creation of this new \variable{} and defining \constraints{} happens in one \begin{itemize} \item For Boolean expressions in a non-\rootc{} context, the new \variable{} is inserted by the \gls{rewriting} process itself. - To constrain this \variable{}, the \compiler{} will then add the \gls{reif} of the \constraint{}. + To constrain this \variable{}, the \compiler{} then adds the \gls{reif} of the \constraint{}. This \constraint{} contains a variation of the call that would have been generated for the expression in \rootc{} context. The name of the function is appended with \mzninline{_reif} and an extra Boolean \variable{} argument is added to the call. The definition of this constraint should implement the \gls{reif} of the original expression: setting the additional argument to \mzninline{true} if the constraint is \gls{satisfied}, and \mzninline{false} otherwise. @@ -1295,7 +1309,7 @@ The creation of this new \variable{} and defining \constraints{} happens in one constraint b \/ this_call(x, y); \end{mzn} - \noindent{} will during \gls{rewriting} be turned into: + \noindent{} is during \gls{rewriting} turned into: \begin{mzn} var bool: i1; @@ -1304,13 +1318,13 @@ The creation of this new \variable{} and defining \constraints{} happens in one \end{mzn} \item For other expressions, the \variable{} and defining \constraints{} are introduced in the definition of the function itself. - For example, the definition of the \mzninline{max} function in the standard library, which calculates the maximum of two values, is defined as: + For example, the \mzninline{max} function in the standard library, which calculates the maximum of two values, is defined as follows. \begin{mzn} - function var int: max(var int: x, var int: y) :: promise_total = + function var int: max(var int: x, var int: y) = let { - var max(lb(x),lb(y))..max(ub(x),ub(y)): m ::is_defined_var; - constraint int_max(x,y,m) ::defines_var(m); + var max(lb(x),lb(y))..max(ub(x),ub(y)): m; + constraint int_max(x,y,m); } in m; \end{mzn} @@ -1322,14 +1336,20 @@ This is, however, not the complete process. The quality of the resulting \gls{slv-mod} is of the utmost importance. A \gls{slv-mod} containing extra \variables{} and \constraints{} that do not add any information to the solving process might exponentially slow it down. Therefore, the \minizinc{} \gls{rewriting} process is extended using many techniques to help improve the quality of the \gls{slv-mod}. -In \crefrange{subsec:back-cse}{subsec:back-delayed-rew}, we will discuss the most important techniques used to improve the \gls{rewriting} process. +In \crefrange{subsec:back-cse}{subsec:back-delayed-rew}, we discuss the most important techniques used to improve the \gls{rewriting} process. \subsection{Common Sub-expression Elimination}% \label{subsec:back-cse} \glsreset{cse} -Because the evaluation of a \minizinc{} expression cannot have any side effects, it is possible to reuse the same result for equivalent expressions. -This simplification, called \gls{cse}, is a well understood technique that originates from compiler optimisation \autocite{cocke-1970-cse} and has proven to be very effective in discrete optimisation \autocite{marinov-2005-sat-optimisations, araya-2008-cse-numcsp}, including during the evaluation of \cmls{} \autocite{rendl-2009-enhanced-tailoring}. +The evaluation of a \minizinc{} expression cannot have any side effects. +Having evaluated one expression cannot influence the result of evaluating another expression. +Similarly, the evaluation of the same expression will always reach an equivalent result. + +It is therefore possible to reuse the same result for equivalent expressions. +This simplification is called \gls{cse}. +It is a well understood technique that originates from compiler optimisation \autocite{cocke-1970-cse}. +\Gls{cse} has also proven to be very effective in discrete optimisation \autocite{marinov-2005-sat-optimisations, araya-2008-cse-numcsp}, including during the evaluation of \cmls{} \autocite{rendl-2009-enhanced-tailoring}. \begin{example} \label{ex:back-cse} @@ -1352,7 +1372,7 @@ Some expressions only become syntactically equal when instantiated, as in the fo \begin{mzn} function var float: pythagoras(var float: a, var float: b) = - let { + let { var float: x = pow(a, 2); var float: y = pow(b, 2); } in sqrt(x + y); @@ -1368,20 +1388,20 @@ Then before any consequent expression is flattened the \gls{cse} table is consul If an equivalent expression is found, then the accompanying result is used; otherwise, the evaluation proceeds as normal. In our example, the evaluation of \mzninline{pythagoras(i, i)} would proceed as normal to evaluate \mzninline{x = pow(i, 2)}. -However, the expression defining \mzninline{y}, \mzninline{pow(i, 2)}, will be found in the \gls{cse} table and replaced by the earlier stored result: \mzninline{y = x}. +However, the expression defining \mzninline{y}, \mzninline{pow(i, 2)}, is then found in the \gls{cse} table and replaced by the earlier stored result: \mzninline{y = x}. \gls{cse} also has an important interaction with the occurrence of \glspl{reif}. \Glspl{reif} are often defined in the library in terms of complicated \gls{decomp} into \gls{native} \constraints{}, or require more complex algorithms in the target \solver{}. -In either case, it can be very beneficial for the efficiency solving process if we can detect that a reified constraint is in fact not required. +In either case, it can be very beneficial for the efficiency solving process if we detect that a reified constraint is in fact not required. -If a \constraint{} is present in the root context, it means that it must hold globally. -If the same \constraint{} is used in a non-\rootc{} context, it can therefore be replaced with the constant \mzninline{true}, avoiding the need for \gls{reif} (or in fact any evaluation). +If a \constraint{} is present in the \rootc{} context, it means that it must hold globally. +If the same \constraint{} is used in a non-\rootc{} context, it is then replaced with the constant \mzninline{true}, avoiding the need for \gls{reif} (or in fact any evaluation). -We can harness \gls{cse} to store the evaluation context when a \constraint{} is added, and detect when the same \constraint{} is used in both contexts. -Whenever a lookup in the \gls{cse} table is successful, action can be taken depending on both the current and stored evaluation context. -If the stored expression was in \rootc{} context, then the constant \mzninline{true} can be used, independent of the current context. -Otherwise, if the stored expression was in non-\rootc{} context and the current context is non-\rootc{}, then the stored result variable can be used. -Finally, if the stored expression was in non-\rootc{} context and the current context is \rootc{} context, then the previous result can be replaced by the constant \mzninline{true} and the evaluation will proceed as normal with the \rootc{} context \constraint{}. +We harness \gls{cse} to store the evaluation context when a \constraint{} is added, and detect when the same \constraint{} is used in both contexts. +Whenever a lookup in the \gls{cse} table is successful, action is taken depending on both the current and stored evaluation context. +If the stored expression was in \rootc{} context, then the constant \mzninline{true} is used, independent of the current context. +Otherwise, if the stored expression was in non-\rootc{} context and the current context is non-\rootc{}, then the stored result variable is used. +Finally, if the stored expression was in non-\rootc{} context and the current context is \rootc{} context, then the previous result is replaced by the constant \mzninline{true} and the evaluation proceeds as normal with the \rootc{} context \constraint{}. \begin{example} Consider the fragment: @@ -1403,13 +1423,15 @@ Finally, if the stored expression was in non-\rootc{} context and the current co \label{subsec:back-adjusting-dom} Sometimes a \constraint{} can be detected to be true based on its semantics, and the known \glspl{domain} of \variables{}. -For example, consider the constraint \mzninline{3*x + 7*y > 8}, and assume that both \mzninline{x} and \mzninline{y} cannot be smaller than 1. In this case, we can determine that the constraint is always \gls{satisfied}, and remove it from the model without changing satisfiability. -This is a simple form of \gls{propagation}, which, as discussed in \cref{subsec:back-cp}, can also tighten the \glspl{domain} of \variables{} in the presence of a \constraint{}. +For example, consider the constraint \mzninline{3*x + 7*y > 8}, and assume that both \mzninline{x} and \mzninline{y} cannot be smaller than one. +In this case, we can determine that the constraint is always \gls{satisfied}, and remove it from the model without changing satisfiability. +This is a simple form of \gls{propagation}, which, as discussed in \cref{subsec:back-cp}, also tightens the \glspl{domain} of \variables{} in the presence of a \constraint{}. The principles of \gls{propagation} can also be applied during the \gls{rewriting} of a \minizinc{} model. It is generally a good idea to detect cases where we can directly change the \gls{domain} of a \variable{}. Sometimes this might mean that the \constraints{} does not need to be added at all and that constricting the \gls{domain} is enough. -Tight domains can also allow us to avoid the creation of \glspl{reif} when the truth-value of a reified \constraint{} can be determined from the \domains{}. +Tight domains also allow us to avoid the creation of \glspl{reif} when the truth-value of a reified \constraint{} can be determined from the \domains{}. +Finally, it can also be helpful for \solvers{} as they might need to decide on a representation of \variables{} based on their initial \domain{}. \begin{example}% \label{ex:back-adj-dom} @@ -1427,17 +1449,17 @@ Tight domains can also allow us to avoid the creation of \glspl{reif} when the t If we however consider the first \constraint{}, then we deduce that \mzninline{a} must always take a value that is 4 or lower. When the compiler adjusts the domain of \mzninline{a} while \gls{rewriting} the first \constraint{}, then the second \constraint{} can be simplified. - The expression \mzninline{a > 5} is known to be \mzninline{false}, which means that the \constraint{} can be simplified to \mzninline{true}. + The expression \mzninline{a > 5} is known to be \mzninline{false}, which means that the \constraint{} is simplified to \mzninline{true}. \end{example} -During \gls{rewriting}, the \minizinc{} compiler will actively remove values from the \domain{} when it encounters \constraints{} that trivially reduces it. +During \gls{rewriting}, the \minizinc{} compiler actively removes values from the \domain{} when it encounters \constraints{} that trivially reduces it. For example, \constraints{} with a single comparison expression between a \variable{} and a \parameter{} (\eg\ \mzninline{x != 5}), \constraints{} with a single comparison between two \variables{} (\eg\ \mzninline{x >= y}), \constraints{} that directly change the domain (\eg\ \mzninline{x in 3..5}). -It, however, will not perform more complex \gls{propagation}, like the \gls{propagation} of \glspl{global}. +It, however, does not perform more complex \gls{propagation}, like the \gls{propagation} of \glspl{global}. \subsection{Constraint Aggregation}% \label{subsec:back-aggregation} -Complex \minizinc{} expression can sometimes result in the creation of many \glspl{ivar} to represent intermediate results. +Complex \minizinc{} expressions sometimes result in the creation of many \glspl{ivar} to represent intermediate results. This is in particular true for linear and boolean equations that are generally written using \minizinc{} operators. \begin{example}% @@ -1468,11 +1490,11 @@ This is in particular true for linear and boolean equations that are generally w This can be resolved using the \gls{aggregation}. When we aggregate \constraints{} we collect multiple \minizinc{} expressions, that would each have been rewritten separately, and combine them into a singular structure that eliminates the need for \glspl{ivar}. -For example, the arithmetic definitions can be combined into linear \constraints{}, Boolean logic can be combined into clauses, and counting \constraints{} can be combined into global cardinality \constraints{}. +For example, the arithmetic definitions are combined into linear \constraints{}, Boolean logic are combined into clauses, and counting \constraints{} are combined into global cardinality \constraints{}. The \minizinc{} \compiler{} aggregates expressions whenever possible. -When the \minizinc{} \compiler{} reaches an expression that could potentially be part of an aggregated \constraint{}, the \compiler{} will not rewrite the expression. -The \compiler{} will instead perform a search of its sub-expression to collect all other expressions to form an aggregated \constraint{}. +When the \minizinc{} \compiler{} reaches an expression that could potentially be part of an aggregated \constraint{}, the \compiler{} does not rewrite the expression. +The \compiler{} instead performs a search of its sub-expression to collect all other expressions to form an aggregated \constraint{}. The \gls{rewriting} process continues by \gls{rewriting} this aggregated \constraint{}. \subsection{Delayed Rewriting}% @@ -1488,7 +1510,7 @@ Adding \gls{propagation} during \gls{rewriting} means that the system becomes no x <= ub(x)*(1-b); \end{mzn} - This predicate expresses the \constraint{} \mzninline{b -> x<=0}, using a well-known method called ``big-M transformation''. + This predicate expresses the \constraint{} \mzninline{b -> x<=0}, using a well-known technique called the ``Big M method''. The expression \mzninline{ub(x)} returns a valid upper bound for \mzninline{x}, \ie{} a fixed value known to be greater than or equal to \mzninline{x}. This could be the initial upper bound \mzninline{x} was declared with or the current value adjusted by the \minizinc{} \compiler{}. If \mzninline{b} takes the value 0, the expression \mzninline{ub(x)*(1-b)} is equal to \mzninline{ub(x)}, and the \constraint{} \mzninline{x <= ub(x)} holds trivially. @@ -1501,13 +1523,13 @@ On the other hand, evaluating a predicate may also \emph{impose} new bounds on \ The same problem occurs with \glspl{reif} that are produced during \gls{rewriting}. Other \constraints{} could fix the \domain{} of the reified \variable{} and make the \gls{reif} unnecessary. -Instead, the \constraint{} (or its negation) can be flattened in \rootc{} context. +Instead, the \constraint{} (or its negation) might be flattened in \rootc{} context. This could avoid the use of a big \gls{decomp} or an expensive \gls{propagator}. To tackle this problem, the \minizinc{} \compiler{} employs \gls{del-rew}. When a linear \constraint{} is aggregated or a relational \gls{reif} \constraint{} is introduced it is not immediately rewritten. Instead, these \constraints{} are appended to the end of the current \gls{ast}. -All other \constraints{}, that are not yet rewritten and could change the relevant \domains{}, will be rewritten first. +All other \constraints{}, that are not yet rewritten and could change the relevant \domains{}, are rewritten first. Note that this heuristic does not guarantee that \variables{} have their tightest possible \gls{domain}. One delayed \constraint{} can still influence the \domains{} of \variables{} used by other delayed \constraints{}. @@ -1523,13 +1545,13 @@ Because the \compiler{} does not revisit \gls{aggregation}, this does not happen After the \compiler{} is done \gls{rewriting} the \minizinc{} instance, it enters the optimisation phase. This phase occurs at the level at which the targeted \solver{} operates. -Depending on this \solver{}, the \minizinc{} \compiler might still understand the meaning of certain \constraints{}. -In these cases, \gls{propagation} methods, as discussed in \cref{subsec:back-cp}, can be used to eliminate values from \domains{} and simplify \constraints{}. +Depending on this \solver{}, the \minizinc{} \compiler{} might still understand the meaning of certain \constraints{}. +In these cases, \gls{propagation} methods, as discussed in \cref{subsec:back-cp}, are used to eliminate values from \domains{} and simplify \constraints{}. In the current implementation the main focus of the \compiler{} is to propagate Boolean \constraints{}. The \compiler{} tries to reduce the number of Boolean \variables{} and tries to reduce the number of literals in clauses and conjunctions. The additional \gls{propagation} might fix the result of the \gls{reif} of a \constraint{}. -If this \constraint{} is not yet rewritten, then the \solver{} will know to use a direct \constraint{} instead of a reified version. +If this \constraint{} is not yet rewritten, then the \solver{} knows to use a direct \constraint{} instead of a reified version. Even more important than the Boolean \constraints{}, are equality \constraints{}. During the \gls{rewriting} process we are in a unique position to perform effective equality propagation. diff --git a/chapters/2_background_preamble.tex b/chapters/2_background_preamble.tex index 8a46718..66c1aa9 100644 --- a/chapters/2_background_preamble.tex +++ b/chapters/2_background_preamble.tex @@ -1,5 +1,5 @@ This research presented in this thesis investigates the process of \gls{rewriting} \cmls{} to address both the lack of information about this process and to improve this process to meet its modern day requirements. -This chapter provides the background necessary to understand the usage of \cmls{}: +This chapter provides the required background information to understand \cmls{}: \begin{itemize} \item How do you create a \cmodel{}? @@ -9,14 +9,14 @@ This chapter provides the background necessary to understand the usage of \cmls{ In particular, it gives further information about \minizinc{} and discusses the functionality available to create \cmodels{}. It also provides some insight into \solvers{}, discussing the most important techniques used to solve \instances{} of \cmodels{}. -Additionally, it summarises the functionality of other \cmls{} to serve as a comparison with \minizinc{} +Additionally, it summarises the functionality of other \cmls{} to serve as a comparison with \minizinc{}. This is followed by a brief overview of other closely related \glspl{trs}. Finally, the chapter analyses the existing approach to \gls{rewriting} \minizinc{} and discusses its limitations. The overview of \cmls{} presented in this chapter supports the research and discussion presented in subsequent chapters. -In the remainder of this chapter we will first, in \cref{sec:back-intro} introduce the reader to \cmls{} and their purpose. +In the remainder of this chapter we first, in \cref{sec:back-intro} introduce the reader to \cmls{} and their purpose. \Cref{sec:back-minizinc} summarised the syntax and functionality of \minizinc{}, the leading \cml{} used within this thesis. -In \cref{sec:back-solving} we discuss how \gls{cp}, \gls{mip}, and \gls{sat} can be used to solve a \gls{slv-mod}. +In \cref{sec:back-solving} we discuss how \gls{cp}, \gls{mip}, and \gls{sat} are used to solve a \gls{slv-mod}. \Cref{sec:back-other-languages} introduces alternative \cmls{} and compares their functionality to \minizinc{}. Then, \cref{sec:back-term} survey the closely related technologies in the field of \glspl{trs}. Finally, \cref{sec:back-mzn-interpreter} explores the process that the current \minizinc{} \interpreter{} uses to translate a \minizinc{} \instance{} into a \gls{slv-mod}.