Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Incorporate Background feedback from Peter

Browse Source
This commit is contained in:
Jip J. Dekker 2021-05-24 14:41:37 +10:00
parent b5ff72e95f
commit 3687260209
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
3 changed files with 934 additions and 904 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
assets/acronyms.tex
View File

@ -45,7 +45,7 @@
\newacronym[see={[Glossary:]{gls-mip}}]{mip}{MIP\glsadd{gls-mip}}{Mixed Integer
Programming}
\newacronym{np-comp}{NP-complete}{Nondeterministic Polynomial-time complete}
\newacronym{np}{NP}{Nondeterministic Polynomial-time}
\newacronym[see={[Glossary:]{gls-opl}}]{opl}{OPL\glsadd{gls-opl}}{The
Optimisation Programming Language}

1531
assets/bibliography/references.bib
View File

File diff suppressed because it is too large Load Diff

305
chapters/2_background.tex
View File

@ -29,10 +29,10 @@ 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\).
Although a constraint model does not contain any instructions 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.
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}
@ -178,16 +178,17 @@ format. In \minizinc\ 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 Mariott et al.\ offer a detailed discussion of the
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\)@ =
@\(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\). 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.
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\). 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.
The main types used in \minizinc\ are Boolean, integer, floating point numbers,
sets of integers, and (user-defined) enumerated types. These types can be used
@ -206,16 +207,14 @@ type expression. These expressions constrain a declaration, not just to a
certain type, but also to a set of value. 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
two declarations declare two integer \variables{} that can take the values from
three to five and one, three, and five respectively.
\begin{mzn}
var 3..5: x;
var {1,3,5}: y;
\end{mzn}
declare two integer \variables{} that can take the values from three to five and
one, three, and five respectively.
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
@ -235,7 +234,9 @@ 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;}.
the value of a \variable{}, \mzninline{solve maximize x;}. 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.}
@ -261,7 +262,7 @@ 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 function is
should be declared within an expression body. Any call to such a function is
directly placed in the flattened model.
\subsection{MiniZinc Expressions}%
@ -273,10 +274,7 @@ 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}. Nethercote et al.\ and
Mariott et al.\ offer a detailed discussion of the expression language of
\minizinc\ and its predecessor \zinc\ respectively
\autocite*{nethercote-2007-minizinc,marriott-2008-zinc}.
can be found in \cref{sec:mzn-grammar-expressions}.
\Glspl{global} are the basic building blocks in the \minizinc\ language. These
expressions capture common (complex) relations between \variables{}.
@ -340,7 +338,7 @@ 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 b >= 0 then a > b else b < a endif;
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
@ -373,7 +371,7 @@ 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 as being an \mzninline{element} function. Otherwise, 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.
@ -394,11 +392,11 @@ parts:
when the filtering condition succeeds.
\end{description}
The following example composes an \gls{array} that contains the doubled even
The following example composes an \gls{array} that contains the tripled even
values of an \gls{array} \mzninline{x}.
\begin{mzn}
[ xi * 2 | xi in x where x mod 2 == 0]
[ 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
@ -418,32 +416,32 @@ resulting definition. 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
%
\begin{mzn}
constraint let { var int: tmp = x div 2; } in tmp mod 2 == 0 \/ tmp = 0;
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 zero.
%
constrains that half of \mzninline{x} is even or one.
\item To introduce a scoped \variable{}. For example, the constraint
%
\begin{mzn}
let {var -2..2: slack;} in x + slack = y;
constraint let {var -2..2: slack;} in x + slack = y;
\end{mzn}
%
constrains that \mzninline{x} and \mzninline{y} are at most two apart.
\item To constrain the resulting expression. For example, the following
function
%
\begin{mzn}
function var int: int_times(var int: x, var int: y) =
let {
let {
var int: z;
constraint pred_int_times(x, y, z);
} 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}.
@ -486,14 +484,17 @@ corresponding constraint \mzninline{c(...)} holds.
reified variables it can set to \mzninline{true}.
\end{example}
We say that the same expression can be used in \emph{root context} as well as in
a \emph{reified context}. 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 \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.
\subsection{Handling Undefined Expressions}%
\label{subsec:back-mzn-partial}
Some expressions in the \cmls\ do not always have a well-defined result.
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.
\begin{example}\label{ex:back-undef}
Consider, for example, the following ``complex constraint''
@ -512,8 +513,7 @@ Some expressions in the \cmls\ do not always have a well-defined result.
the constraint should be trivially true.
\end{example}
Part of the semantics of a \cmls{} is the choice as to how to treat these
partial functions. Examples of such expressions in \minizinc\ are:
Other examples of \minizinc{} expressions that result in partial functions are:
\begin{itemize}
\item Division (or modulus) when the divisor is zero:
@ -522,12 +522,6 @@ partial functions. Examples of such expressions in \minizinc\ are:
x div 0 = @??@
\end{mzn}
\item Array access when the index is outside the given index set:
\begin{mzn}
array1d(1..3, [1,2,3])[0] = @??@
\end{mzn}
\item Finding the minimum or maximum or an empty set:
\begin{mzn}
@ -595,8 +589,7 @@ For example, one might deal with a zero divisor using a disjunction:
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. \jip{TODO:\@ This also corresponds to Kleene semantics, maybe I
should use a different example}
semantics.
Frisch and Stuckey also show that different \solvers{} often employ different
semantics \autocite*{frisch-2009-undefinedness}. It is therefore important that,
@ -642,7 +635,7 @@ targets and their input language.
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} all \variables{}. It will not surprise the
every value in the \gls{domain} of all \variables{}. It will not surprise the
reader that this is an inefficient approach. Given, for example, the constraint
\begin{mzn}
@ -650,22 +643,22 @@ reader that this is an inefficient approach. 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. \gls{cp} is the idea solving \glspl{csp} by
\mzninline{b} can be deduced. \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 and eliminate any
depth first search. At each node, the \solver{} will try to eliminate any
impossible value using a process called \gls{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 the any values that are proven to be
\gls{propagator} will analyse and prune any values that are proven to be
inconsistent.
In the best case scenario, \gls{propagation} will eliminate all impossible value
and all \variables{} have been fixed to a single value. In this case we have
arrived at a solution. Often, \gls{propagation} alone will not be enough to find
a solution to the problem. Instead, when no more \glspl{propagator} are
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. Often, \gls{propagation} alone will not be enough to
find a solution to the problem. Instead, when no more \glspl{propagator} are
triggered (we have reached a \gls{fixpoint}), the \solver{} 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
@ -673,12 +666,12 @@ solution. If no solution is found using the search decision, then it needs to
try making the opposite decision: excluding the chosen value or adding the
opposite constraint.
Note that the important difference between values \gls{propagation} and making
search decisions is that value excluded by a \gls{propagator} are guaranteed to
not occur in any solution, but values excluded by a search heuristic are merely
removed locally and might still be part of a solution. A \gls{cp} \solver{} is
only able to prove that the problem is unsatisfiable by exploring the full
search space.
Note that the important difference between values excluded by \gls{propagation}
and making search decisions is that value excluded by a \gls{propagator} are
guaranteed to not occur in any solution, but values excluded by a search
heuristic are merely removed locally and might still be part of a solution. A
\gls{cp} \solver{} is only able to prove that the problem is unsatisfiable by
exploring the full search space.
\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
@ -718,17 +711,19 @@ constraints otherwise.
\begin{mzn}
int: n;
array [1..n] of var 1..n: q;
set of int: ROW = 1..n;
set of int: COL = 1..n;
array [ROW] of var COL: q;
constraint all_different(q);
constraint all_different([q[i] + i | i in 1..n]);
constraint all_different([q[i] - i | i in 1..n]);
constraint all_different([q[i] + i | i in ROW]);
constraint all_different([q[i] - i | i in ROW]);
\end{mzn}
Since we know that there can only be one queen per column, the decision in the
model left to make is, for every queen, where in the column 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
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.
This model can be directly used in most \gls{cp} \solvers{}, since integer
\variables{} and an \mzninline{all_different} \gls{propagator} are common.
@ -753,8 +748,8 @@ 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, an easy task and
might require high complexity. Instead, it can sometimes be better to use a
algorithm that reaches this level of consistency is, however, not an easy task
and might require high 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}.
@ -762,10 +757,11 @@ might take less time than achieving \gls{domain-con}.
This is, for example, the case for integer linear constraints:
\[ \sum_{i} c_{i} x_{i} = d\] where \(c_{i}\) and \(d\) are integer
\parameters{} and \(x_{i}\) are integer \variable{}. For these constraints, no
realistic \gls{domain-con} \gls{propagator} exists. 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.
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}. The
@ -782,8 +778,8 @@ better solutions than the current incumbent solution.
\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 method
to solve \minizinc\ instances.
OR-Tools \autocite{perron-2021-ortools} have long been one of the leading
methods to solve \minizinc\ instances.
\subsection{Mathematical Programming}%
\label{subsec:back-mip}
@ -794,14 +790,14 @@ 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. In general, a linear
program can be expressed in the form:
%
\begin{align*}
\text{maximise} \hspace{2em} & \sum_{j=1}^{V} c_{j} x_{j} & \\
\text{subject to} \hspace{2em} & l_{i} \leq \sum_{j=0}^{V} a_{ij} x_{j} \leq u_{i} & \forall_{i=1}^{C} \\
& x_{i} \in \mathbb{R} & \forall_{i=1}^{V}
\end{align*}
where \(V\) and \(C\) represent the number of variables and number of
%
\noindent{}where \(V\) and \(C\) represent the number of variables and number of
constraints respectively. The vector \(c\) holds the coefficients of the
objective function and the matrix \(a\) holds the coefficients for the
constraints. The vectors \(l\) and \(u\) respectively contain the lower and
@ -809,10 +805,13 @@ 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. The most prominent method, the simplex method, can
find the optimal solution of a linear program in polynomial time.
to find the optimal solution. 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.
The same method provides the foundation for a harder problem. In \gls{lp} our
These methods provide the foundation for a harder problem. In \gls{lp} our
variables must be continuous. If we require that one or more take a discrete
value (\(x_{i} \in \mathbb{N}\)), then the problem suddenly becomes much harder.
The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all}
@ -845,15 +844,15 @@ Over the years \gls{lp} and \gls{mip} \solvers{} have developed immensely.
often worthwhile to encode problem as a mixed integer program to find a
solution.
\glspl{csp} can be often be encoded as mixed integer programs. This does,
however, come with its challenges. Most \constraints{} in a \minizinc\ model are
not linear equations. The translation of a single \constraint{} can introduce
many linear \constraints{} and even new \variables{}. For example, when a
\constraint{} reasons about the value that a variable will take, 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}\).
To solve a \gls{csp}, it can be encoded as a mixed integer program. This
does, however, come with its challenges. Most \constraints{} in a \minizinc\
model are not linear equations. The translation of a single \constraint{} can
introduce many linear \constraints{} and even new \variables{}. For example,
when a \constraint{} reasons about the value that a variable will take, 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}\).
\begin{example}
Let us again consider the N-Queens problem from \cref{ex:back-nqueens}. The
@ -878,7 +877,7 @@ linear \constraints{} using the \variables{} \(y_{i}\).
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
row. Finally, \cref{line:back-mip-diag1,line:back-mip-diag2} constrain all
column. Finally, \cref{line:back-mip-diag1,line:back-mip-diag2} constrain all
diagonals to contain only one queen.
\end{example}
@ -887,26 +886,26 @@ linear \constraints{} using the \variables{} \(y_{i}\).
\glsreset{sat}
\glsreset{maxsat}
\gls{sat} was the first problem to be proven to be \gls{np-comp}
\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.
There is a field of research dedicated to solving \gls{sat} problems. 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\). 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.
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\). 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.
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
\autocite{biere-2021-sat}. 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.
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.
Many real world problems modelled in \cmls\ directly correspond to \gls{sat}.
However, even problems that contain \variables{} with types other than Boolean
@ -932,7 +931,7 @@ efficient way to solve the problem.
The encoding of the problem uses a Boolean \variable{} for every position of
the chess board. 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 column of the chess board.
placed on every row of the chess board.
\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
@ -1147,8 +1146,8 @@ the solver. Take, for example, the following \gls{opl} search definition:
This search strategy will ensure that we first try and find a solution where the
\variable{} \mzninline{x} takes a value smaller than \mzninline{y}, if it does
not find a solution, then it will try finding a solution where the oposite is
true. This search specification, like many other imaginable, cannot be enforce
not find a solution, then it will try finding a solution where the opposite is
true. This search specification, like many others imaginable, cannot be enforced
using \minizinc\ \gls{search-heuristic} \glspl{annotation}.
To support \gls{opl}'s dedicated search language, the language is tightly
@ -1175,7 +1174,7 @@ variable types that are contained in \minizinc{}, \gls{essence} also contains:
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. These types in \gls{essence} are restricted to Boolean,
finite types. The base types in \gls{essence} are restricted to Boolean,
enumerated types, or a restricted set of integers.
\begin{example}
@ -1246,15 +1245,17 @@ the targeted solver.
\label{sec:back-term}
\glsreset{trs}
At the heart of the flattening process lies a \gls{trs}. A \gls{trs}
\autocite{baader-1998-term-rewriting} 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}\). 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
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}. 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.
\begin{example}
@ -1323,9 +1324,10 @@ symbol might be replaced or equated with a constant symbol, but, different from
\cmls{}, this is not a requirement. A variable can remain a name in the solution
of a constraint logic program. This means that the solution of a constraint
logic program can be a relationship between different variables. In cases where
an instantiated solution is required, a special \mzninline{labeling} constraint
can be used to force a variable to take a constant value. Similarly, there is a
\mzninline{minimize} that can be used to find the optimal value for a variable.
an instantiated solution is required, a special \mzninline{labeling}
\constraint{} can be used to force a variable to take a constant value.
Similarly, there is a \mzninline{minimize} \constraint{} that can be used to
find the optimal value for a variable.
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
@ -1534,17 +1536,17 @@ happens in one of two ways:
\begin{itemize}
\item For Boolean expressions in a reified context, the new \variable{} is
\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 a new reified constraint. This
constraint contains a call a variation of the call that would have been
generated for the expression in root 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. For example, the constraint in
\minizinc{}
\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. 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. For example, the constraint
in \minizinc{}
\begin{mzn}
constraint b \/ this_call(x, y);
@ -1763,9 +1765,8 @@ they directly received the equivalent linear \constraint{}:
constraint int_lin_le([1,2,-1], [x,y,z], 0)
\end{mzn}
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 intermediate values that have to be given a value in the solution.
This can be resolved using the \gls{aggregation} of constraints. When we
aggregate constraints we collect multiple \minizinc\ expressions, that would
@ -1840,22 +1841,24 @@ the \glspl{domain} of \variables{} used by other delayed \constraints{}.
\label{subsec:back-fzn-optimisation}
After the compiler is done flattening the \minizinc\ instance, it enters the
optimisation phase. This phase occurs at the same stage as the solver input
language. Depending on the targeted \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
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{}.
In the current implementation the main focus of the flattener is to propagate
Boolean constraint. The flattener try and reduce the number of Boolean variables
and try and reduce the number of literals in clauses or logical and constraints.
The additional propagation might fix the 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.
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.
Even more important than the Boolean constraints, are equality \constraints{}.
The flattening is in the unique position to \gls{unify} \variables{} when they
are found to be equal. 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 the two \variables{} are unified.
Even more important than the Boolean \constraints{}, are equality
\constraints{}. The flattening is in the unique position to \gls{unify}
\variables{} when they are found to be equal. 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 the two \variables{} are
unified. Once initialised, it is not always possible for \solvers{} to
\gls{unify} \variables{} internally.