diff --git a/assets/acronyms.tex b/assets/acronyms.tex index e8fac30..4300345 100644 --- a/assets/acronyms.tex +++ b/assets/acronyms.tex @@ -34,18 +34,27 @@ \newacronym{maxsat}{MaxSAT}{Maximum Satisfiability} +\newacronym{mix}{\textit{mix}}{mixed context} + \newacronym[see={[Glossary:]{gls-mip}}]{mip}{MIP\glsadd{gls-mip}}{Mixed Integer Programming} +\newacronym{neg}{\textit{neg}}{negative context} + \newacronym{np}{NP}{Nondeterministic Polynomial-time} \newacronym{or}{OR}{Operational Research} \newacronym[see={[Glossary:]{gls-opl}}]{opl}{OPL\glsadd{gls-opl}}{The Optimisation Programming Language} +\newacronym{pos}{\textit{pos}}{positive context} + \newacronym{ram}{RAM}{Random Access Memory} +\newacronym{root}{\textit{root}}{root context} + \newacronym[see={[Glossary:]{gls-sat}}]{sat}{SAT\glsadd{gls-sat}}{Boolean Satisfiability} \newacronym[see={[Glossary:]{gls-trs}}]{trs}{TRS\glsadd{gls-trs}}{Term Rewriting System} \newacronym{tsp}{TSP\glsadd{gls-trs}}{Travelling Salesperson Problem} + diff --git a/assets/bibliography/references.bib b/assets/bibliography/references.bib index 2a155ba..df257c7 100644 --- a/assets/bibliography/references.bib +++ b/assets/bibliography/references.bib @@ -265,6 +265,24 @@ year = 2020, } +@article{davis-1960-dpll, + author = {Davis, Martin and Putnam, Hilary}, + title = {A Computing Procedure for Quantification Theory}, + year = {1960}, + issue_date = {July 1960}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + volume = {7}, + number = {3}, + issn = {0004-5411}, + url = {https://doi.org/10.1145/321033.321034}, + doi = {10.1145/321033.321034}, + journal = {J. ACM}, + month = jul, + pages = {201–215}, + numpages = {15}, +} + @article{davis-1962-dpll, author = {Davis, Martin and Logemann, George and Loveland, Donald}, title = {A Machine Program for Theorem-Proving}, @@ -283,6 +301,25 @@ numpages = 4, } +@inproceedings{een-2003-minisat, + author = {Niklas E{\'{e}}n and Niklas S{\"{o}}rensson}, + editor = {Enrico Giunchiglia and Armando Tacchella}, + title = {An Extensible SAT-solver}, + booktitle = {Theory and Applications of Satisfiability Testing, 6th + International Conference, {SAT} 2003. Santa Margherita Ligure, + Italy, May 5-8, 2003 Selected Revised Papers}, + series = {Lecture Notes in Computer Science}, + volume = {2919}, + pages = {502--518}, + publisher = {Springer}, + year = {2003}, + url = {https://doi.org/10.1007/978-3-540-24605-3\_37}, + doi = {10.1007/978-3-540-24605-3\_37}, + timestamp = {Tue, 14 May 2019 10:00:41 +0200}, + biburl = {https://dblp.org/rec/conf/sat/EenS03.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org}, +} + @inproceedings{ek-2020-online, author = {Alexander Ek and Maria Garcia de la Banda and Andreas Schutt and Peter J. Stuckey and Guido Tack}, diff --git a/assets/glossary.tex b/assets/glossary.tex index 773029b..be4085d 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -45,12 +45,12 @@ \newglossaryentry{backtrack}{ name={backtrack}, - description={}, + description={A \gls{solver} is said to backtrack when it revisits a search decision (\eg{} an value assumed during search). Notably the action of backtracking generally involves invalidating all effects of the revisited and subsequent search decisions}, } \newglossaryentry{bnb}{ name={branch and bound}, - description={}, + description={A search method to find an \gls{opt-sol}. After an initial \gls{sol} is found, the search continuously looks for \glspl{sol} for which the \gls{objective} will return a better value than the incumbent \gls{sol}. If it is proven that no such \gls{sol} exists, then the final incumbent \gls{sol} is an \gls{opt-sol}}, } \newglossaryentry{byte-code}{ @@ -60,7 +60,7 @@ \newglossaryentry{bounds-con}{ name={bounds consistent}, - description={}, + description={A \gls{propagator} is bounds consistent when it reduces the minimum and maximum values of \domains{} for which there is no possible \gls{variable-assignment} such that the \gls{constraint} is satisfied}, } \newglossaryentry{gls-cbls}{ @@ -98,11 +98,6 @@ }, } -\newglossaryentry{constraint-store}{ - name={constraint store}, - description={}, -} - \newglossaryentry{cplex}{ name={CPLEX}, description={}, @@ -130,7 +125,7 @@ \newglossaryentry{confluence}{ name={confluence}, - description={}, + description={A property of a \gls{trs}. The system is said to be confluent if it always arrives at the same \gls{normal-form}}, } \newglossaryentry{gls-csp}{ @@ -191,7 +186,7 @@ \newglossaryentry{domain-con}{ name={domain consistent}, - description={}, + description={A \gls{propagator} is domain consistent if it is able to remove all values from \domains{} for which there is no possible \gls{variable-assignment} such that the \gls{constraint} is satisfied}, } \newglossaryentry{essence}{ @@ -260,9 +255,9 @@ description={}, } -\newglossaryentry{indicator-var}{ - name={indicator variable}, - description={}, +\newglossaryentry{half-reified}{ + name={half reified}, + description={See \gls{half-reif}}, } \newglossaryentry{ivar}{ @@ -290,11 +285,24 @@ }, } +\newglossaryentry{kleene-sem}{ + name={Kleene semantic}, + description={ + A semantic model for treating undefined behaviour in \glspl{cml}. + Under Kleene semantics an occurrence of undefined behaviour will only cause its surrounding expression to be undefined when its value is required to compute its result + }, +} + \newglossaryentry{knapsack}{ name={knapsack problem}, description={}, } +\newglossaryentry{linearisation}{ + name={linearisation}, + description={The process of \gls{rewriting} a \gls{model} to a mixed integer program}, +} + \newglossaryentry{let}{ name={let expression}, description={}, @@ -397,7 +405,7 @@ \newglossaryentry{optional}{ name={optional}, - description={}, + 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.}, } \newglossaryentry{opt-sol}{ @@ -434,6 +442,14 @@ }, } +\newglossaryentry{strict-sem}{ + name={strict semantic}, + description={ + A semantic model for treating undefined behaviour in \glspl{cml}. + Under strict semantics any occurrence of undefined behaviour will cause the result of the \gls{instance} to be undefined + }, +} + \newglossaryentry{parameter}{ name={problem parameter}, description={ @@ -473,6 +489,19 @@ description={A reification is a special form of a \gls{constraint} where, instead of the \gls{constraint} being enforced in the \glspl{sol}, it enforces that a \gls{cvar} represents whether the \gls{constraint} holds or not}, } +\newglossaryentry{reified}{ + name={reified}, + description={See \gls{reification}}, +} + +\newglossaryentry{rel-sem}{ + name={relational semantic}, + description={ + A semantic model for treating undefined behaviour in \glspl{cml}. + Under relational semantics an occurrence of undefined behaviour will cause its closest surrounding Boolean expression to be \mzninline{false} + }, +} + \newglossaryentry{rewriting}{ name={rewriting}, description={ @@ -504,27 +533,22 @@ \newglossaryentry{term}{ name={term}, - description={}, + description={An expression in a \gls{trs}. A term can have nested sub-expressions}, } \newglossaryentry{termination}{ name={termination}, - description={}, + description={A property of a \gls{trs}. A system is terminating if it is guaranteed to eventually arrive at a \gls{normal-form}}, } \newglossaryentry{trail}{ name={trail}, - description={}, + description={A chronological account of changes to data structures with as goal to possibly reverse these changes. The usage of a trail is a common way for \gls{solver} to revisit search decisions (\ie{} \gls{backtrack})}, } \newglossaryentry{gls-trs}{ name={term rewriting system}, - description={}, -} - -\newglossaryentry{unification}{ - name={unification}, - description={}, + description={A computational model that expresses computation through the application of rewriting rules. A rewriting rule replaces the \glspl{term} on its left hand side with the \glspl{term} on its right hand side}, } \newglossaryentry{unsat}{ diff --git a/assets/mzn/minilns/basic.mzn b/assets/mzn/minilns/basic.mzn index 1447120..0486de7 100644 --- a/assets/mzn/minilns/basic.mzn +++ b/assets/mzn/minilns/basic.mzn @@ -1,2 +1,2 @@ predicate basic_LNS() = - (status() != START) -> nbh(X); + (status() != START) -> nbh(X); diff --git a/assets/shorthands.tex b/assets/shorthands.tex index af639f3..719c316 100644 --- a/assets/shorthands.tex +++ b/assets/shorthands.tex @@ -28,6 +28,8 @@ \newcommand*{\nanozinc}{\gls{nanozinc}\xspace{}} \newcommand*{\parameters}{\glspl{parameter}\xspace{}} \newcommand*{\parameter}{\gls{parameter}\xspace{}} +\newcommand*{\reified}{\gls{reified}\xspace{}} +\newcommand*{\halfreified}{\gls{half-reified}\xspace{}} \newcommand*{\solvers}{\glspl{solver}\xspace{}} \newcommand*{\solver}{\gls{solver}\xspace{}} \newcommand*{\variable}{\gls{variable}\xspace{}} @@ -46,10 +48,10 @@ \newcommand*{\Cbind}{\ensuremath{\wedge}} % Context syntax (half-reification) -\newcommand*{\rootc}{\textit{root}} -\newcommand*{\posc}{\textit{pos}} -\newcommand*{\negc}{\textit{neg}} -\newcommand*{\mixc}{\textit{mix}} +\newcommand*{\rootc}{\gls{root}} +\newcommand*{\posc}{\gls{pos}} +\newcommand*{\negc}{\gls{neg}} +\newcommand*{\mixc}{\gls{mix}} \newcommand*{\mayberootc}{\textit{root?}} \newcommand*{\changepos}{\ensuremath{+}} \newcommand*{\changeneg}{\ensuremath{-}} diff --git a/chapters/2_background.tex b/chapters/2_background.tex index 11a9f9d..d8fc529 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -4,8 +4,6 @@ \input{chapters/2_background_preamble} -\jip{TODO:\ Mention something about LCG.} - \section{Introduction to Constraint Modelling Languages} \label{sec:back-intro} @@ -16,24 +14,29 @@ And, early imperative programming languages, like FORTRAN, were the first to off Consequently, in current times, writing a computer program requires little knowledge of how the targeted computer system operates. Freuder 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 \autocite*{freuder-1997-holygrail}. -In \cmls{}, different from imperative (and even other declarative) languages, the modeller does not describe how to solve the problem, but rather provides the problem requirements; therefore, it could be said that a \cmodel{} actually describes the solution to the problem. +In \cmls{}, different from imperative (and even other declarative) languages, the modeller does not describe how to solve the problem, but rather provides the problem requirements; therefore, it could be said that a \cmodel{} actually describes the \gls{sol} to the problem. -In a \cmodel{}, instead of specifying the manner in which we can find the solution, we give a concise description of the problem. +In a \cmodel{}, instead of specifying the manner in which we can find the \gls{sol}, we give a concise description of the problem. The elements of a \cmodel include \parameters{}, what we already know; \variables{}, what we wish to know; and \constraints{}, the relationships that should exist between them. +Through the variation of \parameters{}, a \cmodel{} can describe a full class of problems. +A specific problem is captured by a \instance{}, the combination of a \cmodel{} with a complete \gls{parameter-assignment} (\ie{}, a mapping from all parameters to values). -This type of combinatorial problem is typically called a \gls{csp}. -The goal of a \gls{csp} is to find values for the \variables{} that satisfy the \constraints{} or prove that no such assignment exists. -Many \cmls\ also support the modelling of \gls{cop}, where a \gls{csp} is augmented with a \gls{objective} \(z\). -In this case the goal is to find a solution that satisfies all \constraints{} while minimising (or maximising) \(z\). +The type of combinatorial problems described by \cmodels{} are called \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{}. +Or, when this is not possible, prove that no such \gls{assignment} exists. +Many \cmls{} also support the modelling of \gls{opt-prb}, where a \gls{dec-prb} is augmented with an \gls{objective}. +In this case the goal is to find a \gls{sol} that satisfies all \constraints{} while minimising (or maximising) the value of the \gls{objective}. + +Although a \cmodel{} does not contain any instructions on how to find a suitable \gls{sol}, \instances{} of \cmodels{} can generally be given to a dedicated \solver{}. +The \solver{} will use a dedicated algorithm that finds a \gls{sol} that fits the requirements of the \instance{}. -Although a constraint model does not contain any instructions on how to find a suitable solution, these models can generally be given to a dedicated solving program, or \solver{} for short, that can find a solution that fits the requirements of the model. \begin{example}% - \label{ex:back-knapsack} +\label{ex:back-knapsack} - Let us consider the following scenario: Packing for a weekend trip, I have to decide which toys to bring for my dog, Audrey. + 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 gets enjoys playing with some toys more than others, we can now try and pick the toys that bring Audrey the most amount of joy, but still fit in the car. - The following set of equations describe this knapsack problem as a \gls{cop}: + Since Audrey enjoys playing with some toys more than others, we can now try and pick the toys that bring Audrey the most amount of joy, but still fit in the car. + The following set of equations describe this knapsack problem as an \gls{opt-prb}: \begin{equation*} \text{maximise}~z~\text{subject to}~ @@ -44,36 +47,30 @@ Although a constraint model does not contain any instructions on how to find a s \end{cases} \end{equation*} - In these equations \(S\) is set \variable{}. - It contains the selection of toys that will be packed for the trip. - \(z\) is the objective \variable{} that is maximised to find the optimal selections of toys to pack. - The \parameter{} \(T\) is the set of all the toys. + In these equations \(S\) is a set \variable{}. + It represents the selection of toys that will be packed for the trip. + The \gls{objective} is evaluates the quality of the \gls{sol} through the \variable{} \(z\). + And, \(z\) is bound to the amount of joy that the selection of toys will bring. + This is to be maximised. + The \parameter{} \(T\) is the set of all available toys. The \(joy\) and \(space\) functions are \parameters{} used to map toys, \( t \in T\), to a value depicting the amount of enjoyment and space required respectively. - Finally, the \parameter{} \(C\) is that depicts the total space that is left in the car before packing the toys. - - This constraint model gives an abstract mathematical definition of the \gls{cop} that would be easy to adjust to changes in the requirements. - To solve instances of this problem, however, these instances have to be transformed 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 a definition that can be used by dedicated solvers. + Finally, the \parameter{} \(C\) depicts the total space that is left in the car before packing the toys. + This \cmodel{} gives an abstract mathematical definition of the \gls{opt-prb} that would be easy to adjust to changes in the requirements. + To solve \instances{} of this problem, however, these \instances{} have to be rewritten into input accepted by a \solver{}. + \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/py/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} - -In the remainder of this chapter we will first, in \cref{sec:back-minizinc} we introduce \minizinc\ as the leading \cml\ used within this thesis. -In \cref{sec:back-solving} we discuss how \gls{cp} can be used to solve a constraint model. -We also briefly discuss other solving techniques and the problem format these techniques expect. -\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 solver-level constraint model. +% \begin{listing} +% \pyfile{assets/py/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} \minizinc{} is a high-level, solver- and data-independent modelling language for discrete satisfiability and optimisation problems \autocite{nethercote-2007-minizinc}. -Its expressive language and extensive library of constraints allow users to easily model complex problems. +Its expressive language and extensive library of \glspl{global} allow users to easily model complex problems. \begin{listing} \mznfile{assets/mzn/back_knapsack.mzn} @@ -84,130 +81,183 @@ Its expressive language and extensive library of constraints allow users to easi \label{ex:back-mzn-knapsack} 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}. + A \minizinc{} model encoding this problem is shown in \cref{lst:back-mzn-knapsack}. The model starts with the declaration of the \parameters{}. \Lref{line:back:knap:toys} declares an enumerated type that represents all possible toys, \(T\) in the mathematical model in the example. - \Lrefrange{line:back:knap:joy}{line:back:knap:space} declare arrays mapping from toys to integer values, these represent the functional mappings \(joy\) and \(space\). + \Lrefrange{line:back:knap:joy}{line:back:knap:space} declare arrays that map toys to integer values. + These represent the functional mappings \(joy\) and \(space\). Finally, \lref{line:back:knap:left} declares an integer \parameter{} to represent the car capacity as an equivalent to \(C\). 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. - \(S\) in our earlier model. + 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. - Finally, the model contains a constraint, on \lref{line:back:knap:con}, to ensure we do not exceed the given capacity and states the goal for the solver: to maximise the value of the \variable{} \mzninline{total_joy}. + 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} One might note that, although more textual and explicit, the \minizinc\ model definition is very similar to our earlier mathematical definition. -Given ground assignments to input \parameters{}, a \minizinc\ model is translated (via a process called \emph{flattening}) into a set of \variables{} and primitive constraints. +A \minizinc{} model cannot be solved solved directly. +It first need to be transformed into a \gls{slv-mod}: a list of \variables{} and \constraints{} \gls{native} to the \solver{}. +Type of \variables{} and \constraints{} are said to be \gls{native} to the \solver{} when they are directly supported as input to the \solver{}. -Given the assignments +Given complete \gls{parameter-assignment}, a \minizinc{} model can form a \minizinc{} instance. +The process to transform a \minizinc{} instance into a \gls{slv-mod} is a called \gls{rewriting}. +This \gls{slv-mod} created by \minizinc{} are generally in the form of \flatzinc{}. +\flatzinc{} can be seen as a strict subset of \minizinc{} specifically chosen to represent \glspl{slv-mod}. +It is the primary way in which \minizinc{} communicates with \solvers{}. -\begin{mzn} - TOYS = {football, tennisball, stuffed_elephant}; - toy_joy = [63, 12, 100]; - toy_space = [32, 8, 40]; - space_left = 44; -\end{mzn} +\begin{example} -the following model is the result of flattening: + For example, given the \minizinc{} model in \cref{lst:back-mzn-knapsack} and the \gls{assignment} -\begin{mzn} - var 0..1: selection_0; - var 0..1: selection_1; - var 0..1: selection_2; - var 0..175: total_joy:: is_defined_var; - constraint int_lin_le([32,8,40], [selection_0,selection_1,selection_2], 44); - constraint int_lin_eq( + \begin{mzn} + TOYS = {football, tennisball, stuffed_elephant}; + toy_joy = [63, 12, 100]; + toy_space = [32, 8, 40]; + space_left = 44; + \end{mzn} + + \noindent{}the following \flatzinc{} \gls{slv-mod} might be the result of \gls{rewriting}: + + \begin{mzn} + var 0..1: selection_0; + var 0..1: selection_1; + var 0..1: selection_2; + var 0..175: total_joy:: is_defined_var; + constraint int_lin_le([32,8,40], [selection_0,selection_1,selection_2], 44); + constraint int_lin_eq( [63,12,100,-1], [selection_0,selection_1,selection_2,total_joy], 0 - ):: defines_var(total_joy); - solve maximize total_joy; -\end{mzn} + ):: defines_var(total_joy); + solve maximize total_joy; + \end{mzn} -This \emph{flat} problem will be passed to some \solver{}, which will attempt to determine an assignment to each \variable{} \mzninline{solection_i} and \mzninline{total_joy} that satisfies all constraints and maximises \mzninline{total_joy}, or report that there is no such assignment. + This \emph{flat} problem will be passed to some \solver{}. + The \solver{} will attempt to determine an \gls{assignment} to each \variable{} \mzninline{solection_i} and \mzninline{total_joy} that satisfies all constraints and maximises \mzninline{total_joy}. + If this is not possible, then it will report that there is no such \gls{assignment}. + +\end{example} \subsection{Model Structure}% \label{subsec:back-mzn-structure} -As we have seen in \cref{ex:back-mzn-knapsack}, a \minizinc\ model generally contains value declarations, both for \variables{} and input \parameters{}, \constraints{}, and a solving goal. +The structure of a \minizinc{} model can generally be described directly in terms of a \cmodel{}: + +\begin{itemize} + \item \variables{} and \parameters{} are found in the form of value declarations, + \item \constraints{} are explicitly defined using their own keyword, + \item and the \gls{objective} is included as a solving goal. +\end{itemize} + More complex models might also include definitions for custom types, user defined functions, and a custom output format. -In \minizinc\ these items are not constrained to occur in any particular order. +These items are not constrained to occur in any particular order. We will briefly discuss the most important model items. -For a detailed overview of the structure of \minizinc\ models you can consult the full syntactic structure of \minizinc\ 2.5.5 in \cref{ch:minizinc-grammar}. -Nethercote et al.\ and Marriott et al.\ offer a detailed discussion of the \minizinc\ and \zinc\ language, its predecessor, respectively \autocite*{nethercote-2007-minizinc,marriott-2008-zinc}. +Note that these items will 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}. +Nethercote et al.\ and Marriott et al.\ offer a detailed discussion of the \minizinc{} and \zinc{} language, its predecessor, respectively \autocite*{nethercote-2007-minizinc,marriott-2008-zinc}. -Values in \minizinc\ are declared in the form \mzninline{@\(T\)@: @\(I\)@;} or \mzninline{@\(T\)@: @\(I\)@ = @\(E\)@;}. -\(T\) is the type of the declared value, \(I\) is a new identifier used to reference the declared value, and, optionally, the modeller can functionally define the value using an expression \(E\). +\paragraph{Declaration Items} Values in \minizinc{} are declared in the form \mzninline{@\(T\)@: @\(I\)@ = @\(E\)@}, where: +\begin{itemize} + \item \(T\) is the type 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 can be omitted when a \variable{} has no functional definition, or when a \parameter{} is assigned externally. The identifier used in a top-level value definition must be unique. -Two declarations with the same identifier will result in an error during the flattening process. +Two declarations with the same identifier will 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 main types used in \minizinc{} are Boolean, integer, floating point numbers, sets of integers, and (user-defined) enumerated types. +The declaration of \parameters{} and \variables{} are distinguishes through their type. +The type of a \variable{} is preceded by the \mzninline{var} keyword. +The type of a \parameter{} can similarly be marked by the \mzninline{par} keyword, but this is not required. These types can be used both as normal \parameters{} and as \variables{}. -To better structure models, \minizinc\ allows collections of these types to be contained in arrays. -Unlike other languages, arrays can have a user defined index set, which can start at any value, but has to be a continuous range. -For example, an array going from 5 to 10 of new boolean \variables{} might be declared as +To better structure models, \minizinc{} allows collections of these types to be contained in \glspl{array}. +Unlike other languages, \glspl{array} can have a user defined index set, which can start at any value, but has to be a continuous range. +For example, an array going from 5 to 10 of new Boolean \variables{} might be declared as \begin{mzn} array[5..10] of var bool: bs; \end{mzn} The type in a declaration can, however, be more complex when the modeller uses a type expression. -These expressions constrain a declaration, not just to a certain type, but also to a set of value. +These constrain a declaration, not just to a certain type, but also to a set of values. This set of values is generally referred to as the \gls{domain} of a \variable{}. -In \minizinc\ any expression that has a set type can be used as a type expression. -For example, the following two declarations declare two integer \variables{} that can take the values from three to five and one, three, and five respectively. +In \minizinc{} any expression that has a set type can be used as a type expression. +For example, the following two declarations declare two integer \variables{}. +The first can take the values from three to five and the second can take the values one, three, and five. \begin{mzn} var 3..5: x; var {1,3,5}: y; \end{mzn} -If the declaration includes an expression to functionally define the value, then the identifier can be used as a name for this expression. -If, however, the type of the declaration is given as a type expression, then this places an implicit \constraint{} on the expression, forcing the result of the expression to take a value according to the type expression. +If a declaration does include a functional definition, then the identifier can be seen as 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. -\constraint{} items, \mzninline{constraint @\(E\)@;} contain the top-level constraint of the \minizinc\ model. -A constraint item contains only a single expression \(E\) of Boolean type. -During the flattening of the model the expressions in constraints are translated into solver level versions of the same expression. -It is important that the solver-level versions of the expressions are equisatisfiable, meaning they are only satisfied if-and-only-if the original expression would have been satisfied. +\paragraph{Constraint Items} \Constraints{} in a \minizinc{} model are specified using the syntax: \mzninline{constraint @\(E\)@}. +A \constraint{} item contains only a single expression \(E\) of Boolean type. +During the \gls{rewriting} of the model the expressions in \constraints{} are translated into versions of the same expression that are \gls{native} to the \solver{}. +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}. -A \minizinc\ model can contain a single goal item. -This item can signal the solver to do one of three actions: to find an assignment to the \variables{} that satisfies the constraints, \mzninline{solve satisfy;}, to find an assignment to the \variables{} that satisfies the constraints and minimises the value of a \variable{}, \mzninline{solve minimize x;}, or similarly maximises the value of a \variable{}, \mzninline{solve maximize x;}. +\paragraph{Solving Goal Item} A \minizinc{} model can contain a single solving goal item. +This item can signal the solver to do one of three actions: + +\begin{itemize} + \item \mzninline{solve satisfy} --- to find an assignment to the \variables{} that satisfies the constraints, + \item \mzninline{solve minimize @\(E\)@} --- to find an 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} + +\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. -\jip{TODO:\@ add some information about search in \minizinc{}. -It's probably pretty relevant.} +\paragraph{Function Items} Common structures in \minizinc\ can be captured using function declarations. +Functions are declared using the syntax \mzninline{function @\(T\)@: @\(I\)@(@\(P\)@) = E}, where: +\begin{itemize} + \item \(T\) is the type of its result; + \item \(I\) is its identifier; + \item \(P\) is a list types and identifiers for its arguments; + \item and \(E\) is the body of the function, an expression that can use the arguments \(P\). +\end{itemize} -Common structures in \minizinc\ can be captured using function declarations. -A user can declare a function \mzninline{function @\(T\)@: @\(I\)@(@\(P\)@) = E;}. -In the function declaration \(T\) is the type of the result of the function, \(I\) is the identifier for the function, \(P\) is a list types and identifiers for the parameters of the functions, and finally \(E\) is the expression that can use the parameters \(P\) and when flattened will give the result of the function. -The \minizinc\ language offers the keywords \mzninline{predicate} and \mzninline{test} as a shorthand for \mzninline{function var bool} and \mzninline{function bool} respectively. -For example a function that squares an integer can be defined as follows. +\noindent{}During \gls{rewriting}, a call to the function is replaced by its body instantiated the arguments given in the call. +The \minizinc{} language allows users to write the keywords \mzninline{predicate} as a shorthand \mzninline{function var bool} and \mzninline{test} as a shorthand for \mzninline{function bool}. + +As an example, we can define a function that squares an integer can be defined as follows. \begin{mzn} function int: square(int: a) = a * a; \end{mzn} -Function declarations are also the main way in which \solver{} libraries are defined. -During flattening all \minizinc\ expressions are (eventually) rewritten to function calls. -A solver can then provide its own implementation for these functions. -It is assumed that the implementation of the functions in the \solver{} libraries will ultimately be rewritten into fully relational call. -When a relational constraint is directly supported by a solver the function should be declared within an expression body. -Any call to such a function is directly placed in the flattened model. +During \gls{rewriting} all \minizinc{} expressions are (eventually) transformed into function calls. +As such, the usage of function declarations is the primary method for \solvers{} to specify how to rewrite a \minizinc{} model into a \gls{slv-mod}. +The collection of functions declarations to rewrite for a \solver{} is generally referred to as a \solver{} library. +In this library, functions might be declared without a function body. +This marks them as \gls{native} to the solver. +Calls to these functions can be directly placed in the \gls{slv-mod}. +For non-\gls{native} functions, a \solver can provide a function body that rewrites calls into (or towards) \gls{native} functions. +\solver{} implementers are, however, not forced to provide a definition for all functions in \minizinc{}'s extensive library. +Instead, they can rely on a set of standard declaration, known as the standard library, that rewrite functions into a minimal subset of \gls{native} functions, known as the \flatzinc built-ins. \subsection{MiniZinc Expressions}% \label{subsec:back-mzn-expr} -One of the powers of the \minizinc\ language is the extensive expression language that it offers to help modellers create models that are intuitive to read, but are transformed to fit the structure best suited to the chosen \solver{}. -We will now briefly discuss the most important \minizinc\ expressions and the general methods employed when flattening them. -A detailed overview of the full syntactic structure of the \minizinc\ expressions in \minizinc\ 2.5.5 can be found in \cref{sec:mzn-grammar-expressions}. +One of the powers of the \minizinc{} language is the extensive expression language. +It can help modellers create \cmodels{} that are intuitive to read, but are transformed to fit the structure best suited to the chosen \solver{}. +We will now briefly discuss the most important type of expression in \minizinc{} and the general methods employed when \gls{rewriting} them. -\Glspl{global} are the basic building blocks in the \minizinc\ language. +\paragraph{Global Constraints} It could be said that the basic building blocks of the \minizinc{} language are \Glspl{global}. These expressions capture common (complex) relations between \variables{}. -\Glspl{global} in the \minizinc\ language are used as function calls. +\Glspl{global} in the \minizinc{} language are used as function calls. An example of a \gls{global} is \begin{mzn} @@ -220,40 +270,50 @@ An example of a \gls{global} is ); \end{mzn} -This \gls{global} expresses the knapsack relationship, where the \parameters{} \mzninline{w} are the weights of the items, \mzninline{p} are the profit for each item, the \variables{} in \mzninline{x} represent the amount of time the items are present in the knapsack, and \mzninline{W} and \mzninline{P}, respectively, represent the weight and profit of the knapsack. +This \gls{global} expresses the knapsack relationship, where the argument: +\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 and \mzninline{W} and \mzninline{P}, respectively, represent the weight and profit of the knapsack +\end{itemize} -Note that the usage of this \gls{global} might have simplified the \minizinc\ model in \cref{ex:back-mzn-knapsack}: +Note that the usage of this \gls{global} might have simplified the \minizinc{} model in \cref{ex:back-mzn-knapsack}: \begin{mzn} constraint knapsack(toy_space, toy_joy, set2bool(selection), total_joy, space); \end{mzn} -The usage of this \gls{global} has the additional benefit that the knapsack structure of the problem is then known to the \solver{} which might implement special handling of the relationship. +\noindent{}This would have the additional benefit that the knapsack structure of the problem is then known to the \solver{}. +It might then use special handling for this relationship. -Although \minizinc\ contains an extensive library of \glspl{global}, many problems contain constraints that aren't covered by a \gls{global}. -There are many other expression forms in \minizinc\ that can help modellers express a constraint. +Although \minizinc{} contains an extensive library of \glspl{global}, many problems contain structures that are not covered by a \gls{global}. +There are many other types of expressions in \minizinc{} that can help modellers express complex \constraints{}. -\Gls{operator} symbols in \minizinc\ are used as a shorthand for \minizinc\ functions that can be used to transform or combine other expressions. +\paragraph{Operators} When we express a mathematical formula, we generally do this through the use of \gls{operator} symbols. +\minizinc{} includes \glspl{operator} for many mathematical, logic, and set operations. For example the constraint \begin{mzn} constraint not (a + b < c); \end{mzn} -contains the infix \glspl{operator} \mzninline{+} and \mzninline{<}, and the prefix \gls{operator} \mzninline{not}. +\noindent{}contains the infix \glspl{operator} \mzninline{+} and \mzninline{<}, and the prefix \gls{operator} \mzninline{not}. -These \glspl{operator} will be evaluated using the addition, less-than comparison, and Boolean negation functions respectively. -Although the \gls{operator} syntax for \variables{} and \parameters{} is the same, different (overloaded) versions of these functions will be used during flattening. -For \parameters{} types the result of the function can be directly computed, but when flattening these functions with \variables{} types a new \variable{} for its result must be introduced and a constraint enforcing the functional relationship. +\Gls{operator} symbols in \minizinc{} are a shorthand for \minizinc{} functions. +The \glspl{operator} in the above expression will be evaluated using the addition, less-than comparison, and Boolean negation functions respectively. +Although the \gls{operator} syntax for \variables{} and \parameters{} is the same, different (overloaded) versions of these functions will be used during \gls{rewriting}. +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. -The choice between different expressions can often be expressed using a \gls{conditional} expression, sometimes better known as an ``if-then-else'' expressions. +\paragraph{Conditional Expression} The choice between different expressions can often be expressed using a \gls{conditional} expression, also known as an ``if-then-else'' expressions. You could, for example, force that the absolute value of \mzninline{a} is bigger than \mzninline{b} using the constraint \begin{mzn} constraint if a >= 0 then a > b else b < a endif; \end{mzn} -In \minizinc\ the result of a \gls{conditional} expression is, however, not contained to Boolean types. +The result of a \gls{conditional} expression is not contained to Boolean types. The condition in the expression, the ``if'', must be of a Boolean type, but as long as the different sides of the \gls{conditional} expression are the same type it is a valid conditional expression. This can be used to, for example, define an absolute value function for integer \parameter{}: @@ -262,28 +322,29 @@ This can be used to, for example, define an absolute value function for integer if a >= 0 then a else -a endif; \end{mzn} -When the condition does not contain any \variables{}, then the flattening of a \gls{conditional} expression will result in one of the side of the expressions. -If, however, the condition does contain a \variable{}, then the result of the condition cannot be defined during the flattening. -Instead, the expression will introduce a new \variable{} for the result of the expression and a constraint to enforce the functional relationship. -In \minizinc\ special \mzninline{if_then_else} \glspl{global} are available to implement this relationship. +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. -For the selection of an element from an \gls{array}, instead of between different expressions, the \minizinc\ language uses an \gls{array} access syntax similar to most other languages. +\paragraph{Array access} For the selection of an element from an \gls{array} the \minizinc{} language uses an \gls{array} access syntax similar to most other computer languages. The expression \mzninline{a[i]} selects the element with index \mzninline{i} from the array \mzninline{a}. -Note this is not necessarily the \(\mzninline{i}^{\text{th}}\) element because \minizinc\ allows modellers to provide a custom index set. +Note this is not necessarily the \(\mzninline{i}^{\text{th}}\) element because \minizinc{} allows modellers to provide a custom index set. -Like the previous expressions, the selector \mzninline{i} can be both a \parameter{} or a \variable{}. -If the expression is a \gls{variable}, then the expression is flattened to be an \mzninline{element} function. -Otherwise, the flattening will replace the \gls{array} access expression by the element referenced by expression. +The selection of an element from an \gls{array} is in many way similar to the choice in a \gls{conditional} expression. +Like a \gls{conditional} expression, the selector \mzninline{i} can be both a \parameter{} or a \variable{}. +If the expression is a \gls{variable}, then the expression is rewritten to an \gls{ivar} and an \mzninline{element} \constraint{}. +Otherwise, the \gls{rewriting} will replace the \gls{array} access expression by the chosen element of the \gls{array}. -\Gls{array} \glspl{comprehension} are expressions can be used to compose \gls{array} objects. -This allows modellers to create \glspl{array} that are not given directly as input to the model or are a declared collection of \variables{}. +\paragraph{Comprehensions} \Gls{array} \glspl{comprehension} are expressions can be used to compose \gls{array} objects. +The generation of new \gls{array} structures allows modellers adjust, combine, filter, or order values from within the \minizinc{} model. -\Gls{generator} expressions, \mzninline{[E | G where F]}, consist of three parts: +\Gls{generator} expressions, \mzninline{[@\(E\)@ | @\(G\)@ where @\(F\)@]}, consist of three parts: \begin{description} - \item[\mzninline{G}] The generator expression which assigns the values of collections to identifiers, - \item[\mzninline{F}] an optional filtering condition, which has to evaluate to \mzninline{true} for the iteration to be included in the array, - \item[\mzninline{E}] and the expression that is evaluation for each iteration when the filtering condition succeeds. + \item[\(G\)] The generator expression which assigns the values of collections to identifiers, + \item[\(F\)] an optional filtering condition, which has to evaluate to \mzninline{true} for the iteration to be included in the array, + \item[\(E\)] and the expression that is evaluation for each iteration when the filtering condition succeeds. \end{description} The following example composes an \gls{array} that contains the tripled even values of an \gls{array} \mzninline{x}. @@ -292,26 +353,27 @@ The following example composes an \gls{array} that contains the tripled even val [ xi * 3 | xi in x where x mod 2 == 0] \end{mzn} -The evaluated expression will be added to the new array. -This means that the type of the array will primarily depend on the type of the expression. -However, in recent versions of \minizinc\ both the collections over which we iterate and the filtering condition could have a \variable{} type. -Since we then cannot decide during flattening if an element is present in the array, the elements will be made of a \gls{optional} type. -This means that the solver still will decide if the element is present in the array or if it takes a special ``absent'' value (\mzninline{<>}). +During \gls{rewriting}, the instantiation of the expression with current generator values will be added to the new \gls{array}. +This means that the type of the \gls{array} will primarily depend on the type of the expression. +However, in recent versions of \minizinc{} both the collections over which we iterate and the filtering condition could have a \variable{} type. +Since we then cannot decide during \gls{rewriting} if an element is present in the array, the elements will be made of an \gls{optional} type. +This means that the \solver{} still will decide if the element is present in the array or if it takes a special ``absent'' value (\mzninline{<>}). -Finally, \glspl{let} are the primary scoping mechanism in the \minizinc\ language, together with function definitions. -A \gls{let} allows a modeller to provide a list of definitions, flattened in order, that can be used in its resulting definition. +\paragraph{Let Expressions} Together with function definitions, \glspl{let} are the primary scoping mechanism in the \minizinc{} language. +A \gls{let} allows a modeller to provide a list of declarations, that can only be used in its resulting expression. +Additionally, a \gls{let} can contain \constraints{} to constrain the declared values. There are three main purposes for \glspl{let}: \begin{enumerate} \item To name an intermediate expression, so it can be used multiple times or to simplify the expression. - For example, the constraint + For example, the \constraint{} \begin{mzn} constraint let { var int: tmp = x div 2; } in tmp mod 2 == 0 \/ tmp = 1; \end{mzn} - constrains that half of \mzninline{x} is even or one. + \noindent{}constrains that half of \mzninline{x} is even or takes the value one. \item To introduce a scoped \variable{}. For example, the constraint @@ -319,7 +381,7 @@ There are three main purposes for \glspl{let}: constraint let {var -2..2: slack;} in x + slack = y; \end{mzn} - constrains that \mzninline{x} and \mzninline{y} are at most two apart. + \noindent{}constrains that \mzninline{x} and \mzninline{y} are at most two apart. \item To constrain the resulting expression. For example, the following function @@ -332,21 +394,30 @@ There are three main purposes for \glspl{let}: } in z; \end{mzn} - returns a new \variable{} \mzninline{z} that is constrained to be the multiplication of \mzninline{x} and \mzninline{y} by the relational multiplication constraint \mzninline{pred_int_times}. + \noindent{}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}. \end{enumerate} -An important detail in flattening \glspl{let} is that any \variables{} that are introduced might need to be renamed in the resulting solver level model. -Different from top-level definitions, the \variables{} declared in \glspl{let} can be flattened multiple times when used in loops, function definitions (that are called multiple times), and \gls{array} \glspl{comprehension}. -In these cases the flattener must assign any \variables{} in the \gls{let} a new name and use this name in any subsequent definitions and in the resulting expression. +An important detail in \gls{rewriting} \glspl{let} is that any \variables{} that are introduced might need to be renamed in the resulting \gls{slv-mod}. +Different \variables{} declared directly in declaration items, the \variables{} declared in \glspl{let} can be flattened multiple times when used in loops, function definitions (that are called multiple times), and \gls{array} \glspl{comprehension}. +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{}. +It does this through the use of \glspl{annotation}. +Any item or expression can be annotated. +An annotation is indicated by the \mzninline{::} \gls{operator} followed by an identifier or function call. +The same syntax can be repeated to place multiple \glspl{annotation} on the same item or expression. + +A common use of \glspl{annotation} in \minizinc{} is to provide a search heuristic. +Through the use of an \gls{annotation} on the solving goal item, the modeller can express an order in which they think values should be tried for the \variables{} in the model. \subsection{Reification}% \label{subsec:back-reification} -With the rich expression language in \minizinc{}, \constraints{} can consist of complex expressions that do not translate to a single constraint at the \solver{} level. -Instead, different parts of a complex expression will be translated into different \constraints{}. +With the rich expression language in \minizinc{}, \constraints{} can consist of complex expressions that do result in a single \constraint{} in the \gls{slv-mod}. +Instead, different parts of a complex expression will be rewritten into different \constraints{}. Not all of these \constraints{} will be globally enforced by the solver. -\constraints{} stemming for sub-expressions will typically be \emph{reified} into a Boolean variable. -\Gls{reification} means that a variable \mzninline{b} is constrained to be true if and only if a corresponding constraint \mzninline{c(...)} holds. +\constraints{} stemming for sub-expressions will typically be \reified{} into a Boolean variable. +The \gls{reification} of a \constraint{} \(c\) creates an \gls{ivar} \mzninline{b} constrained to be the truth-value of this \constraint{}: \(\texttt{b} \leftrightarrow{} c\). \begin{example} Consider the \minizinc\ model: @@ -363,15 +434,17 @@ Not all of these \constraints{} will be globally enforced by the solver. Instead, the solver is tasked to maximise the number of reified variables it can set to \mzninline{true}. \end{example} -When an expression occurs in a position where it can be globally enforced, we say it occurs in \emph{root context}. -Contrarily, an expression that occurs in a \emph{non-root context} will be reified during the flattening process. -In \minizinc{}, almost all expressions can be used in both contexts. +When an expression occurs in a position where it can be globally enforced, we say it occurs in \rootc{}. +Contrarily, an expression that occurs in non-\rootc{} will be reified during the \gls{rewriting} process. +In \minizinc{}, almost all expressions can be used in both \rootc{} and non-\rootc{} contexts. \subsection{Handling Undefined Expressions}% \label{subsec:back-mzn-partial} -Some expressions in the \cmls\ do not always have a well-defined result. -Part of the semantics of a \cmls{} is the choice as to how to treat these partial functions. +In this section we will discuss the handling of partial expressions in \cmls{} as studied by Frisch and Stuckey \autocite*{frisch-2009-undefinedness}. + +Some expressions in \cmls{} do not have well-defined results. +Part of the semantics of a \cml{} is the choice as to how to treat these partial functions. \begin{example}\label{ex:back-undef} Consider, for example, the following ``complex constraint'' @@ -380,10 +453,10 @@ Part of the semantics of a \cmls{} is the choice as to how to treat these partia constraint i <= 4 -> a[i] * x >= 6; \end{mzn} - which requires that if \mzninline{i} takes a value less or equal to four, then the value in the \texttt{i}\(^{th}\) position of array \mzninline{a} multiplied by \mzninline{x} must be at least 6. + \noindent{}which requires that if \mzninline{i} takes a value less or equal to four, then the value in the \texttt{i}\(^{th}\) position of array \mzninline{a} multiplied by \mzninline{x} must be at least 6. Suppose the array \texttt{a} has index set \mzninline{1..5}, but \texttt{i} takes the value \texttt{7}. - The constraint \mzninline{element(i, a, t1)} will fail and no solution will be found. + The expression \mzninline{a[i]} will fail and no \gls{sol} will be found. However, intuitively if \mzninline{i = 7} the constraint should be trivially true. \end{example} @@ -411,32 +484,32 @@ Other examples of \minizinc{} expressions that result in partial functions are: \end{itemize} The existence of undefined expressions can cause confusion in \cmls{}. -There is both the question of what happens when an undefined expression is evaluated and at what point during the process undefined values will be resolved, during flattening or at solving time. +There is both the question of what happens when an undefined expression is evaluated and at what point during the process undefined values will be resolved, during \gls{rewriting} or by the \solver{}. -Frisch and Stuckey define three semantic models to deal with the undefinedness in \cmls\ \autocite*{frisch-2009-undefinedness}: +Frisch and Stuckey define three semantic models to deal with the undefinedness in \cmls: \begin{description} - \item[Strict] \cmls\ employing a ``strict'' undefinedness semantic do not allow any undefined behaviour during the evaluation of the constraint model. - If during the flattening or solving process an expression is found to be undefined, then any expressions in which it is used is also marked as undefined. - In the end, this means that the occurrence of a single undefined expression will mark the full model as undefined. + \item[Strict] \Cmls{} employing a \gls{strict-sem} do not allow any undefined behaviour during the evaluation of the \cmodel{}. + If during the \gls{rewriting} or solving process an expression is found to be undefined, then any expressions in which it is used is also marked as undefined. + Consequently, this means that the occurrence of a single undefined expression will cause the full \instance{} to be undefined. - \item[Kleene] The ``Kleene'' semantic treat undefined expressions as expressions for which not enough information is available. - This if an expression contains undefined sub-expression, it will only be marked as undefined if the value of the sub-expression is required to compute its result. - Take for example the expression \mzninline{false -> E}. - Here, when \mzninline{E} is undefined the result of the expression can still be said to be \mzninline{true}, since the value of \mzninline{E} does not influence the result of the expression. - However, if we take the expression \mzninline{true /\ E}, then when \mzninline{E} is undefined the overall expression is also undefined since the value of the expression cannot be determined. + \item[Kleene] The \gls{kleene-sem} treats undefined expressions as expressions for which not enough information is available. + If an expression contains undefined sub-expression, then it will only be marked as undefined if the value of the sub-expression is required to compute its result. + Take for example the expression \mzninline{false -> @\(E\)@}. + When \(E\) is undefined the result of the expression can still be said to be \mzninline{true}, since the value of \(E\) does not influence the result of the expression. + 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 ``relational'' semantic follows from the fact that all expressions in \cmls\ will eventually become part of a relational constraint. + \item[Relational] The \gls{rel-sem} follows from all expressions in a \cml{} eventually becoming part of a relational \constraint{}. So even though a (functional) expression in itself might not have a well-defined result, we can still decide whether its surrounding relationship holds. - For example, the expression \mzninline{x div 0} is undefined, but the relationship \mzninline{int_div(x,0,y)} can be said to be \mzninline{false}. + For example, the expression \mzninline{x div 0} is undefined, but the relationship \mzninline{int_div(x, 0, y)} can be said to be \mzninline{false}. It can be said that the relational semantic will make the closest relational expression that contains an undefined expression \mzninline{false}. \end{description} In practice, it is often natural to guard against undefined behaviour using Boolean logic. -Relational semantics therefore often feel the most natural for the users of constraint modelling languages. -This is why the \minizinc\ uses relational semantics during its evaluation. +\Glspl{rel-sem} therefore often feel the most natural for the users of constraint modelling languages. +This is why the \minizinc{} uses \glspl{rel-sem} during its evaluation. For example, one might deal with a zero divisor using a disjunction: @@ -445,38 +518,40 @@ For example, one might deal with a zero divisor using a disjunction: \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 ``relational'' semantics. +This corresponds to \glspl{rel-sem}. -Frisch and Stuckey also show that different \solvers{} often employ different semantics \autocite*{frisch-2009-undefinedness}. -It is therefore important that, during the flattening process, any potentially undefined expression gets replaced by an equivalent model that is still valid under a strict semantic. -Essentially eliminating the existence of undefined expressions in the \solver{} model. +Frisch and Stuckey 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}. \section{Solving Constraint Models}% \label{sec:back-solving} -There are many prominent techniques to solve a \constraint{} model, but none of them will solve a \minizinc\ model directly. -Instead, a \minizinc\ model get translated into \variables{} and \constraints{} of the type that the solver supports directly. +There are many prominent techniques to solve a \constraint{} model, but none of them will solve a \minizinc{} instance directly. +Instead, a \minizinc{} instance is rewritten into a \gls{slv-mod} containing only \constraints{} and types of \variables{} that are \gls{native} to the \solver{}. \minizinc{} was initially designed as an input language for \gls{cp} \solvers{}. -These \glspl{solver} often support many of the high-level \constraints{} that are written in a \minizinc\ model. -For \gls{cp} solvers the amount of translation required can vary a lot. -It depends on which \constraints{} the targeted \gls{cp} \solver{} are directly supported and which \constraints{} have to be decomposed. +These \glspl{solver} often directly support many of the \glspl{global} in a \minizinc{} model. +For \gls{cp} solvers the amount of \gls{rewriting} required can vary a lot. +It depends on which \constraints{} are \gls{native} to the targeted \gls{cp} \solver{} and which \constraints{} have to be decomposed. -Because \gls{cp} \solvers{} work on a similar level as the \minizinc\ language, some techniques used in \gls{cp} \solvers{} can also be used during the transformation from \minizinc\ to \flatzinc{}. -The usage of these techniques can often help shrink the \glspl{domain} of \variables{} and eliminate or simplify \constraint{}. -\Cref{subsec:back-cp} explains the general method employed by \gls{cp} \solvers{} to solve a \constraint{} model. +In some ways \gls{cp} \solvers{} work on a similar level as the \minizinc{} language. +Therefore, some techniques used in \gls{cp} \solvers{} can also be used during the \gls{rewriting} process. +The usage of these techniques can shrink the \domains{} of \variables{} and eliminate or simplify \constraint{}. +\Cref{subsec:back-cp} explains the general method employed by \gls{cp} \solvers{} to solve a \cmodel{}. -Throughout the years \minizinc\ has seen the addition of solvers using other approaches to finding solutions to \constraint{} models. -Although these \solvers{} bring new classes of problems that can be solved using \minizinc{}, they also bring new challenges in to efficiently encode the problem for these \solvers{}. -To understand these challenges in the translations a \minizinc\ model into a solver level \constraint{} model, the remainder of this section will discuss the other dominant technologies used by \minizinc\ \solver{} targets and their input language. +Throughout the years \minizinc{} has started targeting \solvers{} using different approaches. +Although these \solvers{} allow new classes of problems that to be solved using \minizinc{}, they also bring new challenges to the \gls{rewriting} process. +To understand these \gls{rewriting} challenges, the remainder of this section will discuss the other dominant technologies used by \minizinc{} \solver{} and their \glspl{slv-mod}. \subsection{Constraint Programming}% \label{subsec:back-cp} \glsreset{cp} -When given a \gls{csp}, one might wonder what the best way is to find a solution to the problem. -The simplest solution would be to apply ``brute force'': try every value in the \gls{domain} of all \variables{}. -It will not surprise the reader that this is an inefficient approach. + +When given an \instance{} of a \cmodel{}, one might 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{}. +This is an inefficient approach. Given, for example, the constraint \begin{mzn} @@ -484,77 +559,80 @@ Given, for example, the constraint \end{mzn} It is clear that when the value \mzninline{a} is known, then the value of \mzninline{b} can be deduced. +Therefore, only that one value for \mzninline{b} has to be tried. \gls{cp} is the idea of solving \glspl{csp} by performing an intelligent search by inferring which values are still feasible for each \variable{} \autocite{rossi-2006-cp}. -To find a solution to a given \gls{csp}, a \gls{cp} \solver{} will perform a depth first search. -At each node, the \solver{} will try to eliminate any impossible value using a process called \gls{propagation} \autocite{schulte-2008-propagation}. -For each \constraint{} the \solver{} has a chosen algorithm called a \gls{propagator}. -Triggered by changes in the \glspl{domain} of its \variables{}, the \gls{propagator} will analyse and prune any values that are proven to be inconsistent. +A \gls{cp} \solver{} will perform a depth first search. +Using a mechanism called \gls{propagation} the \solver{} removes values from \domains{} that are no longer possible. +\Gls{propagation} works through the use of \glspl{propagator}: algorithms dedicated to a specific \constraint{} that prune \domains{} when its contains values that are proven to be inconsistent. +This mechanism can be very efficient because a \gls{propagator} only has to be run again if the \domains{} of one of its \variables{} has changed. -In the best case scenario, \gls{propagation} will eliminate all impossible values and all \variables{} have been fixed to a single value. -In this case we have arrived at a solution. +In the best case scenario, \gls{propagation} will eliminate all impossible values and all \variables{} have been \gls{fixed} to a single value. +In this case we have arrived at a \gls{sol}. Often, \gls{propagation} alone will not be enough to find a \gls{sol} and we reach a \gls{fixpoint}, where no more \glspl{propagator} are triggered. The \solver{} then has to make a search decision. It will fix a \variable{} to a value or add a new \constraint{}. -This search decision is an assumption made by the \solver{} in the hope of finding a solution. -If no solution 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. +This search decision is an assumption made by the \solver{} in the hope of finding a \gls{sol}. +If no \gls{sol} is found using the search decision, then it needs to try making the opposite decision which requires the exclusion of the chosen value or adding the opposite \constraint{}. Note that there is an important difference between values excluded by \gls{propagation} and making search decisions. Values excluded by propagation are guaranteed to not occur in any \gls{sol} -Wereas, values excluded by a search heuristic are merely removed locally and might still be part of a \gls{sol}. -A \gls{cp} \solver{} is only able to prove that the problem is \gls{unsat} by try all possible search decisions. +Whereas, values excluded by a search heuristic are merely removed locally and might still be part of a \gls{sol}. +A \gls{cp} \solver{} is only able to prove that the \instance{} is \gls{unsat} by trying all possible search decisions. \Gls{propagation} is not only used when starting the search, but also after making each search decision. This means that some \gls{propagation} depends on the search decision. -Therefore, if the \solver{} needs to reconsider a search decision, then it must also undo all \gls{domain} changes that were caused by \gls{propagation} dependent on that 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 general most common method in \gls{cp} \solvers{} to achieve this is to keep track of \gls{domain} changes using a \gls{trail}. -For every \gls{domain} change that is made during propagation (after the first search decision), the reverse change is stored on in a list. +The most common method in \gls{cp} \solvers{} to to keep track of \gls{domain} changes using a \gls{trail}. +Every \domain{} change that is made during \gls{propagation}, after the first search decision, is stored in a list. Whenever a new search decision is made, the current position of the list is tagged. -If the \solver{} now needs to undo a search decision (\ie\ \gls{backtrack}), it can apply all changes until it reaches the change that is tagged with the search decision. -Because all changes before the tagged point on the \gls{trail} were made before the search decision was made, it is guaranteed that these \gls{domain} changes do not depend on the search decision. -Furthermore, because propagation is performed to a \gls{fixpoint}, it is guaranteed that no duplicate propagation is required. +If the \solver{} now needs to undo a search decision (\ie\ \gls{backtrack}), it can reverse all changes until it reaches the change that is tagged with the search decision. +Because all changes before the tagged point on the \gls{trail} were made before the search decision was made, it is guaranteed that these \domain{} changes do not depend on the search decision. +Furthermore, because \gls{propagation} is performed to a \gls{fixpoint}, it is guaranteed that no duplicate \gls{propagation} is required. The solving method used by \gls{cp} \solvers{} is very flexible. A \solver{} can support many types of \variables{}: they can range from Boolean, floating point numbers, and integers, to intervals, sets, and functions. -Similarly, \solvers{} do not all have access to the same propagators. -Therefore, a \gls{csp} modelled for one \solver{} might look very different to an equivalent \gls{csp} modelled for a different solver. -Instead, \cmls{}, like \minizinc{}, can serve as a standardised form of input for these \solvers{}. -They allow modellers to use high-level constraints that are used directly by the solver when supported, or they are automatically translated to a collection of equivalent supported constraints otherwise. +Similarly, \solvers{} do not all have access to the same \glspl{propagator}. +Therefore, a \gls{slv-mod} for one \solver{} might look very different from a \gls{eqsat} \gls{slv-mod} for a different solver. +\cmls{}, like \minizinc{}, can serve as a standardised form of input for these \solvers{}. +They allow modellers to use always use \glspl{global} and depending on the \solver{} they are either used directly, or they are automatically rewritten using a \gls{decomp}. \begin{example}% \label{ex:back-nqueens} - Consider as an example the N-Queens problem. - Given a chess board of size \(n \times n\), find a placement for \(n\) queen chess pieces such that no queen can attack another. + As an example of the \gls{propagation} mechanism, let us consider as an example the N-Queens problem. + Given a chessboard of size \(n \times n\), find a placement for \(n\) queen chess pieces such that no queen can attack another. Meaning only one queen per row, one queen per column, and one queen per diagonal. - The problem can be modelled in \minizinc\ as follows. + The problem can be modelled in \minizinc\ as follows: \begin{mzn} int: n; set of int: ROW = 1..n; set of int: COL = 1..n; - array [ROW] of var COL: q; + array [COL] of var ROW: q; constraint all_different(q); - constraint all_different([q[i] + i | i in ROW]); - constraint all_different([q[i] - i | i in ROW]); + constraint all_different([q[i] + i | i in COL]); + constraint all_different([q[i] - i | i in COL]); \end{mzn} - Since we know that there can only be one queen per row, the decision in the model left to make is, for every queen, where in the row the piece is placed. - The \constraints{} in the model the remaining rules of the problem: no two queen 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. + The \variables{} in the \gls{array} \mzninline{q} decide for each column in which row the queen will be placed. + This automatically restrict every column to only have a single queen. + As such, no queen will be able to attack vertically. + The \constraints{} in the model the remaining rules of the problem: no two queens can be placed in the same row, no two queen can be place in the same upward diagonal, and no two queens can be place in the same downward diagonal. This model can be directly used in most \gls{cp} \solvers{}, since integer \variables{} and an \mzninline{all_different} \gls{propagator} are common. When solving the problem, initially no values can be eliminated from the \glspl{domain} of the \variables{}. The first propagation will happen when the first queen is placed on the board, the first search decision. - \Cref{fig:back-nqueens} visualises the domain propagation of placing a queen on the d3 square of an eight by eight chess board. - When the queen it placed on the board in \cref{sfig:back-nqueens-1}, it fixes the value of row 4 to the value 3. This implicitly eliminates any possibility of placing another queen in the row. - Now that one queen is placed on the board the propagators for the \mzninline{all_different} constraints can start propagating. + \Cref{fig:back-nqueens} visualises the \gls{propagation} after placing a queen on the d3 square of an eight by eight chessboard. + When the queen it placed on the board in \cref{sfig:back-nqueens-1}, it fixes the value of column 4 (d) to the value 3. This implicitly eliminates any possibility of placing another queen in the column. + Fixing the \domain{} of the column triggers the \glspl{propagator} of the \mzninline{all_different} \constraints{}. As show in \cref{sfig:back-nqueens-2}, the first \mzninline{all_different} constraint can now stop other queens to be placed in the same column. - It eliminates the value 3 from the domains of the queens in the remaining rows. + 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}. - The propagation of the first placed queen severely limits the positions where a second queen can be placed. + The \gls{propagation} after the first placed queen severely limits the positions where a second queen can be placed. \end{example} \begin{figure} @@ -584,9 +662,11 @@ They allow modellers to use high-level constraints that are used directly by the \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}, meaning that all values left in the \glspl{domain} of its \variables{} there is at least one possible variable assignment that satisfies the constraint. -Designing an algorithm that reaches this level of consistency is, however, not an easy task and might require high complexity. +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}. +A \gls{domain-con} \gls{propagator} leaves only values in the \domains{} when there is at least one possible \gls{variable-assignment} that satisfies its \constraint{}. +Designing such a \gls{propagator} is, however, not an easy task. +The algorithm might require high computational complexity. Instead, it can sometimes be better to use a propagator with a lower level of consistency. Although it might not eliminate all possible values of the domain, searching the values that are not eliminated might take less time than achieving \gls{domain-con}. @@ -594,15 +674,16 @@ This is, for example, the case for integer linear constraints: \[ \sum_{i} c_{i} 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 assignment that satisfies the constraint. -Thus far, we have only considered \glspl{csp}. -\gls{cp} solving can, however, also be used to solve optimisation problems using a method called \gls{bnb}. +Thus far, we have only considered finding \glspl{sol} for \glspl{dec-prb}. +\gls{cp} solving can, however, also be used to solve \gls{opt-prb} using a method called \gls{bnb}. The \gls{cp} \solver{} will follow the same method as previously described. -However, when it finds a solution, it does not yet know if this solution is optimal. -It is merely an incumbent solution. -The \solver{} must therefore resume its search, but it is no longer interested in just any solution, only solutions that have a better \gls{objective} value. -This is achieved by adding a new \gls{propagator} that enforces all solutions to have a better \gls{objective} value than the incumbent solution. -If the search process finds another solution, then the incumbent solution is updated and the search process continues. -If the search process does not find any other solutions, then it is proven that there are no better solutions than the current incumbent solution. +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}. +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}. \gls{cp} solvers like Chuffed \autocite{chuffed-2021-chuffed}, Choco \autocite{prudhomme-2016-choco}, \gls{gecode} \autocite{gecode-2021-gecode}, and OR-Tools \autocite{perron-2021-ortools} have long been one of the leading methods to solve \minizinc\ instances. @@ -611,8 +692,8 @@ If the search process does not find any other solutions, then it is proven that \glsreset{lp} \glsreset{mip} -One of the oldest techniques to solve optimisation problems is the use of \gls{lp} \autocite{schrijver-1998-mip}. -A linear program describes a problem using a set of linear equations over continuous variables. +\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{}. In general, a linear program can be expressed in the form: \begin{align*} @@ -626,40 +707,41 @@ The vector \(c\) holds the coefficients of the objective function and the matrix 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. -For problems that are in the form of a linear program, there are proven methods to find the optimal solution. +For problems that are in the form of a linear program, there are proven methods to find an \gls{opt-sol}. In 1947 Dantzig introduced the simplex method, that can find the optimal solution of a linear program in worst-case exponential time. -It was questioned whether the same problem could be solved in worst-case polynomial time, until Khachiyan proved this possible when he introduced the first of the so-called \emph{interior point} methods. +It was questioned whether the same problem could be solved in worst-case polynomial time, until Khachiyan proved this possible when he introduced the first interior point method. These methods provide the foundation for a harder problem. -In \gls{lp} our variables must be continuous. +In \gls{lp} our \variables{} must be continuous. If we require that one or more take a discrete value (\(x_{i} \in \mathbb{N}\)), then the problem suddenly becomes much harder. The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all} \variables{} must take a discrete value). Unlike \gls{lp}, there is no algorithm that can solve a mixed integer program in polynomial time. -The general method to solve a mixed integer program is to treat it as a linear program and find an optimal solution using the simplex method. -If the \variables{} in the problem that are required to be discrete already have discrete values, then we have found our optimal solution. -Otherwise, we pick one of the \variables{}. -For this \variable{} we create a version of the linear program where it is less or equal to the value in the solution rounded down to the nearest discrete value and a version where it is greater or equal to the value in the solution rounded up. -Both versions are solved to find the best solution. -The process is repeated recursively until a discrete solution is found. +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. +Both versions are solved to find the best \gls{sol}. +The process is repeated recursively until a discrete \gls{sol} is found. Much of the power of this solving method comes from bounds that can be inferred during the process. -The solution that the simplex provides an upper bound for the solution in the current step of the solving process. -Similarly, any discrete solution 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 solutions following from the linear program will be strictly worse than the incumbent. +The \gls{sol} to the linear program provides an upper bound for the solution in the current step of the solving process. +Similarly, any discrete \gls{sol} found in an earlier branch of the search process provide a lower bound. +When the upper bound given by the simplex method is lower that the lower bound from an earlier solution, then we know that any discrete \gls{sol} following from the linear program will be strictly worse than the incumbent. Over the years \gls{lp} and \gls{mip} \solvers{} have developed immensely. -\solvers{}, such as \gls{cbc} \autocite{forrest-2020-cbc}, \gls{cplex} \autocite{cplex-2020-cplex}, \gls{gurobi} \autocite{gurobi-2021-gurobi}, and \gls{scip} \autocite{gamrath-2020-scip}, can solve many complex problems. -It is therefore often worthwhile to encode problem as a mixed integer program to find a solution. +Modern \solvers{}, such as \gls{cbc} \autocite{forrest-2020-cbc}, \gls{cplex} \autocite{cplex-2020-cplex}, \gls{gurobi} \autocite{gurobi-2021-gurobi}, and \gls{scip} \autocite{gamrath-2020-scip}, can solve many complex problems. +These \solvers{} are therefore prime targets to solve \minizinc{} \instances{}. -To solve a \gls{csp}, it can be encoded as a mixed integer program. -This process is known as linearisation. +To solve a \instance{} of a \cmodel{}, it can be encoded as a mixed integer program. +This process is known as \gls{linearisation}. It does, however, come with its challenges. -Most \constraints{} in a \minizinc\ model are not linear equations. +Most \constraints{} in a \minizinc{} model are not linear equations. The translation of a single \constraint{} can introduce many linear \constraints{} and even new \variables{}. -For example, when a \constraint{} reasons about the value that a variable will take, to encode it we will need to introduce \glspl{indicator-var}. -The \glspl{indicator-var} \(y_{i}\) for a \variable{} \(x\) take the value 1 if \(x = i\) and 0 otherwise. -\constraints{} reasoning about the value of \(x\) can then be rewritten as linear \constraints{} using the \variables{} \(y_{i}\). +For example, when a \constraint{} reasons about the value that a variable will take, the \gls{linearisation} process introduces indicator variables. +The indicator variables \(y_{i}\) are \glspl{ivar} that for a \variable{} \(x\) take the value 1 if \(x = i\) and 0 otherwise. +\Constraints{} reasoning about the value of \(x\) can then be rewritten as linear \constraints{} using the \variables{} \(y_{i}\). \begin{example} @@ -677,9 +759,9 @@ The \glspl{indicator-var} \(y_{i}\) for a \variable{} \(x\) take the value 1 if \label{line:back-mip-diag2} & \sum_{i,j \in N. i - j =k} y_{ij} \leq 1 & \forall_{k=2-n}^{n-2} \end{align} - The encoding of this variable uses only integers. - Like the \gls{cp} model, integer \variables{} \(q\) are used to represent where the queen is located in each column. - To encode the \mzninline{all_different} constraints, the \glspl{indicator-var} \(y\) are inserted to reason about the value of \(q\). + The encoding of this \cmodel{} uses only integers. + 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. \Cref{line:back-mip-row} ensures that only one queen is placed in the same column. Finally, \cref{line:back-mip-diag1,line:back-mip-diag2} constrain all diagonals to contain only one queen. @@ -691,22 +773,23 @@ The \glspl{indicator-var} \(y_{i}\) for a \variable{} \(x\) take the value 1 if \glsreset{sat} \glsreset{maxsat} -\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 assignment for the variables of a given Boolean formula, such that the formula is satisfied. -This problem can be seen as a restriction of the general \gls{csp} where \variables{} can only be of a Boolean type. +The study of the \gls{sat} problem might be one of the oldest in computer science. +The DPLL algorithm that is used to this day stems from the 60s \autocite{davis-1960-dpll, davis-1962-dpll}, and \gls{sat} was the first problem to be proven to be \gls{np}-complete \autocite{cook-1971-sat}. +The problem asks if there is an \gls{assignment} for the \variables{} of a given Boolean formula, such that the formula is \gls{satisfied}. +This problem can be seen as a restriction of the general \gls{dec-prb} where \variables{} can only be of a Boolean type. There is a field of research dedicated to solving \gls{sat} problems \autocite{biere-2021-sat}. In this field a \gls{sat} problem is generally standardised to be in \gls{cnf}. -A \gls{cnf} is formulated in terms of Boolean literals. -These are variables \(x\) or their negations \(\neg x\). +A \gls{cnf} is formulated in terms of literals. +These are Boolean \variables{} \(x\) or their negations \(\neg x\). These literals are then used in a conjunction of disjunctive clauses: a Boolean formula in the form \(\forall_{i \in P} \exists_{b \in C_{i}} b\). -To solve the \gls{sat} problem, the \solver{} has to find an assignment for the \variables{} where at least one literal is true in every clause. +To solve the \gls{sat} problem, the \solver{} has to find an \gls{assignment} for the \variables{} where at least one literal is true in every clause. Even though the problem is proven to be hard to solve, a lot of progress has been made towards solving even the biggest the most complex \gls{sat} problems. -Modern day \gls{sat} solvers, like Kissat \autocite{biere-2021-kissat} and Clasp \autocite{gebser-2012-clasp}, can solve instances of the problem with thousands of \variables{} and clauses. +Modern day \gls{sat} solvers, like Clasp \autocite{gebser-2012-clasp}, Kissat \autocite{biere-2021-kissat} and MiniSAT \autocite{een-2003-minisat} , can solve instances of the problem with thousands of \variables{} and clauses. -Many real world problems modelled in \cmls\ directly correspond to \gls{sat}. -However, even problems that contain \variables{} with types other than Boolean can often be encoded as a \gls{sat} problem. +Many real world problems modelled using \cmls{} directly correspond to \gls{sat}. +However, even problems that contain \variables{} with types other than Boolean can still be encoded as a \gls{sat} problem. Depending on the problem, using a \gls{sat} \solvers{} to solve the encoded problem can still be the most efficient way to solve the problem. \begin{example} @@ -723,38 +806,39 @@ Depending on the problem, using a \gls{sat} \solvers{} to solve the encoded prob \label{line:back-sat-diag2} & \neg q_{ij} \lor \neg q_{(i+k)(j-k)} & \forall_{i,j \in N} \forall_{k=1}^{\min(n-i, j)} \end{align} - The encoding of the problem uses a Boolean \variable{} for every position of the chess board. + The encoding of the problem uses a Boolean \variable{} for every position of the chessboard. Each \variable{} represents if a queen will be located on this position or not. - \Cref{line:back-sat-at-least} forces that a queen is placed on every row of the chess board. + \Cref{line:back-sat-at-least} forces that a queen is placed on every row of the chessboard. \Cref{line:back-sat-row,line:back-sat-col} ensure that only one queens is place in each row and column respectively. \Cref{line:back-sat-diag1,line:back-sat-diag2} similarly constrain each diagonal to contain only one queen. \end{example} A variation on \gls{sat} is the \gls{maxsat} problem. -Where in a \gls{sat} problem all clauses need to be satisfied, this is not the case in a \gls{maxsat} problem. +In a \gls{sat} problem all clauses need to be \gls{satisfied}, but this is not the case in a \gls{maxsat} problem. 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 assignment for Boolean \variables{} that maximises the cumulative weights of the satisfied clauses. +The goal in the \gls{maxsat} problem is then to find an assignment for Boolean \variables{} that maximises the cumulative weights of the \gls{satisfied} clauses. -The \gls{maxsat} problem is analogous to a \gls{cop}. -Like a \gls{cop}, the aim of \gls{maxsat} is to find the optimal solution to the problem. +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 difference is that the weights are given to the \constraints{} instead of the \variables{} or a function over them. -It is, again, often possible to encode a \gls{cop} as a \gls{maxsat} problem. -A naive approach to encode an integer objective is, for example, to encode each value in the domain as a Boolean variable and assign that same value to a clause containing just that Boolean variable. +It is, again, possible to encode 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. For many problems the use of \gls{maxsat} \solvers{} can offer a very successful method to find the optimal solution to a problem. \section{Other Constraint Modelling Languages}% \label{sec:back-other-languages} -Although \minizinc\ is the \cml\ that is the primary focus of this thesis, there are many other \cmls{}. +Although \minizinc{} is the \cml{} that is the primary focus of this thesis, there are many other \cmls{}. Each \cml{} has its own focus and purpose and comes with its own strength and weaknesses. Most of the techniques that are discusses in this thesis can be adapted to these languages. We will now discuss some other prominent \cmls{} and will compare them to \minizinc{} to indicate to the reader where techniques might have to be adjusted to fit other languages. -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. +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. \subsection{AMPL}% \label{sub:back-ampl} @@ -767,12 +851,12 @@ Specifically \gls{ampl} was designed to model linear programs. These days \gls{ampl} has been extended to allow more advanced \solver{} usage. Depending on the \gls{solver} targeted by \gls{ampl}, the language can give the modeller access to additional functionality. For \solvers{} that have a \gls{mip} solving method, the modellers can require \variables{} to be integers. -Different types of \solvers{} can also have access to different types of constraints, such as quadratic and non-linear constraints. +Different types of \solvers{} can also have access to different types of \constraints{}, such as quadratic and non-linear constraints. \gls{ampl} has even been extended to allow the usage of certain \glspl{global} when using a \gls{cp} \solver{} \autocite{fourer-2002-amplcp}. \begin{example} - If we consider the well-known \gls{tsp}, then we might model this problem in \gls{ampl} as follows: + If we consider the well-known travelling salesman problem, then we might model this problem in \gls{ampl} as follows: \begin{plain} set Cities ordered; @@ -815,9 +899,9 @@ Different types of \solvers{} can also have access to different types of constra The main reason for this difference is the level at which these models are written. The \gls{ampl} model is written to target a \gls{mip} solver. In the \gls{ampl} language this means that you can only use the language functionality that is compatible with the targeted \solver{}; in this case, all expression have to be linear equations. - In \minizinc\ the modeller is not constrained in the same way. - The modeller is always encouraged to create high-level \constraint{} models. - It is the job of the \solver{}'s \minizinc\ library to transform the high-level constraints into compatible \solver{}-level \constraints{}. + In \minizinc{} the modeller is not constrained in the same way. + The modeller is always encouraged to create high-level \cmodels{}. + \minizinc{} will then rewrite these models into compatible \glspl{slv-mod}. \end{example} \subsection{OPL}% @@ -825,7 +909,7 @@ Different types of \solvers{} can also have access to different types of constra \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}. -The syntax of \gls{opl} is very similar to the \minizinc\ syntax. +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}. @@ -882,12 +966,12 @@ When solving a scheduling problem, the \gls{opl} makes use of specialised interv solve minimize makespan; \end{mzn} - Note that the \minizinc{} model does not have explicit Activity variables. + Note that the \minizinc{} model does not have explicit Activity \variables{}. It must instead use \variables{} that represent the start times of the activity and a \variable{} to represent the time at which all activities are finished. The \gls{opl} model also has the advantage that it can first create resource objects and then use the \texttt{requires} keyword to force tasks on the same machine to be mutually exclusive. In \minizinc{} the same requirement is implemented through the use of \mzninline{disjunctive} constraints. Although this has the same effect, all mutually exclusive jobs have to be combined in a single statement in the model. - This can make it harder in \minizinc\ to write the correct \constraint{} and its meaning might be less clear. + This can make it harder in \minizinc{} to write the correct \constraint{} and its meaning might be less clear. \end{example} @@ -912,7 +996,8 @@ It is therefore not possible to connect other \solvers{} to \gls{opl}. \subsection{Essence}% \label{sub:back-essence} -\gls{essence} \autocite{frisch-2007-essence} is another high-level \cml\ is cherished for its adoption of high-level \variable{} types. +\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: \begin{itemize} @@ -923,8 +1008,7 @@ In addition to all variable types that are contained in \minizinc{}, \gls{essenc \end{itemize} Since sets, multi-sets, and functions can be defined on any other type, these types can be arbitrary nested and the modeller can define, for example, a \variable{} that is a sets of sets of integers. -Partitions can be defined for finite types. -The base types in \gls{essence} are restricted to Boolean, enumerated types, or a restricted set of integers. +Partitions can be defined for finite types: Booleans, enumerated types, or a restricted set of integers. \begin{example} @@ -981,15 +1065,16 @@ The base types in \gls{essence} are restricted to Boolean, enumerated types, or \end{example} -The high-level variables available in \gls{essence} are often not directly supported by the \solvers{} that is employed to solve \gls{essence} instances. -To solve the problem, not only do the \constraints{} have to be translated to \constraints{} supported by the solver, but also all \variables{} have to be translated to a combination of \constraints{} and \variables{} compatible with the targeted solver. +The high-level \variables{} available in \gls{essence} are often not \gls{native} to \solvers{}. +To solve an \instance{}, not only do the \constraints{} have to be translated to \constraints{} \gls{native} to the \solver{}, but also all \variables{} have to be translated to a combination of \constraints{} and \variables{} \gls{native} to the \solver{}. \section{Term Rewriting}% \label{sec:back-term} \glsreset{trs} -At the heart of the flattening process, the process as described in \cref{sec:back-minizinc} that translates a \minizinc{} instance into solver level \flatzinc{}, 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}. +At the heart of the \gls{rewriting} process, to transform 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 \emph{function} and \emph{constant} symbols. An example of a term is \(F(0 + 1,F(1,0))\), where \(F\) and \(+\) are function symbols and \(0\) and \(1\) are constant symbols. In a term rewriting rule, a term can also contain a \emph{term variable} which captures a term sub-expression. @@ -1014,33 +1099,33 @@ In a term rewriting rule, a term can also contain a \emph{term variable} which c \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 term where 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 will be \(0\); otherwise, the result will be \(1\). These properties are also interesting when in the translation process of a \minizinc{} instance into \flatzinc{}. -The confluence of the translation process will ensure that the same \flatzinc{} is produced independently of the order in which the \minizinc\ model is processed. -This is a desirable quality as it makes the behaviour of the translation process more predictable. +The \gls{confluence} of the \gls{rewriting} process will ensure that the same \gls{slv-mod} is produced independently of the order in which the \minizinc{} \instance{} is processed. +This is a desirable quality as it makes the behaviour of the \gls{rewriting} process more predictable. -Many of the techniques used by \solvers{} targeted by \minizinc\ are proven to be complete. -Meaning that they are guaranteed to find a (best) solution to the problem or prove that there is none. -For this quality to hold for the \minizinc\ solving process, it has to be guaranteed that the \minizinc\ translation process terminates (so the solving process can start). +Many of the techniques used by \solvers{} targeted by \minizinc{} are proven to be complete. +Meaning that they are guaranteed to (eventually) find a (optimal) \gls{sol} for the \instance{} or prove that there is none. +For this quality to hold for the overall \minizinc{} solving process, it has to be guaranteed that the \minizinc{} \gls{rewriting} process terminates (so the solving process can start). -In the remainder of this section we will discuss two types of \glspl{trs} that are closely related to \cmls\ and their compilation into solver level constraint models: \gls{clp} and \gls{chr}. +In the remainder of this section we will discuss two types of \glspl{trs} that are closely related to \cmls{} and the \gls{rewriting} process: \gls{clp} and \gls{chr}. \subsection{Constraint Logic Programming}% \label{subsec:back-clp} \glsreset{clp} \gls{clp} \autocite{marriott-1998-clp} can be seen as a predecessor of \cmls{} like \minizinc{}. -A constraint logic program describes the process in which a high level constraint model is eventually rewritten into a solver level constraints and added to a \solver{}. -Like in \minizinc{}, can define \constraint{} predicates to use in the definition of the \constraint{} model. +A constraint logic program describes the process in which \cmodel{} is eventually rewritten into a \gls{slv-mod} and solved by a \solver{}. +Like in \minizinc{}, can define \constraint{} predicates to use in the definition of the \cmodel{}. 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 the solver level \glspl{constraint} are all satisfied. +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}. -Variables are another notable difference between \cmls\ and \gls{clp}. +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 might be replaced or equated with a constant symbol, but, different from \cmls{}, this is not a requirement. A variable can remain a name in the solution of a constraint logic program. @@ -1049,31 +1134,31 @@ In cases where an instantiated solution is required, a special \mzninline{labeli Similarly, there is a \mzninline{minimize} \constraint{} that can be 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 rewriting of the constraint predicates is tried in the order in which the different rewriting rules for the constraint predicates are defined. -The process is completed when all constraints are rewritten and no inconsistency is detected between the solver level constraints that are produced. -If all the possible ways of rewriting the program are tried, but all of them prove to be inconsistent, then the program itself can be said to be unsatisfiable. +The \gls{rewriting} of the constraint predicates is tried in the order in which the different \gls{rewriting} rules for the constraint predicates are defined. +The process is completed when all constraints are rewritten and no inconsistency is detected between the \gls{native} \constraints{} that are produced. +If all the possible ways of rewriting the program are tried, but all of them prove to be inconsistent, then the program itself can be said to be \gls{unsat}. Even when a correct rewriting is found, it is possible to continue the process. This way you can find all possible correct ways to rewrite the program. -To implement this mechanism there is a tight integration between the \solver{}, referred to as the \gls{constraint-store}, and the evaluator of the constraint logic program. -In addition to just adding \constraints{}, the program can also inspect the status of the constraint and retract constraints from the constraint store. -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 \gls{constraint-store} to its state before the last decision was made) and try the next rewriting rule. +To implement this mechanism there is a tight integration between the \solver{}, referred to as the \emph{constraint store}, and the evaluator of the constraint logic program. +In addition to just adding \constraints{}, the program can also inspect the status of the \constraint{} and retract \constraints{} from the constraint store. +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 \gls{constraint-store} can influence the correctness of a constraint logic program. -Some \solvers{} are incomplete; it is unable to tell if some of its \constraints{} are satisfied or not. +The strength of the constraint store can influence the correctness of a constraint logic program. +Some \solvers{} are incomplete; it is unable to tell if some of its \constraints{} are \gls{satisfied} or not. This, for example, happens with \solvers{} that work with integer \glspl{domain}. In these cases the programmer must use the \mzninline{labeling} constraint to force constant values for the variables. -Once the variables have been assigned constant values, the solver will be able to decide if the constraints are satisfied. +Once the variables have been assigned constant values, the \solver{} will always be able to decide if the \constraints{} are \gls{satisfied}. \subsection{Constraint Handling Rules}% \label{sub:back-chr} \glsreset{chr} -When \constraints{} are seen as terms in a \gls{trs}, then it is not just possible to define rules to rewrite constraints to the level of a \solver{}. -It is also possible to define rules to simplify, propagate, and derive new constraints within the solver. +When \constraints{} are seen as terms in a \gls{trs}, then it is not just possible to define rules to rewrite \constraints{} to \gls{native} \constraints{}. +It is also possible to define rules to simplify, propagate, and derive new \constraints{} within the \solver{}. \gls{chr} follow from this idea. -\gls{chr} are a language extension (targeted at \gls{clp}) to allow user-defined constraints within a \solver{}. -\constraints{} defined using \gls{chr} are rewritten into simpler constraints until they are solved. +\gls{chr} are a language extension (targeted at \gls{clp}) to allow user-defined \constraints{} within a \solver{}. +\constraints{} defined using \gls{chr} are rewritten into simpler \constraints{} until they are solved. Different from \gls{clp}, \gls{chr} allows term rewriting rules that are multi-headed. This means that, for some rules, multiple terms must match, to apply the rule. @@ -1088,21 +1173,21 @@ This means that, for some rules, multiple terms must match, to apply the rule. transitivity @ X -> Y, Y -> Z ==> X -> Z \end{plain} - These definitions specify how \texttt{->} simplifies and propagates as a constraint. + These definitions specify how \texttt{->} simplifies and propagates as a \constraint{}. 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. This rule removes the term \texttt{X -> Y}. - Since the constraint is said to be logically true, nothing gets added. + Since the \constraint{} is said to be logically true, nothing gets added. \texttt{X = Y} functions as a guard. - This \solver{} built-in \constraint{} is required for the rewriting rule to apply. + This \solver{} \gls{native} \constraint{} is required for the rewriting rule to apply. - \item The second rule implements the anti-symmetry of logical implications; the two implications, \texttt{X -> Y} and \texttt{Y -> X}, are replaced by a \solver{} built-in, \texttt{X = Y}. + \item The second rule implements the anti-symmetry of logical implications; the two implications, \texttt{X -> Y} and \texttt{Y -> X}, are replaced by a \solver{} \gls{native}, \texttt{X = Y}. - \item Finally, the transitivity rule introduces a derived constraint. - When it finds constraints \texttt{X -> Y} and \texttt{Y -> Z}, then it adds another constraint \texttt{X -> Z}. - Different from the other rules, no constraints are removed. + \item Finally, the transitivity rule introduces a derived \constraint{}. + When it finds the \constraints{} \texttt{X -> Y} and \texttt{Y -> Z}, then it adds another constraint \texttt{X -> Z}. + Different from the other rules, no \constraints{} are removed. \end{itemize} Note that the use of multi-headed rewriting rules is essential to define these rules. @@ -1110,33 +1195,34 @@ This means that, for some rules, multiple terms must match, to apply the rule. \end{example} The rules in a \gls{chr} system can be categorised into three different categories: simplification, propagation, and simpagation. -The first two rules in the previous example are simplification rules: they replace some constraint atoms by others. -The final rule in the example was a propagation rule: based on the existence of certain constraints, new constraints can be introduced. +The first two rules in the previous example are simplification rules: they replace some \constraint{} atoms by others. +The final rule in the example was a propagation rule: based on the existence of certain \constraints{}, new \constraints{} can be introduced. Simpagation rules are a combination of both types of rules in the form: \[ H_{1}, \ldots H_{l} \backslash H_{l+1}, \ldots, H_{n} \texttt{<=>} G_{1}, \ldots{}, G_{m} | B_{1}, \ldots, B_{o} \] -It is possible to rewrite using a simpagation rule when there are terms matching \(H_{1}, \ldots, H_{n}\) and there are \solver{} built-ins \(G_{1}, \ldots{}, G_{m}\). +It is possible to rewrite using a simpagation rule when there are terms matching \(H_{1}, \ldots, H_{n}\) and there are \solver{} \gls{native} \constraints{} \(G_{1}, \ldots{}, G_{m}\). When the simpagation rule is applied, the terms \(H_{l+1}, \ldots, H_{n}\) are replaced by the terms \(B_{1}, \ldots, B_{o}\). The terms \(H_{1}, \ldots H_{l}\) are kept in the system. Since simpagation rules incorporate both the elements of simplification and propagation rules, it is possible to formulate all rules as simpagation rules. -\section{Compiling \glsentrytext{minizinc}}% +\section{Rewriting \glsentrytext{minizinc}}% \label{sec:back-mzn-interpreter} -Traditionally the compilation process is split into three sequential parts: the \emph{frontend}, the \emph{middle-end}, and the \emph{backend}. +Traditionally a \compiler{} is split into three sequential parts: the \emph{frontend}, the \emph{middle-end}, and the \emph{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 in a target-independent fashion. +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. +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. -The \minizinc\ compilation process categorised in the same three categories, as shown in \cref{fig:back-mzn-comp}. -In the frontend, a \minizinc\ model is first parsed together with its data into an \gls{ast}. -The process will then analyse 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 user. +The \minizinc{} compilation process categorised in the same three categories, as shown in \cref{fig:back-mzn-comp}. +In the frontend, a \minizinc{} model is combined with its data into an \instance{}. +The instance parsed into an \gls{ast}. +The process will then analyse the \gls{ast} to discover the types of all expressions used in the \instance{}. +If an inconsistency is discovered, then an error is reported to the modeller. Finally, the frontend will also preprocess the \gls{ast}. -This process is used to rewrite expressions into a common form for the middle-end, \eg\ remove the ``syntactic'' sugar. +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. \begin{figure} @@ -1144,65 +1230,67 @@ For instance, replacing the usage of enumerated types by normal integers. \includegraphics[width=\linewidth]{assets/img/back_compilation_structure} \caption{\label{fig:back-mzn-comp} The compilation structure of the \minizinc\ compiler.} + \jip{adjust to rewriting instead of flatten} \end{figure} The middle-end contains the most important two processes: the flattening and the optimisation. -During the flattening process the high-level (\minizinc{}) constraint model is rewritten into a solver level (\flatzinc{}) constraint model. -It could be noted that the flattening step depends on the compilation target to define its solver level constraints. +During the flattening 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{}. 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-flattening}. -Once a solver level constraint model is constructed, the \minizinc\ compiler will try to optimise this model: shrink domains of variables, remove constraints that are proven to hold, and remove variables that have become unused. +A full description of this process will follow in \cref{subsec:back-rewriting}. +Once a \gls{slv-mod} is constructed, the \minizinc{} \compiler{} will try to optimise this model: shrink \domains{} of \variables{}, remove \constraints{} that are proven to hold, and remove \variables{} that have become unused. These optimisation techniques are discussed in \cref{subsec:back-fzn-optimisation}. -The backend will convert the internal solver level constraint model into a format that can be used by the targeted \solver{}. +The backend will convert the internal \gls{slv-mod} into a format that can be used by the targeted \solver{}. Given the formatted artefact, a solver process, controlled by the backend, can then be started. -Whenever the solver process produces a solution, the backend will reconstruct the solution to the specification of the original \minizinc{} model. +Whenever the solver process produces a \gls{sol}, the backend will reconstruct the \gls{sol} to the specification of the original \minizinc{} model. -In this section we will discuss the flattening and optimisation process as employed by the 2.5.5 version of \minizinc{} \autocite{minizinc-2021-minizinc}. +In this section we will discuss the \gls{rewriting} and optimisation process as employed by the 2.5.5 version of \minizinc{} \autocite{minizinc-2021-minizinc}. -\subsection{Flattening}% -\label{subsec:back-flattening} +\subsection{Rewriting}% +\label{subsec:back-rewriting} -The goal of the flattening process is to arrive at a ``flat'' constraint model: it only contains constraints that consist of a singular call instruction, all arguments to calls are \parameter{} literals or \variable{} identifiers, and the call itself is a constraint primitive for 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 call instruction, all arguments to calls are \parameter{} literals or \variable{} identifiers, and using only \constraints{} and \variable{} types that are \gls{native} to the target \solver{}. -To arrive at a flat model, the flattening process will transverse the declarations, \constraints{}, and the solver goal and flatten any expression contained in these items. -During the flattening of an expression, the expression rewritten into other \minizinc\ expressions according to the decomposition given in the target \solver{}'s \minizinc\ library. -Enforced by \minizinc{}'s type system, at most one rule applies for any given constraint. -The flattening of expressions is performed bottom-up, we flatten any sub-expression before its parent expression. -For instance, in a call each argument is flattened before the call itself is flattened. +To arrive at a flat \gls{slv-mod}, the \gls{rewriting} process will transverse the declarations, \constraints{}, and the solver goal and rewrite any expression contained in these items. +During the \gls{rewriting} of an expression, the expression rewritten into other \minizinc{} expressions according to the \gls{decomp} given in the target \solver{}'s library. +Enforced by \minizinc{}'s type system, at most one rule applies for any given \constraint{}. +The \gls{rewriting} of expressions is performed bottom-up, we rewrite any sub-expression before its parent expression. +For instance, in a call each argument is rewritten before the call itself is rewritten. -An exception to this bottom-up approach is the flattening of \gls{generator} expressions. -Expression containing \glspl{generator}, such as array \glspl{comprehension} and loops, have to be instantiated before their sub-expression can be flattened. +An exception to this bottom-up approach is the \gls{rewriting} of \gls{generator} expressions. +Expression containing \glspl{generator}, such as array \glspl{comprehension} and loops, have to be instantiated before their sub-expression can be rewritten. The compiler exhaustively binds the values of the \gls{generator} to the specified identifiers. -For each iteration the compiler flattens the sub-expression and collects its result. -Once the \gls{generator} is exhausted, the compiler can flatten its surrounding expression using the collected values. +For each iteration the compiler rewrites the sub-expression and collects its result. +Once the \gls{generator} is exhausted, the compiler can rewrite its surrounding expression using the collected values. -The decomposition system in \minizinc\ is defined in terms of functions declarations. +The \gls{decomp} system in \minizinc{} is defined in terms of functions declarations. Any call, whose declaration has a function body, will eventually be replaced by an instantiation of this function body using the arguments to the call. -Calls are, however, not the only type of expression that are decomposed during the flattening process. -Other expression, like \gls{operator} expressions, variable array access, and if-then-else expressions, might also have to be decomposed for the targeted \solver{}. -During the flattening process, these expressions are rewritten into equivalent call expressions that will start the decomposition process. +Calls are, however, not the only type of expression that are decomposed during the \gls{rewriting} process. +Other expression, like \gls{operator} expressions, variable array access, and if-then-else expressions, might also have to be decomposed for the target \solver{}. +During the \gls{rewriting} process, these expressions are rewritten into equivalent call expressions that will start the decomposition process. -A notable effect of the flattening is that sub-expression are replaced by literals or identifiers. -If the expression contains only \parameters{}, then the flattening 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 flattening process. +A notable effect of the \gls{rewriting} is that sub-expression are replaced by literals or identifiers. +If the expression contains only \parameters{}, then the \gls{rewriting} of the expression is merely a calculation to find the value of the literal to be put in its place. +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: \begin{itemize} - \item For Boolean expressions in a non-root context, the new \variable{} is inserted by the flattening process itself. - To constrain this \variable{}, the flattener will then add the \gls{reification} of the constraint. - This constraint contains a call a variation of the call that would have been generated for the expression in root context. + \item For Boolean expressions in a non-\rootc{} context, the new \variable{} is inserted by the \gls{rewriting} process itself. + To constrain this \variable{}, the \compiler{} will then add the \gls{reification} 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 reification of the original expression: setting the additional argument to \mzninline{true} if the constraint is satisfied, and \mzninline{false} otherwise. + The definition of this constraint should implement the \gls{reification} of the original expression: setting the additional argument to \mzninline{true} if the constraint is \gls{satisfied}, and \mzninline{false} otherwise. For example, the constraint in \minizinc{} \begin{mzn} constraint b \/ this_call(x, y); \end{mzn} - will during flattening be turned into: + \noindent{} will during \gls{rewriting} be turned into: \begin{mzn} var bool: i1; @@ -1224,34 +1312,35 @@ The creation of this new \variable{} and defining \constraints{} happens in one Using a \gls{let} it explicitly creates a new \variable{}, constrains this \variable{} to take to correct value, and returns the newly created \variable{}. \end{itemize} -These are the basic steps that are followed to flatten \minizinc\ instance. +These are the basic steps that are followed to rewrite \minizinc{} instance. This is, however, not the complete process. -The quality of a \flatzinc\ model is of the utmost importance. -A \flatzinc\ containing extra \variables{} and \constraints{} that do not add any information to the solving process might exponentially slow down the solving process. -Therefore, the \minizinc\ flattening process is extended using many techniques to help improve the quality of the flattened model. -In \crefrange{subsec:back-cse}{subsec:back-delayed-rew}, we will discuss the most important techniques used to improve the flattening process. +The quality of the resulting \gls{slv-mod} is of the utmost importance. +A \gls{slv-mod} containing extra \variables{} and \constraints{} that do not add any information to the solving process might exponentially slow it down. +Therefore, the \minizinc{} \gls{rewriting} process is extended using many techniques to help improve the quality of the \gls{slv-mod}. +In \crefrange{subsec:back-cse}{subsec:back-delayed-rew}, we will discuss the most important techniques used to improve the \gls{rewriting} process. \subsection{Common Sub-expression Elimination}% \label{subsec:back-cse} +\glsreset{cse} Because the evaluation of a \minizinc{} expression cannot have any side effects, it is possible to reuse the same result for equivalent expressions. -This simplification is a well understood technique that originates from compiler optimisation \autocite{cocke-1970-cse} and has proven to be very effective in discrete optimisation \autocite{marinov-2005-sat-optimisations, araya-2008-cse-numcsp}, including during the evaluation of \cmls\ \autocite{rendl-2009-enhanced-tailoring}. +This simplification, called \gls{cse}, is a well understood technique that originates from compiler optimisation \autocite{cocke-1970-cse} and has proven to be very effective in discrete optimisation \autocite{marinov-2005-sat-optimisations, araya-2008-cse-numcsp}, including during the evaluation of \cmls{} \autocite{rendl-2009-enhanced-tailoring}. \begin{example} \label{ex:back-cse} - For instance, in the constraint + For instance, in the \constraint{} \begin{mzn} constraint (abs(x)*2 >= 20) \/ (abs(x)+5 >= 15); \end{mzn} - the expression \mzninline{abs(x)} occurs twice. + \noindent{}the expression \mzninline{abs(x)} occurs twice. There is however no need to create two separate \variables{} (and defining \constraints{}) to represent the absolute value of \mzninline{x}. The same \variable{} can be used to represent the \mzninline{abs(x)} in both sides of the disjunction. \end{example} Seeing that the same expression occurs multiple times is not always easy. -Some expressions only become syntactically equal during evaluation, as in the following example. +Some expressions only become syntactically equal when instantiated, as in the following example. \begin{example} Consider the fragment: @@ -1265,29 +1354,29 @@ Some expressions only become syntactically equal during evaluation, as in the fo constraint pythagoras(i, i) >= 5; \end{mzn} - 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. + 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 memorisation. -After the flattening of an expression, the instantiated expression and its result are stored in a lookup table, the \gls{cse} table. +To ensure that the same instantiation of a function are only evaluated once, the \minizinc{} \compiler{} uses memorisation. +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 flattened the \gls{cse} table is consulted. If an equivalent expression is found, then the accompanying result is used; otherwise, the evaluation proceeds as normal. In our example, the evaluation of \mzninline{pythagoras(i, i)} would proceed as normal to evaluate \mzninline{x = pow(i, 2)}. However, the expression defining \mzninline{y}, \mzninline{pow(i, 2)}, will be found in the \gls{cse} table and replaced by the earlier stored result: \mzninline{y = x}. -\gls{cse} also has an important interaction with the occurrence of reified constraints. -\Glspl{reification} of a \constraint{} are often defined in the library in terms of complicated decompositions into simpler constraints, or require specialised algorithms in the target solvers. +\gls{cse} also has an important interaction with the occurrence of \glspl{reification}. +\Glspl{reification} are often defined in the library in terms of complicated \gls{decomp} into \gls{native} \constraints{}, or require more complex algorithms in the target \solver{}. In either case, it can be very beneficial for the efficiency solving process if we can detect that a reified constraint is in fact not required. -If a constraint is present in the root context, it means that it must hold globally. -If the same constraint is used in a reified context, it can therefore be replaced with the constant \mzninline{true}, avoiding the need for reification (or in fact any evaluation). +If a \constraint{} is present in the root context, it means that it must hold globally. +If the same \constraint{} is used in a non-\rootc{} context, it can therefore be replaced with the constant \mzninline{true}, avoiding the need for \gls{reification} (or in fact any evaluation). -We can harness \gls{cse} to store the evaluation context when a constraint is added, and detect when the same constraint is used in both contexts. +We can harness \gls{cse} to store the evaluation context when a \constraint{} is added, and detect when the same \constraint{} is used in both contexts. Whenever a lookup in the \gls{cse} table is successful, action can be taken depending on both the current and stored evaluation context. -If the stored expression was in root context, then the constant \mzninline{true} can be used, independent of the current context. -Otherwise, if the stored expression was in reified context and the current context is reified, then the stored result variable can be used. -Finally, if the stored expression was in reified context and the current context is root context, then the previous result can be replaced by the constant \mzninline{true} and the evaluation will proceed as normal with the root context constraint. +If the stored expression was in \rootc{} context, then the constant \mzninline{true} can be used, independent of the current context. +Otherwise, if the stored expression was in non-\rootc{} context and the current context is non-\rootc{}, then the stored result variable can be used. +Finally, if the stored expression was in non-\rootc{} context and the current context is \rootc{} context, then the previous result can be replaced by the constant \mzninline{true} and the evaluation will proceed as normal with the \rootc{} context \constraint{}. \begin{example} Consider the fragment: @@ -1299,9 +1388,9 @@ Finally, if the stored expression was in reified context and the current context constraint b1 <-> p(x,y); \end{mzn} - If we process the top-level 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 root context. + 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. So \gls{cse} needs to set \mzninline{b0} to \mzninline{true}. \end{example} @@ -1309,17 +1398,17 @@ Finally, if the stored expression was in reified context and the current context \label{subsec:back-adjusting-dom} Sometimes a \constraint{} can be detected to be true based on its semantics, and the known \glspl{domain} of \variables{}. -For example, consider the constraint \mzninline{3*x + 7*y > 8}, and assume that both \mzninline{x} and \mzninline{y} cannot be smaller than 1. In this case, we can determine that the constraint is always satisfied, and remove it from the model without changing satisfiability. +For example, consider the constraint \mzninline{3*x + 7*y > 8}, and assume that both \mzninline{x} and \mzninline{y} cannot be smaller than 1. In this case, we can determine that the constraint is always \gls{satisfied}, and remove it from the model without changing satisfiability. This is a simple form of \gls{propagation}, which, as discussed in \cref{subsec:back-cp}, can also tighten the \glspl{domain} of \variables{} in the presence of a \constraint{}. -The principles of \constraint{} propagation can also be applied during the flattening of a \minizinc\ model. +The principles of \gls{propagation} can also be applied during the \gls{rewriting} of a \minizinc{} model. It is generally a good idea to detect cases where we can directly change the \gls{domain} of a \variable{}. -Sometimes this might mean that the \constraint{} does not need to be added at all and that constricting the \gls{domain} is enough. -Tight domains can also allow us to avoid the creation of reified constraints when the truth-value of a reified \constraint{} can be determined from the \glspl{domain} of variables. +Sometimes this might mean that the \constraints{} does not need to be added at all and that constricting the \gls{domain} is enough. +Tight domains can also allow us to avoid the creation of \glspl{reification} when the truth-value of a reified \constraint{} can be determined from the \domains{}. \begin{example}% \label{ex:back-adj-dom} - Consider the following \minizinc\ model: + Consider the following \minizinc{} model: \begin{mzn} var 1..10: a; @@ -1329,26 +1418,26 @@ Tight domains can also allow us to avoid the creation of reified constraints whe constraint (a > 5) -> (a + b > 12); \end{mzn} - Given the \glspl{domain} specified in the model, the second constraint is flattened using to reified \constraints{} for each side of the implication. + Given the \domain{} specified in the model, the second \constraint is rewritten using a reified \constraints{} 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 flattening the first \constraint{}, then the second \gls{constraint} can be simplified. - The expression \mzninline{a > 5} is known to be \mzninline{false}, which means that the constraint can be simplified to \mzninline{true}. + When the compiler adjusts the domain of \mzninline{a} while \gls{rewriting} the first \constraint{}, then the second \constraint{} can be simplified. + The expression \mzninline{a > 5} is known to be \mzninline{false}, which means that the \constraint{} can be simplified to \mzninline{true}. \end{example} -During flattening, the \minizinc\ compiler will actively remove values from the \gls{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}), constraint 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 will actively remove values from the \domain{} when it encounters \constraints{} that trivially reduces it. +For example, \constraints{} with a single comparison expression between a \variable{} and a \parameter{} (\eg\ \mzninline{x != 5}), \constraints{} with a single comparison between two \variables{} (\eg\ \mzninline{x >= y}), \constraints{} that directly change the domain (\eg\ \mzninline{x in 3..5}). It, however, will not perform more complex \gls{propagation}, like the \gls{propagation} of \glspl{global}. \subsection{Constraint Aggregation}% \label{subsec:back-aggregation} -Complex \minizinc\ expression can sometimes result in the creation of many new variables that represent intermediate results. -This is in particular true for linear and boolean equations that are generally written using \minizinc\ operators. +Complex \minizinc{} expression can sometimes result in the creation of many \glspl{ivar} to represent intermediate results. +This is in particular true for linear and boolean equations that are generally written using \minizinc{} operators. \begin{example}% \label{ex:back-agg} - For example the evaluation of the linear constraint \mzninline{x + 2*y <= z} could result in the following \flatzinc: + For example the evaluation of the linear constraint \mzninline{x + 2*y <= z} could result in the following \flatzinc{}: \begin{nzn} var int: x; @@ -1361,7 +1450,7 @@ 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 intermediate variables 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 \glspl{ivar} 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} @@ -1369,76 +1458,76 @@ This is in particular true for linear and boolean equations that are generally w \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 intermediate values that have to be given a value in the solution. + 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. \end{example} This can be resolved using the \gls{aggregation}. -When we aggregate constraints we collect multiple \minizinc\ expressions, that would each have been separately translated, and combine them into a singular structure that eliminates the need for intermediate \variables{}. -For example, the arithmetic definitions can be combined into linear constraints, Boolean logic can be combined into clauses, and counting constraints can be combined into global cardinality constraints. +When we aggregate \constraints{} we collect multiple \minizinc{} expressions, that would each have been rewritten separately, and combine them into a singular structure that eliminates the need for \glspl{ivar}. +For example, the arithmetic definitions can be combined into linear \constraints{}, Boolean logic can be combined into clauses, and counting \constraints{} can be combined into global cardinality \constraints{}. -The \minizinc\ compiler aggregates expressions whenever possible. -When the \minizinc\ compiler reaches an expression that could potentially be part of an aggregated constraint, the compiler will not flatten the expression. -The compiler will instead perform a search of its sub-expression to collect all other expressions to form an aggregated constraint. -The flattening process continues by flattening this aggregated constraint, which might still contain non-flat arguments. +The \minizinc{} \compiler{} aggregates expressions whenever possible. +When the \minizinc{} \compiler{} reaches an expression that could potentially be part of an aggregated \constraint{}, the \compiler{} will not rewrite the expression. +The \compiler{} will instead perform a search of its sub-expression to collect all other expressions to form an aggregated \constraint{}. +The \gls{rewriting} process continues by \gls{rewriting} this aggregated \constraint{}. \subsection{Delayed Rewriting}% \label{subsec:back-delayed-rew} -Adding \constraint{} \gls{propagation} during flattening means that the system becomes non-confluent, and some orders of execution may produce ``better'', \ie\ more compact or more efficient, \flatzinc{}. +Adding \gls{propagation} during \gls{rewriting} means that the system becomes non-confluent, and some orders of execution may produce ``better'', \ie{} more compact or more efficient, \flatzinc{}. \begin{example} - The following example is similar to code found in the \minizinc\ libraries of \gls{mip} solvers. + The following example is similar to code found in the \minizinc{} libraries of \gls{mip} \solvers{}. \begin{mzn} function var int: lq_zero_if_b(var int: x, var bool: b) = x <= ub(x)*(1-b); \end{mzn} - This predicate expresses the constraint \mzninline{b -> x<=0}, using a well-known method called ``big-M transformation''. - The expression \mzninline{ub(x)} returns a valid upper bound for \mzninline{x}, \ie\ a fixed value known to be greater than or equal to \mzninline{x}. - This could be the initial upper bound \mzninline{x} was declared with or the current value adjusted by the \minizinc\ compiler. - If \mzninline{b} takes the value 0, the expression \mzninline{ub(x)*(1-b)} is equal to \mzninline{ub(x)}, and the constraint \mzninline{x <= ub(x)} holds trivially. - If \mzninline{b} takes the value 1, \mzninline{ub(x)*(1-b)} is equal to 0, enforcing the constraint \mzninline{x <= 0}. + This predicate expresses the \constraint{} \mzninline{b -> x<=0}, using a well-known method called ``big-M transformation''. + The expression \mzninline{ub(x)} returns a valid upper bound for \mzninline{x}, \ie{} a fixed value known to be greater than or equal to \mzninline{x}. + This could be the initial upper bound \mzninline{x} was declared with or the current value adjusted by the \minizinc{} \compiler{}. + If \mzninline{b} takes the value 0, the expression \mzninline{ub(x)*(1-b)} is equal to \mzninline{ub(x)}, and the \constraint{} \mzninline{x <= ub(x)} holds trivially. + If \mzninline{b} takes the value 1, \mzninline{ub(x)*(1-b)} is equal to 0, enforcing the \constraint{} \mzninline{x <= 0}. \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 \glspl{domain} of the involved variables has 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 \emph{impose} new bounds on variables, so it is not always clear which order of evaluation is best. +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. +On the other hand, evaluating a predicate may also \emph{impose} new bounds on \variables{}, so it is not always clear which order of evaluation is best. -The same problem occurs with \glspl{reification} that are produced during flattening. -Other constraints could fix the domain of the reified \variable{} and make the \gls{reification} unnecessary. -Instead, the constraint (or its negation) can be flattened in root context. -This could avoid the use of a big decomposition or an expensive propagator. +The same problem occurs with \glspl{reification} that are produced during \gls{rewriting}. +Other \constraints{} could fix the \domain{} of the reified \variable{} and make the \gls{reification} unnecessary. +Instead, the \constraint{} (or its negation) can be flattened in \rootc{} context. +This could avoid the use of a big \gls{decomp} or an expensive \gls{propagator}. -To tackle this problem, the \minizinc\ compiler employs \gls{del-rew}. -When a linear \constraint{} is aggregated or a relational \gls{reification} \constraint{} is introduced it is not directly flattened. -Instead, these constraints are appended to the end of the current \gls{ast}. -All other not yet flattened constraints, that could change the relevant \glspl{domain}, will be flattened first. +To tackle this problem, the \minizinc{} \compiler{} employs \gls{del-rew}. +When a linear \constraint{} is aggregated or a relational \gls{reification} \constraint{} is introduced it is not immediately rewritten. +Instead, these \constraints{} are appended to the end of the current \gls{ast}. +All other \constraints{}, that are not yet rewritten and could change the relevant \domains{}, will be rewritten first. Note that this heuristic does not guarantee that \variables{} have their tightest possible \gls{domain}. -One delayed \constraint{} can still influence the \glspl{domain} of \variables{} used by other delayed \constraints{}. +One delayed \constraint{} can still influence the \domains{} of \variables{} used by other delayed \constraints{}. -Delaying the rewriting of constraints might, however, interfere with the \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. +Delaying the rewriting of constraints might also interfere with the \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 reified constraint turn out to be in terms of Boolean clauses as well, then this definition could have been aggregated as well. -Because the flattener does not revisit \gls{aggregation}, this does not happen. +The problem is, however, that if the definition of this \gls{reification} 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. \subsection{FlatZinc Optimisation}% \label{subsec:back-fzn-optimisation} -After the compiler is done flattening the \minizinc\ instance, it enters the optimisation phase. +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\ flattener might still understand the meaning of certain \constraints{}. -In these cases, \gls{propagation} methods, as discussed in \cref{subsec:back-cp}, can be used to eliminate values from variable \glspl{domain} and simplify \constraints{}. +Depending on this \solver{}, the \minizinc{} \compiler might still understand the meaning of certain \constraints{}. +In these cases, \gls{propagation} methods, as discussed in \cref{subsec:back-cp}, can be used to eliminate values from \domains{} and simplify \constraints{}. -In the current implementation the main focus of the flattener is to propagate Boolean \constraints{}. -The flattener tries to reduce the number of Boolean \variables{} and tries to reduce the number of literals in clauses and conjunctions. -The additional propagation might fix the result of the \gls{reification} of a constraint. -If this constraint is not yet rewritten, then the \solver{} will know to use a direct constraint instead of a reified version. +In the current implementation the main focus of the \compiler{} is to propagate Boolean \constraints{}. +The \compiler{} tries to reduce the number of Boolean \variables{} and tries to reduce the number of literals in clauses and conjunctions. +The additional \gls{propagation} might fix the result of the \gls{reification} of a \constraint{}. +If this \constraint{} is not yet rewritten, then the \solver{} will know to use a direct \constraint{} instead of a reified version. 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 \gls{propagation}. -Since they both have to take the same value, only a single \variable{} is required in the \flatzinc\ model 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. +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. 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 6a6646d..8a46718 100644 --- a/chapters/2_background_preamble.tex +++ b/chapters/2_background_preamble.tex @@ -15,7 +15,7 @@ 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 will 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 constraint modelling language used within this thesis. +\Cref{sec:back-minizinc} summarised the syntax and functionality of \minizinc{}, the leading \cml{} used within this thesis. In \cref{sec:back-solving} we discuss how \gls{cp}, \gls{mip}, and \gls{sat} can be used to solve a \gls{slv-mod}. \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}. diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex index 53bc07b..5ccad84 100644 --- a/chapters/3_rewriting.tex +++ b/chapters/3_rewriting.tex @@ -644,7 +644,7 @@ The resulting \nanozinc{} looks like this: constraint g_rel(b, x); \end{nzn} -The process of equality propagation is similar to \gls{unification} in logic programming \autocite{warren-1983-wam}. +The process of equality propagation is similar to unification in logic programming \autocite{warren-1983-wam}. However, since equations in \minizinc\ always concern scalar variables rather than terms, we can restrict ourselves to this simple substitution scheme and leave the further checking of the resulting equalities to the target \solver{}. \paragraph{Implementation} diff --git a/chapters/4_half_reif.tex b/chapters/4_half_reif.tex index 7c09607..3bb364a 100644 --- a/chapters/4_half_reif.tex +++ b/chapters/4_half_reif.tex @@ -535,7 +535,7 @@ The declaration item of a \variable{} does not further the context, and does not It merely triggers the creation of a new \variable{}. The (Item0) rule is triggered when there are no more inner items in the let-expression. -\subsection{Potentially \rootc{}}% +\subsection{Potentially Root}% \label{subsec:half-?root} In the previous section, we briefly discussed the context transformations for the (Access) and (ITE) rules in \cref{fig:half-analysis-expr}.