diff --git a/assets/bibliography/references.bib b/assets/bibliography/references.bib index 0f112b1..52bf959 100644 --- a/assets/bibliography/references.bib +++ b/assets/bibliography/references.bib @@ -258,26 +258,15 @@ bibsource = {dblp computer science bibliography, https://dblp.org}, } -@manual{cplex-2020-cplex, - title = {V20.1: User’s Manual for CPLEX}, - author = {CPLEX, IBM ILOG}, - journal = {International Business Machines Corporation}, - year = 2020, -} - -@article{dantzig-1982-simplex, - author = {George B. Dantzig}, - title = {Reminiscences about the origins of linear programming}, - journal = {Oper. Res. Lett.}, - volume = {1}, +@article{dantzig-1955-simplex, + title = {The generalized simplex method for minimizing a linear form under + linear inequality restraints}, + author = {Dantzig, George B and Orden, Alex and Wolfe, Philip and others}, + journal = {Pacific Journal of Mathematics}, + volume = {5}, 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}, + pages = {183--195}, + year = {1955}, } @article{davis-1960-dpll, @@ -559,6 +548,20 @@ bibsource = {dblp computer science bibliography, https://dblp.org}, } +@manual{ibm-2017-opl, + title = {OPL Language User’s Manual}, + author = {CPLEX, IBM ILOG}, + journal = {International Business Machines Corporation}, + year = 2017, +} + +@manual{ibm-2020-cplex, + title = {V20.1: User’s Manual for CPLEX}, + author = {CPLEX, IBM ILOG}, + journal = {International Business Machines Corporation}, + year = 2020, +} + @inproceedings{ingmar-2020-diverse, author = {Linnea Ingmar and Maria Garcia de la Banda and Peter J. Stuckey and Guido Tack}, @@ -822,6 +825,21 @@ bibsource = {dblp computer science bibliography, https://dblp.org}, } +@article{miller-1960-subtour, + author = {C. E. Miller and A. W. Tucker and R. A. Zemlin}, + title = {Integer Programming Formulation of Traveling Salesman Problems}, + journal = {J. {ACM}}, + volume = {7}, + number = {4}, + pages = {326--329}, + year = {1960}, + url = {https://doi.org/10.1145/321043.321046}, + doi = {10.1145/321043.321046}, + timestamp = {Wed, 14 Nov 2018 10:35:26 +0100}, + biburl = {https://dblp.org/rec/journals/jacm/MillerTZ60.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org}, +} + @software{minizinc-2021-minizinc, author = {{MiniZinc Team}}, title = {MiniZinc: a free and open-source constraint modeling language}, diff --git a/assets/glossary.tex b/assets/glossary.tex index 575a6de..0e08291 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -21,10 +21,10 @@ \newglossaryentry{assignment}{ name={assignment}, description={ - A mapping from \glspl{parameter} or \glspl{variable} to values. - An assignment is referred to as \gls{partial} when it maps only a subset of the \glspl{parameter} and \glspl{variable} of a \gls{model}. - A \gls{parameter-assignment} is an \gls{partial} \gls{assignment} that maps only the \glspl{parameter}, a \gls{variable-assignment} maps only the \glspl{variable}. - A complete \gls{parameter-assignment} maps all \glspl{parameter} of a \gls{model}, a complete \gls{variable-assignment} maps all \glspl{variable} of a \gls{model} + A mapping from \glspl{prb-par} or \glspl{variable} to values. + An assignment is referred to as \gls{partial} when it maps only a subset of the \glspl{prb-par} and \glspl{variable} of a \gls{model}. + A \gls{parameter-assignment} is an \gls{partial} \gls{assignment} that maps only the \glspl{prb-par}, a \gls{variable-assignment} maps only the \glspl{variable}. + A complete \gls{parameter-assignment} maps all \glspl{prb-par} of a \gls{model}, a complete \gls{variable-assignment} maps all \glspl{variable} of a \gls{model} }, } @@ -45,7 +45,15 @@ \newglossaryentry{array}{ name={array}, - description={A data structure that holds a collection of elements (\glspl{parameter} or \glspl{variable}), each identified by an index. Provided the index of an element, the array can retrieve the element}, + description={A data structure that holds a collection of elements, each identified by an index. Provided the index of an element, the array can retrieve the element}, +} + +\newglossaryentry{avar}{ + name={auxiliary variable}, + description={ + A \gls{variable} not explicitly defined in a \gls{model}, but rather introduced in the \gls{rewriting} of an \gls{instance}. + Auxiliary \glspl{variable} are generally introduced to redefine an existing \gls{variable} using \glspl{variable} of a different type, to represent an sub-expression, or to connect \glspl{constraint} in a \gls{decomp} + }, } \newglossaryentry{backtrack}{ @@ -118,7 +126,7 @@ name={constraint modelling language}, description={ A computer language used to define \glspl{model}. - Constraint modelling languages allow modellers to define \glspl{model} in terms of \glspl{parameter}, \gls{variable} and \glspl{constraint}. + Constraint modelling languages allow modellers to define \glspl{model} in terms of \glspl{prb-par}, \gls{variable} and \glspl{constraint}. Together with a complete \gls{parameter-assignment} a \gls{model} forms an \gls{instance}. Through the process of \gls{rewriting} the \gls{instance} is transformed into a \gls{slv-mod}, for which a \gls{solver} can find \glspl{sol} }, @@ -126,7 +134,7 @@ \newglossaryentry{cplex}{ name={CPLEX}, - description={A well-known proprietary \gls{mip} \gls{solver} developed by IBM \autocite{cplex-2020-cplex}}, + description={A well-known proprietary \gls{mip} \gls{solver} developed by IBM \autocite{ibm-2020-cplex}}, } \newglossaryentry{gls-chr}{ @@ -161,7 +169,7 @@ \newglossaryentry{cvar}{ name={control variable}, description={ - A special form of an \gls{ivar} where the \gls{variable} represent the result of a \gls{reif} + A special form of an \gls{avar} where the \gls{variable} represent the result of a \gls{reif} }, } @@ -266,17 +274,10 @@ } \newglossaryentry{half-reified}{ - name={half reified}, + name={half-reified}, description={See \gls{half-reif}}, } -\newglossaryentry{ivar}{ - name={introduced variable}, - description={ - A \gls{variable} that was created in the reformulation of a \gls{decomp}. - New \gls{variable} are introduced either to redefine an existing \gls{variable} using a different type or to connect newly introduced \glspl{constraint} - }, -} \newglossaryentry{incremental-rewriting}{ name={incremental-rewriting}, @@ -362,8 +363,8 @@ description={ A formalisation of a \gls{dec-prb} or an \gls{opt-prb}. It is defined in terms of formalised decision, \glspl{variable} of different kinds (\eg{} Boolean, integers, or even sets), and \glspl{constraint}, Boolean logic formulas which are forced to hold in any \gls{sol}, and, in case of an \gls{opt-prb}, an \gls{objective}. - Any external data required to formulate the \glspl{constraint} is said to be the \glspl{parameter}. - The combination of a constraint model and \gls{assignment}s for its \glspl{parameter} is said to be an \gls{instance} of the constraint model + Any external data required to formulate the \glspl{constraint} is said to be the \glspl{prb-par}. + The combination of a constraint model and \gls{assignment}s for its \glspl{prb-par} is said to be an \gls{instance} of the constraint model }, } @@ -384,7 +385,7 @@ \newglossaryentry{gls-mip}{ name={mixed integer programming}, description={ - A solving technique tries to find the \gls{opt-sol} for a \cmodel{} containing a mixture of Integer and floating point \glspl{variable} subject to \glspl{constraint} in the form of linear equations. + A solving technique tries to find the \gls{opt-sol} for a \cmodel{} containing a mixture of Integer and floating point \glspl{variable} subject to \glspl{constraint} in the form of linear (in-)equations. Mixed integer programming is extensively studied and there are many successful \glspl{solver} dedicated to solving mixed integer programs. See \cref{subsec:back-mip} }, @@ -437,7 +438,7 @@ \newglossaryentry{optional}{ name={optional}, - description={When it is not certain if a value, either \gls{variable} or \gls{parameter}, will exist in a \gls{minizinc} model, its type is marked as optional (\mzninline{opt}). If the value does not occur it is said to be absent.}, + description={When it is not certain if a value, either \gls{variable} or \gls{parameter}, will exist in a \gls{minizinc} \instance{}, its type is marked as optional (\mzninline{opt}). If the value does not occur it is said to be absent.}, } \newglossaryentry{opt-sol}{ @@ -517,11 +518,11 @@ } \newglossaryentry{parameter}{ - name={problem parameter}, + name={parameter}, description={ - Problem parameters are part of the external input for a \gls{model}. - They can be used as immutable data used to define \glspl{constraint} or provide structural information about an \gls{instance}. - For example, a problem parameter can influence the number of \glspl{constraint} in an \gls{instance} + Parameter variables, shortened to parameters, are variables in the sense of programming languages, and are not to be confused with \glspl{variable}. + In \minizinc{}, a parameter variable represents a value that will be known during \gls{rewriting}. + Examples of such values are \glspl{prb-par}, the result of introspection (such as \mzninline{dom(x)}, returning the current domain of a \gls{variable} \mzninline{x}), or the result of calculations over other parameter variables. }, } @@ -532,9 +533,19 @@ \newglossaryentry{partial}{ name={partial}, - description={A function is said to be partial when it does not have a defined result for every possible input. Similarly, an \gls{assignment} is said to be partial when it maps only a subset of the \glspl{parameter} and \glspl{variable} in a \gls{model}.}, + description={A function is said to be partial when it does not have a defined result for every possible input. Similarly, an \gls{assignment} is said to be partial when it maps only a subset of the \glspl{prb-par} and \glspl{variable} in a \gls{model}.}, } +\newglossaryentry{prb-par}{ + name={problem parameter}, + description={ + Problem parameters are part of the external input for a \gls{model}. + They can be used as immutable data used to define \glspl{constraint} or provide structural information about an \gls{instance}. + For example, a problem parameter can influence the number of \glspl{constraint} in an \gls{instance} + }, +} + + \newglossaryentry{propagation}{ name={constraint propagation}, description={The removal of values from \glspl{domain} of \glspl{variable} that violate a \gls{constraint}. See \cref{subsec:back-cp}}, diff --git a/assets/listing/back_sgp.mzn b/assets/listing/back_sgp.mzn index 8000164..e413bb2 100644 --- a/assets/listing/back_sgp.mzn +++ b/assets/listing/back_sgp.mzn @@ -4,7 +4,7 @@ include "globals.mzn"; 1..infinity: ngroups; 1..infinity: size; -enum: golfers = anon_enum(ngroups * size); +enum golfers = anon_enum(ngroups * size); set of int: groups = 1..g; set of int: Rounds = 1..w; diff --git a/assets/listing/back_tsp.mod b/assets/listing/back_tsp.mod index ef8ea36..3e37ea1 100644 --- a/assets/listing/back_tsp.mod +++ b/assets/listing/back_tsp.mod @@ -4,15 +4,12 @@ param cost {Paths} >= 0;@\Vlabel{line:back:ampl:parend}@ var Take {Paths} binary;@\Vlabel{line:back:ampl:var}@ -param n := card {Cities};@\Vlabel{line:back:ampl:compstart}@ -set SubSets := 0 .. (2**n - 1); -set PowerSet {k in SubSets} := {i in Cities: (k div 2**(ord(i)-1)) mod 2 = 1};@\Vlabel{line:back:ampl:compend}@ - minimize TotalCost: sum {(i,j) in Paths} cost[i,j] * Take[i,j];@\Vlabel{line:back:ampl:goal}@ subj to Tour {i in S}:@\Vlabel{line:back:ampl:con1}@ sum {(i,j) in Paths} Take[i,j] + sum {(j,i) in Paths} Take[j,i] = 2; -subj to SubtourElimation {k in SubSet diff {0,2**n-1}}:@\Vlabel{line:back:ampl:con2}@ - sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (i,j) in Paths} X[i,j] + - sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (j,i) in Paths} X[j,i] >= 2; +var Order {Cities} >= 1, <= card(Cities);@\Vlabel{line:back:ampl:compstart}@ +let Order[first(Cities)] = 1; +subj to SubtourElimation {(i,j) in Cities: ord(i) < ord(j)}: + (Order[i] - Order[j] + card(Cities)*Take[i,j]) <= (card(Cities) - 1);@\Vlabel{line:back:ampl:compend}@ diff --git a/assets/shorthands.tex b/assets/shorthands.tex index 6f714ed..58484af 100644 --- a/assets/shorthands.tex +++ b/assets/shorthands.tex @@ -26,6 +26,8 @@ \newcommand*{\cmodel}{\gls{model}\xspace} \newcommand*{\cmodels}[0]{\glspl{model}\xspace} \newcommand*{\nanozinc}{\gls{nanozinc}\xspace} +\newcommand*{\prbpar}{\gls{prb-par}\xspace} +\newcommand*{\prbpars}{\glspl{prb-par}\xspace} \newcommand*{\parameters}{\glspl{parameter}\xspace} \newcommand*{\parameter}{\gls{parameter}\xspace} \newcommand*{\reified}{\gls{reified}\xspace} diff --git a/chapters/1_introduction.tex b/chapters/1_introduction.tex index be3621e..3015f2d 100644 --- a/chapters/1_introduction.tex +++ b/chapters/1_introduction.tex @@ -30,8 +30,8 @@ Two \solvers{} designed to solve the same problem class can perform very differe \Cmls{} have been designed to tackle these issues. 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 \gls{assignment} of the \parameters{}, the \cmodel{} forms an \instance{}. +A \cmodel{} can generally describe a class of problems through the use of \prbpars{}, values assigned by external input. +Once given a complete \gls{assignment} of the \prbpars{}, the \cmodel{} forms an \instance{}. The \instance{} is transformed into a \gls{slv-mod} through a process class \gls{rewriting}. A commonly used \cml{} is \glsxtrshort{ampl} \autocite{fourer-2003-ampl}. @@ -56,7 +56,7 @@ As an \gls{opt-prb}, our goal is to find a schedule that minimises the finishing \end{listing} \Cref{lst:intro-open-shop} shows an \glsxtrshort{ampl} model for the open shop problem. -In order of occurence, \lrefrange{line:intro:param:start}{line:intro:param:end} show the declarations of the \parameters{}. +In order of occurence, \lrefrange{line:intro:param:start}{line:intro:param:end} show the declarations of the \prbpars{}. To create an \instance{} of the problem, the user provides the number of jobs and machines that are considered, and the duration of each task. \Lrefrange{line:intro:var:start}{line:intro:var:end} show the \variable{} declarations: for each task we decide on its start time. Additionally, we declare the end time of the last task as a \variable{}, to ease the modelling of the problem. @@ -108,7 +108,7 @@ As such, a \gls{clp} program is not \solver{}-independent. Like \glsxtrshort{ampl}, it is a \solver{}-independent \cml{}. And like \gls{clp} languages, modellers can declare common concepts and control the encoding into the \gls{slv-mod}. The latter is accomplished through the use of function definitions. -For example, a user could create the following \minizinc{} function to express the non-overlapping relationship. +For example, a user could create the following \minizinc{} function to express the non-overlapping relation. \begin{mzn} function var bool: non_overlap( @@ -173,7 +173,7 @@ In particular: \begin{itemize} - \item The \minizinc{} \compiler{} is inefficient. + \item The existing implementation of \minizinc{} is inefficient. It does a surprisingly large amount of work for each expression (especially resolving sub-typing and overloading), which may be repeated many times. And as models generated for low-level \solver{} technologies can be quite large, the resulting \gls{rewriting} procedure can be intolerably slow. As the model transformations implemented in \minizinc{} become more sophisticated, these performance problems are simply magnified. @@ -236,7 +236,7 @@ Overall, this thesis makes the following contributions: \item It presents a design and implementation of techniques to automatically introduce \gls{half-reif} of \constraints{} in \minizinc{}. - \item It develops a technique to simplify problem specifications by efficiently eliminating implication chains. + \item It develops a technique to simplify \glspl{slv-mod} by efficiently eliminating \glspl{implication-chain}. \item It proposes two novel methods to reduce the overhead of using \cmls{} in incremental techniques: \gls{rbmo} and the \gls{incremental-rewriting} of changing \instances{}. @@ -251,7 +251,7 @@ First, it introduces the reader to \minizinc{}, how its models are formulated, a Then, we review different solving methods such as \gls{sat}, \gls{mip}, and \gls{cp}. This is followed by a comparison of \minizinc{} with other \cmls{}. This chapter also reviews techniques that are closely related to \cmls{}. -We conclude this chapter with a description of the current \minizinc{} compiler and the techniques it uses to simplify the \solver{} specifications it produces. +We conclude this chapter with a description of the current \minizinc{} compiler and the techniques it uses to simplify the \glspl{slv-mod} it produces. \emph{\Cref{ch:rewriting}} presents a formal execution model for \minizinc{} and the core of our new architecture. We construct a set of formal rewriting rules for a subset of \minizinc{} called \microzinc{}. diff --git a/chapters/2_background.tex b/chapters/2_background.tex index b7b8829..4f752ae 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -9,32 +9,32 @@ \section{Introduction to Constraint Modelling Languages} \label{sec:back-intro} -A goal shared between all programming languages is to provide a certain level of abstraction to its users. -Reduce the complexity by hiding unnecessary information. +A goal shared between all programming languages is to provide a certain level of abstraction to their users. +This reduces the complexity of the programming tasks by hiding unnecessary information. For example, an assembly language allows you to abstract from the machine instructions and memory positions that are used by the hardware. And, early imperative programming languages, like FORTRAN, were the first to offer abstraction from the processor architecture of the targeted system. Consequently, in current times, writing a computer program requires little knowledge of how the targeted computer system operates. -\textcite{freuder-1997-holygrail} states that the ``Holy Grail'' of programming languages would be where the user merely states the problem, and the computer solves it and that \constraint{} modelling is one of the biggest steps towards this goal to this day. -\Cmls{} operate different from other computer languages. +\textcite{freuder-1997-holygrail} states that the ``Holy Grail'' of programming languages would be where the user merely states the problem, and the computer solves it, and that \constraint{} modelling is one of the biggest steps towards this goal to this day. +\Cmls{} operate differently from other computer languages. 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 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 elements of a \cmodel{} include \prbpars{}, what we already know; \variables{}, what we wish to know; and \constraints{}, the relations that should exist between them. +Through the variation of \prbpars{}, a \cmodel{} describes a full class of problems. +A specific problem is captured by an \instance{}, the combination of a \cmodel{} with a complete \gls{parameter-assignment} (\ie{} a mapping from all \prbpars{} 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{}. +The goal of a \gls{dec-prb} is to find a \gls{sol}: a complete \gls{variable-assignment} that satisfies the \constraints{}. 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}. +Many \cmls{} also support the modelling of \glspl{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}. 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{}. To solve these \instances{}, however, they can go through a \gls{rewriting} process to arrive at a \gls{slv-mod}, input accepted by a \solver{}. The \solver{} then uses a dedicated algorithm that finds a \gls{sol} that fits the requirements of the \instance{}. -This process of a \cml{} is visualised in \cref{fig:back-cml-flow}. +This process is visualised in \cref{fig:back-cml-flow}. \begin{figure} \centering @@ -48,7 +48,7 @@ This process of a \cml{} is visualised in \cref{fig:back-cml-flow}. 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 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}: + The following set of equations describes this knapsack problem as an \gls{opt-prb}: \begin{equation*} \text{maximise}~z~\text{subject to}~ @@ -64,20 +64,15 @@ This process of a \cml{} is visualised in \cref{fig:back-cml-flow}. 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 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. + The \prbpars{} \(T\) is the set of all available toys. + The \(joy\) and \(space\) functions are \prbpars{} used to map toys, \( t \in T\), to a numeric value describing the amount of enjoyment and space required respectively. + Finally, the \prbpar{} \(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, the \instances{} have to be rewritten into input accepted by a \solver{}. \Cmls{} are designed to allow the modeller to express combinatorial problems similar to the above mathematical definition and generate input that can be directly used by dedicated \solvers{}. \end{example} -% \begin{listing} -% \pyfile{assets/listing/2_dyn_knapsack.py} -% \caption{\label{lst:2-dyn-knapsack} A Python program that solves a 0-1 knapsack problem using dynamic programming} -% \end{listing} - \section{\glsentrytext{minizinc}}% \label{sec:back-minizinc} @@ -90,18 +85,18 @@ Its expressive language and extensive library of \glspl{global} allow users to e Let us introduce the language by modelling the problem from \cref{ex:back-knapsack}. A \minizinc{} model encoding this problem is shown in \cref{lst:back-mzn-knapsack}. - The model starts with the declaration of the \parameters{}. + The model starts with the declaration of the \prbpars{}. \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 \glspl{array} \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 the integer \parameter{} \mzninline{total_space} to represent the remaining car capacity, equivalent to \(C\). + Finally, \lref{line:back:knap:left} declares the integer \prbpar{} \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. This is \(S\) in our earlier model. We also declare the \variable{} \mzninline{total_joy}, on \lref{line:back:knap:tj}, which is functionally defined to be the summation of all the joy for the toy picked in our selection. - The model, then contains a \constraint{}, on \lref{line:back:knap:con}, which ensures we do not exceed the given capacity. + The model then contains a \constraint{}, on \lref{line:back:knap:con}, which ensures we do not exceed the given capacity. Finally, it states the goal for the \solver{}: to maximise the value of the \variable{} \mzninline{total_joy}. \end{example} @@ -113,18 +108,17 @@ Its expressive language and extensive library of \glspl{global} allow users to e 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 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{}. +It first needs to be transformed into a \gls{slv-mod}: a list of \variables{} and \constraints{} that are directly supported as input by the \solver{}. +We call these types of \variables and \constraints{} \gls{native} to the \solver{}. 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}. +The process to transform a \minizinc{} instance into a \gls{slv-mod} is called \gls{rewriting}. \Glspl{slv-mod} for \minizinc{} \solvers{} are generally represented in \flatzinc{}. \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} - - For example, given the \minizinc{} model in \cref{lst:back-mzn-knapsack} and the following \gls{assignment} will result in the \flatzinc{} \gls{slv-mod} in \cref{lst:back-fzn-knapsack}. + For example, the \minizinc{} model in \cref{lst:back-mzn-knapsack} and the following \gls{assignment} can form a \minizinc{} \instance{}. \begin{mzn} TOYS = {football, tennisball, stuffed_elephant}; @@ -133,16 +127,27 @@ It is the primary way in which \minizinc{} communicates with \solvers{}. space_left = 44; \end{mzn} - \begin{listing} - \mznfile{assets/listing/back_knapsack.fzn} - \caption{\label{lst:back-fzn-knapsack} A \flatzinc{} \gls{slv-mod} resulting from \gls{rewriting} \cref{lst:back-mzn-knapsack} with a given complete \gls{parameter-assignment}.} - \end{listing} + The modeller can then choose a \solver{}. + Let us assume we choose a \gls{mip} \solver{}, whose \gls{native} \variables{} are only integer \variables{} and whose \gls{native} \constraints{} are only linear \constraints{}. + \Gls{rewriting} the \instance{} would result in the \flatzinc{} \gls{slv-mod} in \cref{lst:back-fzn-knapsack}. + The set type \variable{} \mzninline{selection} is now represented using three integer \variables{}, \mzninline{selection_@\(i\)@}. + Each represent whether an element is present in the set. + They take the value one if the element is present, and zero otherwise. + The sum-\constraints{} have been transformed into integer linear \constraints{}, \mzninline{int_lin_le} and \mzninline{int_lin_eq}. + The former constrains that the selection \variables{} multiplied by the space required for the represented element and ensures their sum is smaller than the available space. + The latter calculates the value of the \mzninline{total_joy} \variable{} by adding together selection \variables{} multiplied by the joy value of the represented element. + In these \constraints{}, the \prbpars{} are merely represented by the values given in the \gls{parameter-assignment}. + Their names are no longer present in the \gls{slv-mod}. - This \gls{slv-mod} is then passed to a \solver{}. - The \solver{} attempts to determine a complete \gls{variable-assignment}, \mzninline{selection_@\(i\)@} and \mzninline{total_joy}, that satisfies all \constraints{} and maximises \mzninline{total_joy}. + This \gls{slv-mod} is then passed to the targeted \solver{}. + The \solver{} attempts to determine a complete \gls{variable-assignment} and maximise the \gls{assignment} of the \mzninline{total_joy} \variable{}. If there is no such \gls{assignment}, then it reports that the \gls{slv-mod} is \gls{unsat}. - \end{example} +\begin{listing} + \mznfile{assets/listing/back_knapsack.fzn} + \caption{\label{lst:back-fzn-knapsack} A \flatzinc{} \gls{slv-mod} for a \gls{mip} \solver{}, resulting from \gls{rewriting} \cref{lst:back-mzn-knapsack} with a given complete \gls{parameter-assignment}.} +\end{listing} + \subsection{Model Structure}% \label{subsec:back-mzn-structure} @@ -150,7 +155,7 @@ It is the primary way in which \minizinc{} communicates with \solvers{}. 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, + \item \variables{} and \prbpars{} are found in the form of variable declarations, \item \constraints{} are explicitly defined using their own keyword, \item and the \gls{objective} is included as a solving goal. \end{itemize} @@ -160,26 +165,33 @@ These items are not constrained to occur in any particular order. 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}. +\textcite{nethercote-2007-minizinc} offer a detailed discussion of \minizinc{}. +And, much of its history can be learned from the description of its predecessor, \zinc{} \autocite{marriott-2008-zinc}. -\paragraph{Declaration Items} Values in \minizinc{} are declared in the form \mzninline{@\(T\)@: @\(I\)@ = @\(E\)@}, where: +\paragraph{Variable Declaration Items} Variables are declared using variable declaration items. +The term ``variable'' has two overlapping, and slightly confusing meanings. +As a programming language, \minizinc uses it to describe a distinct object that contains (currently unknown) information. +As such, a variable in \minizinc{} can be used to represent either a \variable{}, as defined before, or a \gls{parameter} variable. +The latter is used to represent any information that will be known during \gls{rewriting}. +This includes \prbpars{}, but also the result of introspection, or the result of calculations over other \parameters{}. +In the remainder of this thesis we will refer to \parameter{} variables merely as \parameters{}, but will distinguish them from \variables{}. + +Variable declarations are stated in the form \mzninline{@\(T\)@: @\(I\)@ = @\(E\)@}, where: \begin{itemize} - \item \(T\) is the type of the declared value, + \item \(T\) is the type instance of the declared value, \item \(I\) is a new identifier used to reference the declared value, \item and the modeller can functionally define the value using an expression \(E\). \end{itemize} The syntax \mzninline{= @\(E\)@} is optional. -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. +It is omitted when a \variable{} has no functional definition, or when a \parameter{} is a \prbpar{} and assigned externally. +The identifier used in a top-level variable declaration must be unique. 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 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}. +The declaration of \parameters{} and \variables{} are distinguished through the instance of these types. +In the type instance of a \variable{}, the type is preceded by the \mzninline{var} keyword. +In the type instance of a \parameter{}, the type can similarly be marked by the \mzninline{par} keyword, but this is not required. +\minizinc{} allows collections of these types to be contained in \glspl{array}. 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, the following declaration declares an array going from 5 to 10 of new Boolean \variables{}. @@ -199,31 +211,31 @@ The first takes the values from three to five and the second takes the values on var {1,3,5}: y; \end{mzn} -If a declaration does include a functional definition, then the identifier is merely a name given to the expression. +If a declaration includes 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. -The \gls{rewriting} of the model translated the expressions in \constraints{} into versions of the same expression that are \gls{native} to the \solver{}. +The \gls{rewriting} of the \instance{} translates the expressions in \constraints{} into \constraints{} and potentially additional \variables{} 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}. +This means that the \constraints{} in the \solver{} are \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 signals the solver to do one of three actions: +This item signals the \solver{} to perform one of three actions: -\begin{itemize} - \item \mzninline{solve satisfy} --- to find an \gls{assignment} to the \variables{} that satisfies the \constraints{}, - \item \mzninline{solve minimize @\(E\)@} --- to find an \gls{assignment} to the \variables{} that satisfies the \constraints{} and minimises the value of the expression \(E\), - \item or \mzninline{solve maximize @\(E\)@} --- to similarly maximise the value of the expression \(E\). -\end{itemize} +\begin{description} + \item[\mzninline{solve satisfy}] to find an \gls{assignment} to the \variables{} that satisfies the \constraints{}, + \item[\mzninline{solve minimize @\(E\)@}] to find an \gls{assignment} to the \variables{} that satisfies the \constraints{} and minimises the value of the expression \(E\), or + \item[\mzninline{solve maximize @\(E\)@}] to similarly maximise the value of the expression \(E\). +\end{description} \noindent{}The first type of goal indicates that the problem is a \gls{dec-prb}. -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. +The other two types of goals are used when the model describes an \gls{opt-prb}. +If the model does not contain a goal item, then the problem is assumed to be a \gls{dec-prb}. \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: +A functions is declared using the syntax \mzninline{function @\(T\)@: @\(I\)@(@\(P\)@) = @\(E\)@}, where: \begin{itemize} \item \(T\) is the type of its result; \item \(I\) is its identifier; @@ -231,7 +243,7 @@ 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{}\Gls{rewriting} replaces a call to a function by its body instantiated the arguments given in the call. +\noindent{}\Gls{rewriting} replaces a call to a function by its body instantiated with 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 as follows. @@ -242,20 +254,20 @@ As an example, we can define a function that squares an integer as follows. \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. +The collection of function declarations to rewrite for a \solver{} is generally referred to as a \solver{} library. In this library, functions can be declared without a function body. 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 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. +Instead, they can rely on a set of standard declarations, 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 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. +We now briefly discuss the most important types 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}. These expressions capture common (complex) relations between \variables{}. @@ -272,11 +284,11 @@ The following is an example of a \gls{global}. ); \end{mzn} -This \gls{global} expresses the knapsack relationship, where the argument: +This \gls{global} expresses the knapsack relation, with the following arguments: \begin{itemize} \item \mzninline{w} are the weights of the items, - \item \mzninline{p} are the profit for each item, - \item the \variables{} in \mzninline{x} represent the amount of time the items are present in the knapsack, + \item \mzninline{p} are the profits for each item, + \item the \variables{} in \mzninline{x} represent how many of each item are present in the knapsack, \item and \mzninline{W} and \mzninline{P}, respectively, represent the weight and profit of the knapsack \end{itemize} @@ -288,7 +300,7 @@ Note that using this \gls{global} as follows would have simplified the \minizinc \end{mzn} \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 can be marked as \gls{native} \constraint{}. +The \constraint{} can be rewritten using a specialised \gls{decomp} provided by the \solver{} or it can be marked as a \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 help modellers express complex \constraints{}. @@ -305,20 +317,20 @@ Consider, for example, the following \constraint{} \Gls{operator} symbols in \minizinc{} are a shorthand for \minizinc{} functions. 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}. +Although the \gls{operator} syntax for \variables{} and \parameters{} is the same, different (overloaded) versions of these functions are 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. +However, \gls{rewriting} functions with \variable{} as arguments results in a new \variable{} that is constrained to the result of the function. -\paragraph{Conditional Expression} The choice between different expressions are often expressed using a \gls{conditional} expression, also known as an ``if-then-else'' expression. +\paragraph{Conditional Expression} The choice between different expressions is 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; \end{mzn} -The result of a \gls{conditional} expression is not contained to Boolean types. +The result of a \gls{conditional} expression is not limited 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 \gls{conditional} expression. -This can be used to, for example, define an absolute value function for integer \parameter{} as follows. +This can be used to, for example, define an absolute value function an integer as follows. \begin{mzn} function int: abs(int: a) = @@ -327,8 +339,8 @@ This can be used to, for example, define an absolute value function for integer When the condition does not contain any \variables{}, then the \gls{rewriting} process merely has to choose the correct side of the expression. If, however, the condition does contain a \variable{}, then the result of the expression cannot be defined during \gls{rewriting}. -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. +Instead, an \gls{avar} is created and a \constraint{} is added to ensure that it takes the correct value. +A special \mzninline{if_then_else} \glspl{global} is available to implement this relation. \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 \gls{array} \mzninline{a}. @@ -336,21 +348,21 @@ Note this is not necessarily the \(\mzninline{i}^{\text{th}}\) element because \ 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{}. +If the expression is a \gls{variable}, then the expression is rewritten to an \gls{avar} and an \mzninline{element} \constraint{}. 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 which are used to compose \gls{array} objects. +\paragraph{Comprehensions} \Gls{array} \glspl{comprehension} are expressions which allows modellers to construct \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: +\Gls{comprehension} expressions \mzninline{[@\(E\)@ | @\(G\)@ where @\(F\)@]} consist of three parts: \begin{description} - \item[\(G\)] The generator expression which assigns the values of collections to identifiers, + \item[\(G\)] The \gls{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 \gls{array}, \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}. +The following example constructs an \gls{array} that contains the tripled even values of an \gls{array} \mzninline{x}. \begin{mzn} [ xi * 3 | xi in x where x mod 2 == 0] @@ -363,7 +375,7 @@ Since we then cannot decide during \gls{rewriting} if an element is present in t This means that the \solver{} still will decide if the element is present in the \gls{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. +A \gls{let} allows a modeller to provide a list of declarations, that can only be used in the body of the \gls{let}. Additionally, a \gls{let} can contain \constraints{} to constrain the declared values. There are three main purposes for \glspl{let}. @@ -385,7 +397,7 @@ There are three main purposes for \glspl{let}. \item It can constrain the resulting expression. - For example, the following function returns an \gls{ivar} \mzninline{z} that is constrained to be the multiplication of \mzninline{x} and \mzninline{y} by the relational multiplication \constraint{} \mzninline{pred_int_times}. + For example, the following function returns an \gls{avar} \mzninline{z} that is constrained to be the multiplication of \mzninline{x} and \mzninline{y} by the relational multiplication \constraint{} \mzninline{pred_int_times}. \begin{mzn} function var int: int_times(var int: x, var int: y) = @@ -398,10 +410,10 @@ 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 may 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 evaluated multiple times when used in loops, function definitions (that are called multiple times), and \gls{array} \glspl{comprehension}. +Different to \variables{} declared directly in declaration items, the \variables{} declared in \glspl{let} can be evaluated 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 provides the modeller with 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. @@ -414,10 +426,9 @@ Through the use of an \gls{annotation} on the solving goal item, the modeller ca \label{subsec:back-reif} 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 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\). +The sub-expressions of a complex expressions are often rewritten into \glspl{avar}. +If the sub-expression, and therefore \gls{avar}, is of Boolean type, then it needs to be rewritten into a \gls{reified} \constraint{}. +The \gls{reif} of a \constraint{} \(c\) creates an Boolean \gls{avar} \mzninline{b}, also referred to as its \gls{cvar}, constrained to be the truth-value of this \constraint{}: \(\texttt{b} \leftrightarrow{} c\). \begin{example} Consider the following \minizinc{} model. @@ -429,7 +440,9 @@ The \gls{reif} of a \constraint{} \(c\) creates an \gls{ivar} \mzninline{b} cons \end{mzn} This model maximises the number of even numbers taken by the elements of the \gls{array} \mzninline{x}. - In this model the expression \mzninline{x[i] mod 2 == 0} has to be reified. + In this model the expression \mzninline{x[i] mod 2 == 0} has to be \gls{reified}. + This means that for each \mzninline{i}, a \gls{cvar} \mzninline{b_i} is added, together with a constraint that makes \mzninline{b_i} true if-and-only-if \mzninline{x[i] mod 2 = 0}. + We can then add up the values of all these \mzninline{b_i}, as required by the maximisation. 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 sets to \mzninline{true}. \end{example} @@ -441,10 +454,10 @@ In \minizinc{}, almost all expressions can be used in both \rootc{} and non-\roo \subsection{Handling Undefined Expressions}% \label{subsec:back-mzn-partial} -In this subsection we discuss the handling of partial expressions in \cmls{} as studied by \textcite{frisch-2009-undefinedness}. +In this subsection we discuss the handling of partial functions in \cmls{} as studied by \textcite{frisch-2009-undefinedness}. -When an expression has a well-defined result it is said to be total. -Some expressions in \cmls{}, however, do not have well-defined results. +When an function has a well-defined result for all its possible inputs it is said to be total. +Some expression in \cmls{}, however, are rewritten into functions that do not have well-defined results for all possible inputs. Part of the semantics of a \cml{} is the choice as to how to treat these partial functions. \begin{example}\label{ex:back-undef} @@ -454,14 +467,15 @@ Part of the semantics of a \cml{} is the choice as to how to treat these partial constraint i <= 4 -> a[i] * x >= 6; \end{mzn} - \noindent{}It requires that if \mzninline{i} takes a value less or equal to four, then the value in the \texttt{i}\(^{th}\) position of \gls{array} \mzninline{a} multiplied by \mzninline{x} must be at least 6. + \noindent{}It requires that if \mzninline{i} takes a value less or equal to four, then the value in the \texttt{i}\(^{th}\) position of \gls{array} \mzninline{a} multiplied by \mzninline{x} must be at least six. - Suppose the \gls{array} \texttt{a} has index set \mzninline{1..5}, but \texttt{i} takes the value \texttt{7}. - The expression \mzninline{a[i]} fails and no \gls{sol} is found. + Suppose the \gls{array} \texttt{a} has index set \mzninline{1..5}, but \texttt{i} takes the value seven. + This means the expression \mzninline{a[i]} undefined. + If \minizinc{} did not implement any special handling for partial functions, then the whole expression would have to be marked as undefined and no \gls{sol} is found. However, intuitively if \mzninline{i = 7} the \constraint{} should be trivially true. \end{example} -Other examples of \minizinc{} expressions that result in partial functions are: +Other examples of partial functions in \minizinc{} are: \begin{itemize} \item division (or modulus) when the divisor is zero, @@ -470,7 +484,7 @@ Other examples of \minizinc{} expressions that result in partial functions are: x div 0 = @??@ \end{mzn} - \item finding the minimum or maximum or an empty set, + \item finding the minimum or maximum of an empty set, \begin{mzn} min({}) = @??@ @@ -496,34 +510,32 @@ There is both the question of what happens when an undefined expression is evalu 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 is only marked as undefined if the value of the sub-expression is required to compute its result. + If an expression contains an 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 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 does 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)} is said to be \mzninline{false}. + So even though a (functional) expression does not have a well-defined result, we can still decide whether its surrounding relation holds. + For example, the expression \mzninline{x div 0} is undefined, but the relation \mzninline{int_div(x, 0, y)} is said to be \mzninline{false}. + There are no possible values for \mzninline{x} and \mzninline{y} such that the relation holds. It can be said that the relational semantic makes the closest relational expression that contains an undefined expression \mzninline{false}. \end{description} In practice, it is often natural to guard against undefined behaviour using Boolean logic. \Glspl{rel-sem} therefore often feel the most natural for the users of \glspl{cml}. -This is why the \minizinc{} uses \glspl{rel-sem} during its evaluation. +This is why \minizinc{} uses \glspl{rel-sem} during its evaluation. -For example, the following \constraint{} shows how we can deal with a zero divisor using a disjunction. - -\begin{mzn} - constraint d == 0 \/ a div d < 3; -\end{mzn} - -In this case we expect the undefinedness of the division to be contained within the second part of the disjunction. -This corresponds to \glspl{rel-sem}. +If we, for example, reconsider the \constraint{} from \cref{ex:back-undef}, we will find that \glspl{rel-sem} will correspond to the intuitive expectation. +When \mzninline{i} takes the value seven, the expression \mzninline{a[i]} is undefined. +Its closest Boolean context will take the value false. +In this case, that means the right hand side of the implication becomes false. +However, since the left hand side of the implication is also false, the \constraint{} is \gls{satisfied}. \textcite{frisch-2009-undefinedness} also show that different \solvers{} often employ different semantics. -It is therefore important that the \gls{rewriting} process replaces any potentially undefined expression by an \gls{eqsat} expression that is valid under a \gls{strict-sem}. -This essentially eliminates the existence of undefined expressions in the \gls{slv-mod}. +\minizinc{} therefore implements the \glspl{rel-sem} by translating any potentially undefined expression into an expression that is always defined, by introducing appropriate \glspl{avar} and \gls{reified} \constraints{}. +That way, the solving result is independent of the semantics of the chosen \solver{}, and always consistent with the \glspl{rel-sem} of the model. \section{Solving Constraint Models}% \label{sec:back-solving} @@ -538,19 +550,19 @@ It depends on which \constraints{} are \gls{native} to the targeted \gls{cp} \so In some ways \gls{cp} \solvers{} work on a similar level as the \minizinc{} language. 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{}. +The usage of these techniques shrinks the \domains{} of \variables{} and eliminates or simplifies \constraints{}. \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 discusses the other dominant technologies used by \minizinc{} \solver{} and their \glspl{slv-mod}. +Although these \solvers{} allow new classes of problems 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 discusses the other dominant technologies used by \minizinc{} \solvers{} and their \glspl{slv-mod}. \subsection{Constraint Programming}% \label{subsec:back-cp} \glsreset{cp} When given an \instance{} of a \cmodel{}, one may wonder how to find a \gls{sol}. -The simplest solution would be to apply ``brute force'': try every value in the \domains{} of all \variables{}. +The simplest algorithm would be to apply ``brute force'': try every value in the \domains{} of all \variables{}. This is an inefficient approach. Consider, for example, the following \constraint{}. @@ -564,14 +576,14 @@ Therefore, only that one value for \mzninline{b} has to be tried. 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. +\Gls{propagation} works through the use of \glspl{propagator}: algorithms dedicated to a specific \constraint{} that prune \domains{} when they contain 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 \domain{} of one of its \variables{} has changed. If a \gls{propagator} can prove that it is always \gls{satisfied}, then it is subsumed: it never has to be run again. 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 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. +Often, \gls{propagation} alone is not enough to find a \gls{sol}. +When we reach a \gls{fixpoint}, where no more \domain{} reductions are performed, and no \gls{sol} is found, the \solver{} then has to make a search decision. 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{}. @@ -584,7 +596,7 @@ A \gls{cp} \solver{} is only able to prove that the \instance{} is \gls{unsat} b 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 keep track of \gls{domain} changes using a \gls{trail} data structure \autocite{warren-1983-wam}. +The most common method in \gls{cp} \solvers{} to keep track of \gls{domain} changes uses a \gls{trail} data structure \autocite{warren-1983-wam}. 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 reverses all changes until it reaches the change that is tagged with the search decision. @@ -593,16 +605,16 @@ Furthermore, because \gls{propagation} is performed to a \gls{fixpoint}, it is g 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}. +Similarly, \solvers{} do not all have implementations for the same \glspl{propagator}. Therefore, a \gls{slv-mod} for one \solver{} looks 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}. +\Cmls{}, like \minizinc{}, serve as a standardised form of input for these \solvers{}. +They allow modellers to 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}% \label{ex:back-nqueens} - As an example of the \gls{propagation} mechanism, let us consider as an example the N-Queens problem. + As an example of the \gls{propagation} mechanism, let us consider the N-Queens problem. Given a chessboard of size \(n \times n\), find a placement for \(n\) queen chess pieces such that no queen can attack another. - Meaning only one queen per row, one queen per column, and one queen per diagonal. + This means we can only place one queen per row, one queen per column, and one queen per diagonal. The problem can be modelled in \minizinc\ as follows. \begin{mzn} @@ -617,10 +629,10 @@ They allow modellers to use always use \glspl{global} and depending on the \solv \end{mzn} 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. + This automatically restricts 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. + The \constraints{} model the remaining rules of the problem: no two queens can be placed in the same row, no two queen can be placed in the same upward diagonal, and no two queens can be placed in the same downward diagonal. + For many \gls{cp} \solvers{} this model is close to a \gls{slv-mod}, 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 happens when the first queen is placed on the board, the first search decision. @@ -628,7 +640,7 @@ They allow modellers to use always use \glspl{global} and depending on the \solv \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{} now stops other queens from being placed in the same column. + As shown 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}. @@ -662,25 +674,25 @@ They allow modellers to use always use \glspl{global} and depending on the \solv \caption{\label{fig:back-nqueens} An example of domain propagation when a queen gets assigned in the N-Queens problem.} \end{figure} -In \gls{cp} solving there is a trade-off between the amount of time spend propagating a \constraint{} and the amount of search that is otherwise required. -The golden standard for a \gls{propagator} is to be \gls{domain-con}. +In \gls{cp} solving there is a trade-off between the amount of time spent propagating a \constraint{} and the amount of search that is otherwise required. +The gold 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 can require high computational complexity. Instead, it is sometimes be better to use a propagator with a lower level of consistency. -Although it does not eliminate all possible values of the domain, searching the values that are not eliminated may take less time than achieving \gls{domain-con}. +Although it does not eliminate all possible values of the domain, searching the values that are not eliminated may take less time than achieving domain consistency. 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{}. For these \constraints{}, no realistic \gls{domain-con} \gls{propagator} exists because the problem is \gls{np}-hard \autocite{choi-2006-fin-cons}. -Instead, \solvers{} generally use a \gls{bounds-con} \gls{propagator}, which guarantee only that the minimum and maximum values in the \glspl{domain} of the \variables{} are used in at least one possible \gls{assignment} that satisfies the \constraint{}. +Instead, \solvers{} generally use a \gls{bounds-con} \gls{propagator}, which guarantees only that the minimum and maximum values in the \glspl{domain} of the \variables{} are used in at least one possible \gls{assignment} that satisfies the \constraint{}. 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}. +\gls{cp} solving can, however, also be used to solve \glspl{opt-prb} using a method called \gls{bnb}. 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. -This is achieved by adding a new \gls{propagator} that enforces a better objective value than the incumbent \gls{sol}. +The \solver{} must therefore resume its search, but it is no longer interested in just any \gls{sol}, only \glspl{sol} for which the \gls{objective} returns a better value. +This is achieved by adding a new \constraint{} that enforces a better objective value than the incumbent \gls{sol}. If the search process finds another \gls{sol}, then the incumbent \gls{sol} is updated and the search process continues. If the search process does not find any other \glspl{sol}, then it is proven that there are no better \glspl{sol} than the current incumbent \gls{sol}. It is an \gls{opt-sol}. @@ -692,56 +704,57 @@ It is an \gls{opt-sol}. \glsreset{lp} \glsreset{mip} -\gls{lp} is the foundation of maybe the prominent solving techniques for \glspl{opt-prb} \autocite{schrijver-1998-mip}. -A linear program describes a problem using \constraints{} in the form of linear equations over continuous \variables{}. +Mathematical programming \solvers{} are the most prominent solving technique employed in \gls{or} \autocite{schrijver-1998-mip}. +At its foundation lies \gls{lp}. +A linear program describes a problem using \constraints{} in the form of linear (in-)equations over continuous \variables{}. 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{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} + & x_{j} \in \mathbb{R} & \forall_{1 \leq{} j \leq{} V} \end{align*} -\noindent{}where \(V\) and \(C\) represent the number of variables and number of \constraints{} respectively. +\noindent{}where \(V\) and \(C\) represent the number of \variables{} and number of \constraints{} respectively. The vector \(c\) holds the coefficients of the objective function and the matrix \(a\) holds the coefficients for the \constraints{}. The vectors \(l\) and \(u\) respectively contain the lower and upper bounds of the \constraints{}. -Finally, the \variables{} of the linear program held in the \(x\) vector. +Finally, the \variables{} of the linear program are 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}. -One such method, the simplex method, was first conceived by \textcite{dantzig-1982-simplex} during the second world war. +One such method, the simplex method, was first conceived by \textcite{dantzig-1955-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. +Methods for solving linear programs 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{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). +If we require that one or more take a integer value (\(x_{i} \in \mathbb{Z}\)), then the problem becomes \gls{np} hard. +The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all} \variables{} must take a integer value). 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}. -Otherwise, we pick one of the integer \variables{} that does not yet have a discrete value. -For this \variable{} we create two versions of the linear program: a version where this \variable{} is less or equal to the value in the \gls{sol} rounded down to the nearest discrete value; and a version where it is greater or equal to the value in the \gls{sol} rounded up. +If the \variables{} happen to take integer values in the \gls{sol}, then we have found an \gls{opt-sol} to the mixed integer program. +Otherwise, we pick one of the \variables{} that needs to be integer but whose value in the \gls{sol} of the linear program is not. +For this \variable{} we create two versions of the linear program: a version where this \variable{} is constrained to be less or equal to the value in the \gls{sol} rounded down to the nearest integer value; and a version where it is constrained to be greater or equal to the value in the \gls{sol} rounded up. Both versions are solved to find the best \gls{sol}. -The process is repeated recursively until a discrete \gls{sol} is found. +The process is repeated recursively until a integer \gls{sol} is found. 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 is strictly worse than the incumbent. +Similarly, any integer \gls{sol} found in an earlier branch of the search process provides a lower bound. +When the upper bound given by the linear program is lower that the lower bound from an earlier solution, then we know that any integer \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}, solve many complex problems. +Modern \solvers{}, such as \gls{cbc} \autocite{forrest-2020-cbc}, \gls{cplex} \autocite{ibm-2020-cplex}, \gls{gurobi} \autocite{gurobi-2021-gurobi}, and \gls{scip} \autocite{gamrath-2020-scip}, are routinely used to solve very large industrial optimisation 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. +To solve an \instance{} of a \cmodel{}, it can be rewritten into 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{}. +Many \minizinc{} models contain \constraint{} that are not linear (in-)equations. +The translation of a single such \constraint{} can introduce many linear \constraints{} and \glspl{avar}. 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. +The indicator variables \(y_{i}\) are \gls{avar} that for a \variable{} \(x\) take the value 1 if \(x = i\) and 0 otherwise. \Constraints{} reasoning about the value of \(x\) are then rewritten as linear \constraints{} using the \variables{} \(y_{i}\). \begin{example} @@ -760,7 +773,7 @@ The indicator variables \(y_{i}\) are \glspl{ivar} that for a \variable{} \(x\) \label{line:back-mip-diag2} & \sum_{i,j \in N: i - j =k} y_{ij} \leq 1 & \forall_{-n+2 \leq{} k \leq{} n-2} \end{align} - The encoding of this \cmodel{} uses only integers. + As we can see, this \cmodel{} only uses integer \variables{} and linear \constraints{}. Like the \minizinc{} model, \variables{} \(q\) are used to represent where the queen is located in each column. To encode the \mzninline{all_different} \constraints{}, the indicator variables \(y\) are inserted to reason about the value of \(q\). The \cref{line:back-mip-channel} is used to connect the \(q\) and \(y\) \variables{} and make sure that their values correspond. @@ -775,9 +788,9 @@ The indicator variables \(y_{i}\) are \glspl{ivar} that for a \variable{} \(x\) \glsreset{maxsat} The study of the \gls{sat} problem is 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 DPLL algorithm that is still the basis for modern \gls{sat} solving stems from the 1960s \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 is a restriction of the general \gls{dec-prb} where all \variables{} have a Boolean type. +This problem is a restriction of the general \gls{dec-prb} where all \variables{} have a Boolean type and all \constraints{} are simple Boolean formulas. 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}. @@ -786,7 +799,7 @@ 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 \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, much progress has been made towards solving even the biggest the most complex \gls{sat} problems. +Even though the problem is proven to be hard to solve, much progress has been made towards solving even very 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} , solve instances of the problem with thousands of \variables{} and clauses. Many real world problems modelled using \cmls{} directly correspond to \gls{sat}. @@ -811,7 +824,7 @@ Depending on the problem, using a \gls{sat} \solvers{} to solve the encoded prob The encoding of the problem uses a Boolean \variable{} for every position of the chessboard. 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-row,line:back-sat-col} ensure that only one queens is placed in each row and column respectively. \Cref{line:back-sat-diag1,line:back-sat-diag2} similarly constrain each diagonal to contain only one queen. \end{example} @@ -821,23 +834,23 @@ Instead, clauses are given individual weights. The higher the weight, the more important the clause is for the overall problem. The goal in the \gls{maxsat} problem is then to find an \gls{assignment} for Boolean \variables{} that maximises the cumulative weights of the \gls{satisfied} clauses. -The \gls{maxsat} problem is analogous to a \gls{opt-prb}. -Like a \gls{opt-prb}, the aim of \gls{maxsat} is to find the \gls{opt-sol} to the problem. +The \gls{maxsat} problem is analogous to an \gls{opt-prb}. +Like an \gls{opt-prb}, the aim of \gls{maxsat} is to find the \gls{opt-sol} to the problem. The difference is that the weights are given to the \constraints{} instead of the \variables{} or a function over them. -It is, again, possible to encode a \cmodel{} with an \gls{objective} as a \gls{maxsat} problem. +It is, again, possible to rewrite a \cmodel{} with an \gls{objective} as a \gls{maxsat} problem. 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. +This Boolean \variable{} then forms a singleton clause with the result value as its weight. -For many problems the use of \gls{maxsat} \solvers{} offers a very successful method to find the \gls{opt-sol} to a problem. +For many problems the use of \gls{maxsat} \solvers{} offers a very successful method to find an \gls{opt-sol} to a problem. -\section{Other Constraint Modelling Languages}% +\section{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 may be adapted to these languages. +Each \cml{} has its own focus and purpose and comes with its own strengths and weaknesses. +Most of the techniques that are discussed in this thesis may be adapted to these languages. -We now discuss some other prominent \cmls{} and compare them to \minizinc{} to indicate to the reader where techniques will need to be adjusted to fit other languages. +We now discuss some prominent \cmls{} and compare them to \minizinc{} to indicate to the reader where our techniques will need 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. @@ -852,13 +865,12 @@ 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 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} - Let us consider modelling in \gls{ampl} by considering the well-known \gls{tsp}. + Let us consider modelling in \gls{ampl} using the well-known \gls{tsp}. In the \gls{tsp}, we are given a list of cities and the distances between all cities. The goal of the problem is to find a shortest path that visits all the cities exactly once and returns to its origin. A possible \cmodel{} for this problem in \gls{ampl} is shown in \cref{lst:back-ampl-tsp}. @@ -870,42 +882,44 @@ Different types of \solvers{} can also have access to different types of \constr \Lrefrange{line:back:ampl:parstart}{line:back:ampl:parend} declare the \parameters{} of the \cmodel{}. The \gls{ampl} model requires a set of names of cities, \texttt{Cities}, as input. - From these cities it declares a set \texttt{Paths} that contain all possible paths between the different cities. + From these cities it declares a set \texttt{Paths} that contains all possible paths between the different cities. Note how its definition uses a \gls{comprehension} to eliminate symmetric paths. - For each possible paths the model also requires its cost. + For each possible path the model also requires its cost. On \lref{line:back:ampl:var} we find the declaration for the \variables{} of the model. - For each possible path it decides whether the it is used, yes or no. + For each possible path it decides whether it is used or not. The \constraint{} on \lref{line:back:ampl:con1} ensures that for each city, one possible path to the city and one possible path from the city is taken. - Crucially, this does yet enforce that the taken variables represent a single path. - It is still possible for so-called subtours to exist, multiple unconnected path that together span all the cities. - A naive way to eliminate these subtours is by forcing that any subset of the set of cities has at least an incoming and an outgoing path. - \Lrefrange{line:back:ampl:compstart}{line:back:ampl:compend} of the model compute all possible subsets of cities. - These are then used by the \constraint{} on \lref{line:back:ampl:con2} to ensure they have the required paths going in and out. + Crucially, this does not yet enforce that the taken variables represent a single path. + It is still possible for so-called subtours to exist, multiple unconnected paths that together span all the cities. + \Lrefrange{line:back:ampl:compstart}{line:back:ampl:compend} introduce the classic Miller--Tucker--Zemlin method \autocite{miller-1960-subtour} to the model to eliminate these subtours. + For each city, this method introduces a variable that represent the order of the cities in the path. + The \constraint{} forces that if a path is taken from \texttt{i} to \texttt{j}, then \texttt{Order[i] < Order[j]}. + As such, each \texttt{Order} \variable{} must take a unique value and all cities are on the same path. + To remove symmetries in the model we set the \texttt{Order} \variable{} of the first city in the set to be one. Finally, \lref{line:back:ampl:goal} sets the goal of the \gls{ampl} model: to minimize the cost of all the paths taken. 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. + Like \minizinc{}, \gls{ampl} has an extensive expression language, which includes \gls{generator} expressions and a large collection of \glspl{operator}. + The building blocks of the model are also similar: \parameter{} declarations, \variable{} declarations, \constraints{}, and a solving goal. \begin{listing} \mznfile{assets/listing/back_tsp.mzn} \caption{\label{lst:back-mzn-tsp} An \minizinc{} model describing the \gls{tsp}} \end{listing} - A \minizinc{} model for the same problem is shown in \cref{lst:back-mzn-tsp} - - Even though the \gls{ampl} has a similar syntax to \minizinc{}, the models could not be more different. + A \minizinc{} model for the same problem is shown in \cref{lst:back-mzn-tsp}. + Even though \gls{ampl} has a similar syntax 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 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 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 (in-)equations. In \minizinc{} the modeller is not constrained in the same way. It can use the viewpoint of choosing, from each city, to which city to go next. A \mzninline{circuit} \gls{global} is then used to enforce that these decisions form a single path over all cities. + When targeting a \gls{mip} \solver{}, the \gls{decomp} of the \mzninline{circuit} \constraint{} will use a similar method to Miller--Tucker--Zemlin. In \minizinc{}, the modeller is always encouraged to create high-level \cmodels{}. \minizinc{} then rewrites these models into compatible \glspl{slv-mod}. @@ -915,19 +929,19 @@ Different types of \solvers{} can also have access to different types of \constr \label{sub:back-opl} \glsreset{opl} -\gls{opl} is a \cml{} that has a focus aims to combine the strengths of mathematical programming languages like \gls{ampl} with the strengths of \gls{cp} \autocite{van-hentenryck-1999-opl}. +\gls{opl} is a \cml{} that aims to combine the strengths of mathematical programming languages like \gls{ampl} with the strengths of \gls{cp} \autocite{van-hentenryck-1999-opl}. 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 is scheduled. +Where \gls{opl} really shines is when modelling scheduling problems. +Resources and activities are separate objects in \gls{opl}. +This allows users to express resource scheduling \constraints{} in an incremental and more natural fashion. +When solving a scheduling problem, \gls{opl} makes use of specialised interval \variables{}, which represent when a task is scheduled. \begin{example} - Let us consider modelling in \gls{opl}, by considering the well-known ``job shop problem''. + Let us consider modelling in \gls{opl} using the well-known ``job shop problem''. The job shop problem is similar to the open shop problem discussed in the introduction. - Like the open shop problem, we are tasked with scheduling jobs with multiple tasks. + Like the open shop problem, the goal is to schedule jobs with multiple tasks. Each task must be performed by an assigned machine. A machine can only perform one task at the same time. And, only one task of the same job can be scheduled at the same time. @@ -939,17 +953,17 @@ When solving a scheduling problem, the \gls{opl} makes use of specialised interv \caption{\label{lst:back-opl-jsp} An \gls{opl} model describing the job shop problem, abstracting from \parameter{} declarations.} \end{listing} - \Lref{line:back:opl:task} declares the \texttt{task} \variables{}, the main \variable{} of in model. - These \variables{} have the type \texttt{Activity}, a special type used to declare any scheduling event with a begin and end time. - \Variables{} of this type are influence by the \texttt{ScheduleHorizon} \parameter{} defined on \lref{line:back:opl:horizon} of the model. + \Lref{line:back:opl:task} declares the \texttt{task} \variables{}, the main \variables{} in model. + These \variables{} have the type \texttt{Activity}, a special type used to declare any scheduling event with a start and end time. + \Variables{} of this type are influenced by the \texttt{ScheduleHorizon} \parameter{} defined on \lref{line:back:opl:horizon} of the model. This \parameter{} restricts the time span in which all activities in the \cmodel{} must be scheduled. On \lref{line:back:opl:con2}, we enforce the order between the different tasks for the same job. - The \constraint{} uses the \texttt{precedes} operator to enforce one activity takes places before another. + The \constraint{} uses the \texttt{precedes} operator to enforce that one activity takes places before another. Another activity is declared on \lref{line:back:opl:makespan}. The \texttt{makespan} \variable{} represents the time spanned by all tasks. This is enforced by the \constraint{} on \lref{line:back:opl:con1}. - \Lref{line:back:opl:goal} set the minimisation of \texttt{makespan} to be the goal of the model. + \Lref{line:back:opl:goal} sets the minimisation of \texttt{makespan} to be the goal of the model. Resources are important notions in \gls{opl}. A resource can be any requirement of an activity. @@ -963,7 +977,7 @@ When solving a scheduling problem, the \gls{opl} makes use of specialised interv \caption{\label{lst:back-mzn-jsp} An \minizinc{} model describing the job shop problem, abstracting from \parameter{} declarations.} \end{listing} - A fragment of a \minizinc{} model modelling the same parts of job shop problem is shown in \cref{lst:back-mzn-jsp}. + A fragment of a \minizinc{} model, modelling the same parts of the job shop problem, is shown in \cref{lst:back-mzn-jsp}. Notably, \minizinc{} does not have explicit activity \variables{}. It instead uses integer \variables{} that represent the start times of the tasks and the time at which all tasks are finished. @@ -971,7 +985,7 @@ When solving a scheduling problem, the \gls{opl} makes use of specialised interv Where in the \gls{opl} model we could just state a global scheduling horizon, in \minizinc{} it has to be explicitly included in the \domains{} of the time \variables{}. And, instead of a \texttt{precedes} operator, we have to explicitly enforce the precedence of tasks using linear \constraints{}. - The \gls{opl} model also has the advantage of its resource syntax. + \Gls{opl} model also has the advantage of its resource syntax. It first states the resource objects and then merely has to use 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. @@ -979,8 +993,8 @@ When solving a scheduling problem, the \gls{opl} makes use of specialised interv \end{example} 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. +This syntax gives modellers full programmatic control over how the solver explores the search space depending on the current state of the variables. +This gives the 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: \begin{plain} @@ -989,19 +1003,24 @@ Take, for example, the following \gls{opl} search definition: } \end{plain} -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}. +This search strategy ensures that we first try to find a \gls{sol} where the \variable{} \mzninline{x} takes a value smaller than \mzninline{y}. +If it does not find a \gls{sol}, then it tries finding a \gls{sol} where the opposite is true. +This search specification, like many others imaginable, cannot be enforced using \minizinc{}'s \gls{search-heuristic} \glspl{annotation}. -To support \gls{opl}'s dedicated search language, the language is tightly integrated with its dedicated \solvers{}. +To support \gls{opl}'s dedicated search language, the language is tightly integrated with its supported \solvers{}. 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}. +It is therefore not always possible to connect other \solvers{} to \gls{opl}. + +While this advanced search language is an interesting construct, it is no longer available in the current version of \gls{opl} \autocite{ibm-2017-opl}. +Instead, \gls{opl} now offers the use of ``search phases'', which function similarly to \minizinc{}'s \gls{search-heuristic} \glspl{annotation}. + \subsection{Essence}% \label{sub:back-essence} \gls{essence} \autocite{frisch-2007-essence} is another high-level \cml{}. It is cherished for its adoption of high-level \variable{} types. -In addition to all variable types that are contained in \minizinc{}, \gls{essence} also contains: +In addition to all variable types that are supported by \minizinc{}, \gls{essence} also contains: \begin{itemize} \item Finite sets of non-integer types, @@ -1010,15 +1029,15 @@ 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 could, for example, define a \variable{} that is a sets of sets of integers. +Since sets, multi-sets, and functions can be defined on any other type, these types can be arbitrarily nested and the modeller could, for example, define a \variable{} that is a set of sets of integers. Partitions are defined for finite types: Booleans, enumerated types, or a restricted set of integers. \begin{example} - Let us consider modelling in \gls{essence} by considering the well-known ``social golfers problem''. - The social golfers problem considers a community of golfers that plans games of golf for a set number of weeks. + Let us consider modelling in \gls{essence} using the well-known ``social golfers problem''. + In the social golfers problem, a community of golfers plans games of golf for a set number of weeks. Every week all the golfers are split into groups of equal size and each group plays a game of golf. - The goals of the problem is find a way to split the groups different every week, such that no two golfers will meet each other twice. + The goal of the problem is to find a way to split the groups differently every week, such that no two golfers will meet each other twice. Two golfers can only be part of the same group once. A \cmodel{} for the social golfers problem in \gls{essence} can be seen in \cref{lst:back-essence-sgp}. @@ -1030,38 +1049,36 @@ Partitions are defined for finite types: Booleans, enumerated types, or a restri The \gls{essence} model starts with the preamble declaring the version of the language that is used. All the \parameters{} of the \cmodel{} are declared on line \lref{line:back:essence:pars}: \texttt{weeks} is the number of weeks to be considered, \texttt{groups} is the number of groups of golfers, and \texttt{size} is the size of each group. The input for the \parameters{} is checked to ensure that they take a value that is one or higher. - \Lref{line:back:essence:ntype} then uses the \parameters{} to declares a new type to represent the golfers. + \Lref{line:back:essence:ntype} then uses the \parameters{} to declare a new type to represent the golfers. - Most of the problem is modelled in the \variable{} declared on \lref{line:back:essence:var}. + Most of the problem is modelled on \lref{line:back:essence:var}. It declares a \variable{} that is a set of partitions of the golfers. The choice in \variable already contains some of the implied \constraints{}. Because the \variable{} reasons about partitions of the golfers, a correct \gls{assignment} is already guaranteed to correctly split the golfers into groups. The usage of a set of size \texttt{weeks} means that we directly reason about that number of partitions that have to be unique. - The type of the \variable{} does, however, not guarantee that the no two golfers will not meet each other twice. + The type of the \variable{} does, however, not guarantee that no two golfers will meet each other twice. Therefore, a \constraint{} that enforces this is found on \lref{line:back:essence:con}. Notably, the \texttt{together} function tests whether two elements are in the same part of a partition. - A \minizinc{} the same problem could be modelled can be found in \cref{lst:back-mzn-sgp}. - - The \minizinc{} model start similar to the essence model, in the declaration of the \parameters{} and a type for the golfers. + A \minizinc{} model for the same problem can be found in \cref{lst:back-mzn-sgp}. + It starts similarly to the \gls{essence} model, with the declaration of the \parameters{} and a type for the golfers. The differences start from the declaration of the \variables{}. - The \minizinc{} model is unable to use a set of partitions and instead uses a \gls{array} of sets. + The \minizinc{} model is unable to use a set of partitions and instead uses an \gls{array} of sets. Each set represents a single group in a single week. - 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. + Note that, through the \gls{essence} type system, the first two \constraints{} in the \minizinc{} model are implied in the \gls{essence} model. + This is an example where the use of high-level types helps the modeller create more concise models. Apart from syntax and the \variable{} viewpoint, the \constraint{} that enforces that golfers only occur in the same group once is identical. \begin{listing} \mznfile{assets/listing/back_sgp.mzn} - \caption{\label{lst:back-mzn-sgp} An \minizinc{} model describing the social golfers problem} + \caption{\label{lst:back-mzn-sgp} A \minizinc{} model describing the social golfers problem} \end{listing} \end{example} -\Gls{essence} allows the use of many high-level \variable{} and \constraints{} on these \variables{}. -Since these types of \variables{} are often not \gls{native} to the \solver{}. -\Gls{rewriting} will translate these types into \gls{native} \variables{} and \constraints{}. +\Gls{essence} allows the use of many high-level \variable{} types and \constraints{} on these \variables{}. +Since these types of \variables{} are often not \gls{native} to the \solver{}, \gls{rewriting} will translate these types into \gls{native} \variables{} and \constraints{}. However, along the way there can be many decisions about the representation used for the \solver{}. There are often multiple ways to represent a high-level \variable{}, or how to enforce its implicit \constraints{}. Unlike \minizinc{}, \Gls{essence} does not allow modellers or \solvers{} to influence this process directly. @@ -1071,7 +1088,7 @@ The process is internal to the \gls{essence} compiler. \label{sec:back-term} \glsreset{trs} -At the heart of the \gls{rewriting} process, to transform a \minizinc{} \instance{} into a \gls{slv-mod}, lies a \gls{trs}. +At the heart of the \gls{rewriting} process that transforms a \minizinc{} \instance{} into a \gls{slv-mod}, lies a \gls{trs}. A \gls{trs} describes a computational model. The full process can be described as the application of rules \(l \rightarrow r_{1}, \ldots, r_{n}\), that replace a \gls{term} \(l\) with one or more \glspl{term} \(r_{1}, \ldots, r_{n}\) \autocite{baader-1998-term-rewriting}. A \gls{term} is an expression with nested sub-expressions consisting of function and constant symbols. @@ -1080,7 +1097,7 @@ In a term rewriting rule, a term can also contain a term variable, which capture \begin{example} - Consider the following \gls{trs} consists of some (well-known) rules to rewrite logical and operations. + Consider the following \gls{trs}, which consists of some (well-known) rules to rewrite logical conjunctions. \begin{align*} (r_{1}):\hspace{5pt} & 0 \land x \rightarrow 0 \\ @@ -1098,19 +1115,21 @@ In a term rewriting rule, a term can also contain a term variable, which capture \end{example} Two properties of a \gls{trs} that are often studied are \gls{termination} and \gls{confluence}. -A \gls{trs} is said to be terminating if, no-matter what order the term rewriting rules are applied, you always arrive at a \gls{normal-form} (\ie, a set of \glspl{term} for which no more rules apply). +A \gls{trs} is said to be terminating if, no-matter what order the term rewriting rules are applied, you always arrive at a \gls{normal-form} (\ie{} a set of \glspl{term} for which no more rules apply). 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 is \(0\); otherwise, the result is \(1\). +The system, however, is confluent, since, if it terminates, it always 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 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. +These properties are also interesting in the translation process of a \minizinc{} instance into \flatzinc{}. +The \gls{confluence} of the \gls{rewriting} process would ensure that the same \gls{slv-mod} is produced independently of the order in which the \minizinc{} \instance{} is processed. +Although this is a desirable quality, it is not guaranteed since it conflicts with important simplifications, discussed in \cref{sec:back-mzn-interpreter}, used to improve the quality of \gls{slv-mod}. 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. +This means 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 is able to start). +While this property is interesting, it cannot be guaranteed for the \gls{rewriting} process in general. +Since \minizinc{} is a Turing complete language, it is possible to create a \minizinc{} model for which the \gls{rewriting} process will infinitely recurse. 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}. @@ -1119,10 +1138,10 @@ In the remainder of this section we discuss two types of \glspl{trs} that are cl \glsreset{clp} \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} +This subsection provides a brief introduction into the workings of 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{}. +A constraint logic program describes the process in which a \cmodel{} is eventually rewritten into a \gls{slv-mod} and solved by a \solver{}. 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}. @@ -1131,9 +1150,9 @@ Variables{} are another notable difference between \cmls{} and \gls{clp}. In \gls{clp}, like in a conventional \gls{trs}, a variable is merely a name. The symbol can 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{} 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. +This means that the solution of a constraint logic program can be a relation between different variables. +In cases where an instantiated solution is required, a special \mzninline{labeling} predicate is used to force a variable to take a constant value. +Similarly, there is a \mzninline{minimize} predicate 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. @@ -1143,11 +1162,11 @@ Even when a correct rewriting is found, it is possible to continue the process. 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 constraint store, and the evaluator of the constraint logic program. -In addition to just adding \constraints{}, the program also inspects the status of the \constraint{} and retracts \constraints{} from the constraint store. +In addition to just adding \constraints{}, the program also inspects the status of the constraint store 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 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. +The strength of the constraint store affects the correctness of a constraint logic program. +Some \solvers{} are incomplete; they are unable to tell if some of their \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{} is always able to decide if the \constraints{} are \gls{satisfied}. @@ -1159,7 +1178,7 @@ Once the variables have been assigned constant values, the \solver{} is always a 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} \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{}. +\gls{chr} are a language extension (targeted at \gls{clp}) to allow for the definition of user-defined \constraints{} within a \solver{}. \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. @@ -1179,7 +1198,7 @@ This means that, for some rules, multiple terms must match, to apply the rule. The rules follow the mathematical concepts of reflexivity, anti-symmetry, and transitivity. \begin{itemize} - \item The first rules states that if \texttt{X = Y}, then \texttt{X -> Y} is logically true. + \item The first rule states that if \texttt{X = Y}, then \texttt{X -> Y} is logically true. This rule removes the term \texttt{X -> Y}. Since the \constraint{} is said to be logically true, nothing gets added. \texttt{X = Y} functions as a guard. @@ -1214,18 +1233,18 @@ Since simpagation rules incorporate both the elements of simplification and prop Traditionally a \compiler{} is split into three sequential parts: the ``frontend'', the ``middle-end'', and the ``backend''. It is the job of the frontend to parse the user input, report on any errors or inconsistencies in the input, and transform it into an internal representation. The middle-end performs the main translation, independent of the compilation target. -It converts the internal representation at the level of the compiler frontend to another internal representation as close to the level required by the compilation targets. -The final transformation to the format required by the compilation target are performed by the backend. -When a \compiler{} is separated into these few steps, then adding support for new language or compilation target only require the addition of a frontend or backend respectively. +It converts the internal representation at the level of the compiler frontend to another internal representation as close as possible to the level required by the compilation targets. +The final transformations into the format required by the compilation target are performed by the backend. +When a \compiler{} is separated into these three steps, then adding support for a new language or compilation target only requires the addition of a frontend or backend respectively. -The \minizinc{} compilation process categorised in the same three categories, as shown in \cref{fig:back-mzn-comp}. +The \minizinc{} compilation process can be split into the same three parts, 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 instance is parsed into an \gls{ast}. 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 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. +This process is used to transform expressions into a common form for the middle-end, removing the ``syntactic sugar''. +For instance, this replaces the usage of enumerated types by normal integers. \begin{figure} \centering @@ -1234,54 +1253,59 @@ For instance, replacing the usage of enumerated types by normal integers. compiler.} \end{figure} -The middle-end contains the most important two processes: the rewriting and the optimisation. +The middle-end contains the most important two processes: \gls{rewriting} and optimisation. During the \gls{rewriting} process the \minizinc{} model is rewritten into a \gls{slv-mod}. -It could be noted that the rewriting step depends on the compilation target to define its \gls{native} \constraints{}. +It could be noted that the \gls{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{} 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 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. +The backend converts the internal \gls{slv-mod} into a format to be used by the targeted \solver{}. +Given the formatted artefact, a \solver{} process, controlled by the backend, is then started. +The \solver{} process produces \glspl{sol} for the \gls{slv-mod}. +Before these are given to the modeller, the backend reformulates these \glspl{sol} to become \glspl{sol} of the modeller's \instance{}. 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} -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{}. +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 calls, 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 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. +To arrive at a flat \gls{slv-mod}, the \gls{rewriting} process traverses the declarations, \constraints{}, and the solver goal and rewrites any expression contained in these items. +An expression is 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 \gls{array} \glspl{comprehension} and loops, have to be instantiated before their sub-expression is rewritten. +An exception to this bottom-up approach is the \gls{rewriting} of \glspl{comprehension}. +\glspl{comprehension} 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. + +An exception to this bottom-up approach is the \gls{rewriting} of \glspl{comprehension} \mzninline{[@\(E\)@ | @\(i\)@ in @\(S\)@ where @\(F\)@]}. +\Gls{rewriting} \(E\) requires instantiating the identifier \(i\) with the values from the set \(S\), and evaluating the condition \(W\). +The \compiler{} therefore iterates through all values in \(S\), binds the values to the specified identifier(s), and rewrites the condition \(F\). +If \(F\) is true, it rewrites the expression \(E\) and collects the result. 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. +The \gls{decomp} system in \minizinc{} is defined in terms of function declarations. 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 \gls{array} access, and if-then-else expressions, may also have to be decomposed for the target \solver{}. +Other expressions, like \gls{operator} expressions, variable \gls{array} access, and \gls{conditional} expressions, may also have to be decomposed for the target \solver{}. 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. +A notable effect of the \gls{rewriting} is that sub-expressions are replaced by literals or \glspl{avar}. 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. If, however, the expression contains a \variable{}, then this calculation cannot be performed during the \gls{rewriting} process. -Instead, a new \variable{} must be created to represent the value of the sub-expression, and it must be constrained to take the value corresponding to the expression. -The creation of this new \variable{} and defining \constraints{} happens in one of two ways: +Instead, an \gls{avar} must be created to represent the value of the sub-expression, and it must be constrained to take the value corresponding to the expression. +The creation of this \gls{avar} and defining \constraints{} happens in one of two ways: \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{} then adds the \gls{reif} of the \constraint{}. + \item For Boolean expressions in a non-\rootc{} context, the \gls{avar} is inserted by the \gls{rewriting} process itself. + To constrain this \gls{avar}, 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. @@ -1299,7 +1323,9 @@ The creation of this new \variable{} and defining \constraints{} happens in one constraint b \/ i1 \end{mzn} - \item For other expressions, the \variable{} and defining \constraints{} are introduced in the definition of the function itself. + \noindent{}Rewriting then continues with the \mzninline{this_call_reif} function (if its declaration has a body), as well as the disjunction operator. + + \item For non-Boolean expressions, the \gls{avar} and defining \constraints{} are introduced in the definition of the function itself. For example, the \mzninline{max} function in the standard library, which calculates the maximum of two values, is defined as follows. \begin{mzn} @@ -1310,23 +1336,22 @@ The creation of this new \variable{} and defining \constraints{} happens in one } in m; \end{mzn} - Using a \gls{let} it explicitly creates a new \variable{}, constrains this \variable{} to take to correct value, and returns the newly created \variable{}. + Using a \gls{let} the function body explicitly creates an \gls{avar}, constrains it to take to correct value, and then returns it. \end{itemize} -These are the basic steps that are followed to rewrite \minizinc{} instance. +These are the basic steps that are followed to rewrite \minizinc{} instances. This is, however, not the complete process. -The quality of the resulting \gls{slv-mod} is of the utmost importance. +Following these steps alone would result in poor quality \glspl{slv-mod}. A \gls{slv-mod} containing extra \variables{} and \constraints{} that do not add any information to the solving process can 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 discuss the most important techniques used to improve the \gls{rewriting} process. +In the remainder of this chapter, we discuss the most important techniques used to improve the \gls{rewriting} process. \subsection{Common Sub-expression Elimination}% \label{subsec:back-cse} \glsreset{cse} -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. +Since \minizinc{} is, at its core, a pure functional programming language, the evaluation of a \minizinc{} expression does not have any side effects. +As a consequence, evaluating the same expression twice will always reach an equivalent result. It is therefore possible to reuse the same result for equivalent expressions. This simplification is called \gls{cse}. @@ -1364,7 +1389,7 @@ Some expressions only become syntactically equal when instantiated, as in the fo Although the expressions \mzninline{pow(a, 2)} and \mzninline{pow(b, 2)} are not syntactically equal, the function call \mzninline{pythagoras(i,i)} using the same \variable{} for \mzninline{a} and \mzninline{b} makes them equivalent. \end{example} -To ensure that the same instantiation of a function are only evaluated once, the \minizinc{} \compiler{} uses memoisation. +To ensure that two identical instantiations of a function are only evaluated once, the \minizinc{} \compiler{} uses memoisation. After the \gls{rewriting} of an expression, the instantiated expression and its result are stored in a lookup table: the \gls{cse} table. Then before any consequent expression is rewritten the \gls{cse} table is consulted. If an equivalent expression is found, then the accompanying result is used; otherwise, the evaluation proceeds as normal. @@ -1373,11 +1398,11 @@ In our example, the evaluation of \mzninline{pythagoras(i, i)} would proceed as 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 detect that a reified \constraint{} is in fact not required. +\Glspl{reif} are often defined in the library in terms of complicated \glspl{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 of the solving process if we detect that a \gls{reified} \constraint{} is in fact not required. 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). +If the same \constraint{} is used in a non-\rootc{} context, \gls{cse} can then replace them with the constant \mzninline{true}, avoiding the need for \gls{reif} (or in fact any evaluation). 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. @@ -1397,7 +1422,7 @@ Finally, if the stored expression was in non-\rootc{} context and the current co If we process the \constraints{} in order we create a reified call to \mzninline{q(x)} for the original call. Suppose processing the second \constraint{} we discover \mzninline{t(x,y)} is \mzninline{true}, fixing \mzninline{b1}. - When we then process \mzninline{q(x)} in instantiation of the call \mzninline{p(x,y)}, we find it is the \rootc{} context. + When we then process \mzninline{q(x)} in instantiation of the call \mzninline{p(x,y)}, it is in the \rootc{} context. So \gls{cse} needs to set \mzninline{b0} to \mzninline{true}. \end{example} @@ -1411,7 +1436,7 @@ This is a simple form of \gls{propagation}, which, as discussed in \cref{subsec: 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 means that the \constraints{} does not need to be added at all and that constricting the \gls{domain} is enough. +Sometimes this means that the \constraint{} does not need to be added at all and that constricting the \gls{domain} is enough. 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 may need to decide on a representation of \variables{} based on their initial \domain{}. @@ -1427,22 +1452,23 @@ Finally, it can also be helpful for \solvers{} as they may need to decide on a r constraint (a > 5) -> (a + b > 12); \end{mzn} - Given the \domain{} specified in the model, the second \constraint is rewritten using a reified \constraints{} for each side of the implication. + Given the \domain{} specified in the model, the second \constraint{} is rewritten using \gls{reified} \constraints{}. + One for each side of the implication. 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{} is simplified to \mzninline{true}. \end{example} -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}). +During \gls{rewriting}, the \minizinc{} compiler actively removes values from the \domain{} when it encounters \constraints{} that trivially reduce it. +For example, it detects \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, does not perform more complex \gls{propagation}, like the \gls{propagation} of \glspl{global}. \subsection{Constraint Aggregation}% \label{subsec:back-aggregation} -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. +Complex \minizinc{} expressions sometimes result in the creation of many \gls{avar} to represent intermediate results. +This is in particular true for linear and Boolean equations that are generally written using \minizinc{} operators. \begin{example}% \label{ex:back-agg} @@ -1459,24 +1485,23 @@ This is in particular true for linear and boolean equations that are generally w constraint int_le(i2, z); \end{nzn} - This \flatzinc{} model is correct, but, at least for pure \gls{cp} solvers, the existence of the \glspl{ivar} is likely to have a negative impact on the \solver{}'s performance. + This \flatzinc{} model is correct, but, at least for pure \gls{cp} solvers, the existence of the \gls{avar} is likely to have a negative impact on the \solver{}'s performance. These \solvers{} would likely perform better had they directly received the equivalent linear \constraint{}: \begin{mzn} constraint int_lin_le([1,2,-1], [x,y,z], 0) \end{mzn} - This \constraint{} directly represents the initial \constraint{} in the \cmodel{} without the use of \glspl{ivar}. - Since many \solvers{} support linear \constraints{}, it is often an additional burden to have \glspl{ivar} that have to be given a value in the solution. + This \constraint{} directly represents the initial \constraint{} in the \cmodel{} without the use of \gls{avar}. \end{example} -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 are combined into linear \constraints{}, Boolean logic are combined into clauses, and counting \constraints{} are combined into global cardinality \constraints{}. +This can be resolved using \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 \gls{avar}. +For example, arithmetic expressions are combined into linear \constraints{}, Boolean logic expressions 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{} 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 \compiler{} instead performs a search of its sub-expressions to collect all other expressions to form an aggregated \constraint{}. The \gls{rewriting} process continues by \gls{rewriting} this aggregated \constraint{}. \subsection{Delayed Rewriting}% @@ -1500,7 +1525,7 @@ Adding \gls{propagation} during \gls{rewriting} means that the system becomes no \end{example} For \gls{mip} solvers, it is quite important to enforce tight bounds in order to improve efficiency and sometimes even numerical stability. -It would therefore be useful to rewrite the \mzninline{lq_zero_if_b} predicate only after the \domains{} of the involved \variables{} has been reduced as much as possible, in order to take advantage of the tightest possible bounds. +It would therefore be useful to rewrite the \mzninline{lq_zero_if_b} predicate only after the \domains{} of the involved \variables{} have been reduced as much as possible, in order to take advantage of the tightest possible bounds. On the other hand, evaluating a predicate may also impose new bounds on \variables{}, so it is not always clear which order of evaluation is best. The same problem occurs with \glspl{reif} that are produced during \gls{rewriting}. @@ -1518,25 +1543,32 @@ One delayed \constraint{} can still influence the \domains{} of \variables{} use Delaying the rewriting of \constraints{} also interferes with \gls{aggregation}. Since \gls{aggregation} is eagerly performed only when a \constraint{} is first encountered, it cannot aggregate any \constraints{} that follow from delayed values. -For example, if when aggregating Boolean clauses comes across an expression that needs to be reified, then a new Boolean \variable{} is created and the reified \constraint{} is delayed. -The problem is, however, that if the definition of this \gls{reif} turn out to be in terms of Boolean clauses as well, then this definition could have been aggregated as well. -Because the \compiler{} does not revisit \gls{aggregation}, this does not happen. +For example, when aggregating Boolean logic expressions, we can come across an expression that needs to be \gls{reified}. +A Boolean \gls{avar} is created and the reified \constraint{} is delayed. +Although the Boolean \gls{avar} can be used in the aggregated \constraints{}, we did not consider the body of the \gls{reif}. +If the body of the \gls{reif} was defined in terms of Boolean logic, then it would have been aggregated as well. +However, since the rewriting of the body was delayed and the \compiler{} does not revisit \gls{aggregation}, this does not happen. + +A possible solution to this problem, is for the modeller to activate \minizinc{}'s multi-pass compilation \autocite{leo-2015-multipass}. +When activate it compiles (and propagates) an \instance{} multiple times, remembering information about the earlier iteration. +As such, information normally discovered later in the \gls{rewriting} process, such as the final \domains{} of \variables and whether an expressions must be \gls{reified}, can be used from the start. \subsection{FlatZinc Optimisation}% \label{subsec:back-fzn-optimisation} -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{} may 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{}. +After the \compiler{} has finished \gls{rewriting} the \minizinc{} instance, it enters the optimisation phase. +This phase operates at the level of the \gls{slv-mod}, where all \constraints{} are now \gls{native} \constraints{} of the target \solver{}. +This means that, depending on the target \solver{}, the \compiler{} will not be able to understand the meaning of all \constraints{}. +It only understand the meaning of the standard \flatzinc{} \constraints{}, but not any of the \solver{} specific \gls{native} \constraints{}. +For the standard \flatzinc{} \constraints{}, \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} can fix the result of the \gls{reif} of a \constraint{}. -If this \constraint{} is not yet rewritten, then the \solver{} knows to use a direct \constraint{} instead of a reified version. +If the \gls{reif} was a \gls{native} \constraint, then the \solver{} can still use a direct \constraint{} instead of a \gls{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. -Since they both have to take the same value, only a single \variable{} is required in the \gls{slv-mod} to represent them both. -Whenever any (recognisable) equality \constraint{} is found during the optimisation phase, it is removed and one of the \variables{} is replaced by the other. +If the \compiler{} finds that two \variables{} \mzninline{x} and \mzninline{y} are equal, then only a single \variable{} is required in the \gls{slv-mod} to represent them both. +Whenever any equality \constraint{} is found during the optimisation phase, it is removed and one of the \variables{} is replaced by the other. Once initialised, it is generally not possible for \solvers{} to perform this replacement internally. diff --git a/chapters/2_background_preamble.tex b/chapters/2_background_preamble.tex index 66c1aa9..109c931 100644 --- a/chapters/2_background_preamble.tex +++ b/chapters/2_background_preamble.tex @@ -1,4 +1,4 @@ -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. +The research presented in this thesis investigates the process of \gls{rewriting} \cmls{}. This chapter provides the required background information to understand \cmls{}: \begin{itemize} @@ -15,8 +15,8 @@ Finally, the chapter analyses the existing approach to \gls{rewriting} \minizinc The overview of \cmls{} presented in this chapter supports the research and discussion presented in subsequent chapters. 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. +\Cref{sec:back-minizinc} summarises the syntax and functionality of \minizinc{}, the \cml{} used within this thesis. 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}. +Then, \cref{sec:back-term} surveys the closely related technologies in the field of \glspl{trs}. +Finally, \cref{sec:back-mzn-interpreter} explores the process that the existing \minizinc{} implementation uses to translate a \minizinc{} \instance{} into a \gls{slv-mod}. diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex index 1f81979..aa62f04 100644 --- a/chapters/3_rewriting.tex +++ b/chapters/3_rewriting.tex @@ -53,7 +53,7 @@ This section introduces the two sub-languages of \minizinc{} at the core of the \microzinc{} is a simple language used to define transformations to be performed by the \interpreter{}. It is simplified subset of \minizinc{}. The transformation are represented in the language through the use of function definitions. -A function of type \mzninline{var bool}, describing a relationship, can be defined as a \gls{native} \constraint{}. +A function of type \mzninline{var bool}, describing a relation, can be defined as a \gls{native} \constraint{}. Otherwise, a function body must be provided for \gls{rewriting}. The function body can use a restriction of the \minizinc{} expression language. @@ -72,7 +72,7 @@ The core of the syntax of \microzinc{} is defined in \cref{fig:rew-uzn-syntax}. In \microzinc{} it is specifically used to mark functions that are \gls{native} to the target \solver{}. We have omitted the definitions of \syntax{} and \syntax{}, which can be assumed to be the same as the definition of \syntax{} and \syntax{} in the \minizinc{} grammar, see \cref{ch:minizinc-grammar}. While we omit the typing rules here for space reasons, we will assume that in well-typed \microzinc{} programs conditions of expressions are \parameters{}. -This means that the where conditions \syntax{} in \glspl{comprehension}, the conditions \syntax{} in if-then-else expressions, and the \syntax{} index in \gls{array} accesses must have \mzninline{par} type. +This means that the where conditions \syntax{} in \glspl{comprehension}, the conditions \syntax{} in \gls{conditional} expressions, and the \syntax{} index in \gls{array} accesses must have \mzninline{par} type. In \minizinc{} the use of \variables{} in these positions is allowed and these expressions are rewritten to function calls. We will discuss how the same transformation takes place in when translating \minizinc{} to \microzinc{}. @@ -284,7 +284,7 @@ In order to track these dependencies, \nanozinc{} attaches \constraints{} that d A \nanozinc{} program (\cref{fig:rew-nzn-syntax}) consists of a topologically-ordered list of declarations of \variables{} and \constraints{}. \Variables{} are declared with an identifier, a domain, and are associated with a list of attached \constraints{}. \Constraints{} can also occur at the top-level of the \nanozinc{} program. -These are said to be the ``root-context'' \constraints{} of the \cmodel{}, \ie{} those that have to hold globally and are not just used to define an \gls{ivar}. +These are said to be the ``root-context'' \constraints{} of the \cmodel{}, \ie{} those that have to hold globally and are not just used to define an \gls{avar}. Only root-context \constraints{} can effectively constrain the overall problem. \Constraints{} attached to \variables{} originate from function calls, and since all functions are guaranteed to be total, attached \constraints{} can only define the function result. @@ -350,7 +350,7 @@ The rule evaluates the function body \(\ptinline{E}\) where the formal parameter The (CallBuiltin) rule applies to ``built-in'' functions that can be evaluated directly, such as arithmetic and Boolean operations on fixed values. The rule simply returns the result of evaluating the built-in function on the evaluated parameter values. -The (CallNative) rule applies to calls to \mzninline{var bool} functions, that describe relationships, that have been marked as \constraints{} \gls{native} to the \solver{}. +The (CallNative) rule applies to calls to \mzninline{var bool} functions, that describe relations, that have been marked as \constraints{} \gls{native} to the \solver{}. Since these are directly supported by the \solver{}, they simply need to be transferred into the \nanozinc{} program. \begin{figure*}[p] @@ -555,9 +555,9 @@ The \constraints{} directly succeeding the declaration prepended by \texttt{↳} \end{example} It is important to notice the difference between \constraints{} that appear at the top level and \constraints{} that appear as part of the attached \constraints{} of a \variable{}. -Top-level \constraints{} help define the problem, they are globally enforced and cannot be removed from the problem unless it can be proved that its relationships are already enforced. +Top-level \constraints{} help define the problem, they are globally enforced and cannot be removed from the problem unless it can be proved that its relations are already enforced. \Constraints{} attached to a \variable{}, on the other hand, are used to define a \variable{}. -\Constraints{} are generally attached when they stem from a functional relationship, like \mzninline{abs(x)} in the example, or from a \gls{reif}, like \mzninline{abs(x) > y} when used in the disjunction with \mzninline{c}. +\Constraints{} are generally attached when they stem from a functional relation, like \mzninline{abs(x)} in the example, or from a \gls{reif}, like \mzninline{abs(x) > y} when used in the disjunction with \mzninline{c}. In this thesis we will follow the same naming standard as \minizinc{}, where a \gls{reif} of a \constraint{} has the same name as the original \constraint{} with \texttt{\_reif} appended. \begin{example} @@ -752,12 +752,12 @@ This allows us to disable the \gls{cse} when it is guaranteed to be unnecessary. \label{subsec:rew-aggregation} In our new system it is still possible to support \gls{aggregation}. -We aggregate \constraints{} by combining \constraints{} connected through attached \constraints{}, eliminating the need for \glspl{ivar} to which they are attached. +We aggregate \constraints{} by combining \constraints{} connected through attached \constraints{}, eliminating the need for \gls{avar} to which they are attached. To aggregate a certain kind of \constraint{}, it is marked as a \gls{native} \constraint{}. These functional definitions are kept in the \nanozinc{} program until a top-level \constraint{} is posted that uses the \variables{} to which they are attached. Once this happens, the interpreter will employ dedicated \gls{aggregation} logic to visit the attached \constraints{} and combine them. The top-level \gls{constraint} is then replaced by the combined \gls{constraint}. -When the \glspl{ivar} become unused, they will be removed using the normal mechanisms. +When the \gls{avar} become unused, they will be removed using the normal mechanisms. \begin{example} For example, let us reconsider the linear \constraint{} from \cref{ex:back-agg}: \mzninline{x + 2*y <= z}. The constraint will result in the following \nanozinc{}. diff --git a/chapters/4_half_reif.tex b/chapters/4_half_reif.tex index 7c3cb1e..ad6fb02 100644 --- a/chapters/4_half_reif.tex +++ b/chapters/4_half_reif.tex @@ -728,7 +728,7 @@ In the case where a \variable{} has one incoming edge, but it is marked as used When using full \gls{reif}, all \glspl{reif} are stored in the \gls{cse} table. This ensure that if the same expression is \gls{reified} twice, then the resulting \gls{reif} will be reused. -This avoids that the solver has to enforce the same functional relationship twice. +This avoids that the solver has to enforce the same functional relation twice. If the \gls{rewriting} uses \gls{half-reif}, in addition to full \gls{reif}, then \gls{cse} needs to ensure not just that the expressions are equivalent, but also that the context of the two expressions are compatible. For example, if an expression was first found in a \posc{} context and later found in a \mixc{} context, then the resulting \gls{half-reif} from the first cannot be used for the second expression. diff --git a/chapters/6_conclusions.tex b/chapters/6_conclusions.tex index 98b1018..4be6b04 100644 --- a/chapters/6_conclusions.tex +++ b/chapters/6_conclusions.tex @@ -36,7 +36,7 @@ Crucially, the architecture is easily extended with well-known simplification te \item \Gls{cse} is used to detect any duplicate calls. We describe how it can be employed both during the compilation from \minizinc{} to \microzinc{}, and in the evaluation of \microzinc{}. - \item When it is beneficial, the architecture can utilize \gls{aggregation} to combine certain \constraints{} and eliminate \glspl{ivar}. + \item When it is beneficial, the architecture can utilize \gls{aggregation} to combine certain \constraints{} and eliminate \gls{avar}. \item Finally, \constraints{} can be marked for \gls{del-rew}. This implores to \microzinc{} \interpreter{} to delay the \gls{rewriting} of a certain call until all possible information is available. diff --git a/chapters/A2_benchmark.tex b/chapters/A2_benchmark.tex index 3910ce5..18a2cb5 100644 --- a/chapters/A2_benchmark.tex +++ b/chapters/A2_benchmark.tex @@ -141,7 +141,7 @@ In this thesis we use four different versions of the \gls{gecode} solver: \end{itemize} -\paragraph{IBM CPLEX} is a proprietary \gls{mip} \solver{} \autocite{cplex-2020-cplex}. +\paragraph{IBM CPLEX} is a proprietary \gls{mip} \solver{} \autocite{ibm-2020-cplex}. In this thesis we use \gls{cplex} version 20.1 under an academic license in our experiments. \paragraph{OpenWBO} is a open source \gls{maxsat} \solver{} \autocite{martins-2014-openwbo}.