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

Incorporate most of Guido's feedback on Background

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-22 21:57:28 +10:00
parent da2158ab87
commit c399924c89
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
12 changed files with 438 additions and 378 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
assets/bibliography/references.bib
View File

@ -258,26 +258,15 @@
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@manual{cplex-2020-cplex,
title = {V20.1: User’s Manual for CPLEX},
author = {CPLEX, IBM ILOG},
journal = {International Business Machines Corporation},
year = 2020,
}
@article{dantzig-1982-simplex,
author = {George B. Dantzig},
title = {Reminiscences about the origins of linear programming},
journal = {Oper. Res. Lett.},
volume = {1},
@article{dantzig-1955-simplex,
title = {The generalized simplex method for minimizing a linear form under
linear inequality restraints},
author = {Dantzig, George B and Orden, Alex and Wolfe, Philip and others},
journal = {Pacific Journal of Mathematics},
volume = {5},
number = {2},
pages = {43--48},
year = {1982},
url = {https://doi.org/10.1016/0167-6377(82)90043-8},
doi = {10.1016/0167-6377(82)90043-8},
timestamp = {Sun, 02 Jun 2019 20:50:37 +0200},
biburl = {https://dblp.org/rec/journals/orl/Dantzig82.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
pages = {183--195},
year = {1955},
}
@article{davis-1960-dpll,
@ -559,6 +548,20 @@
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@manual{ibm-2017-opl,
title = {OPL Language User’s Manual},
author = {CPLEX, IBM ILOG},
journal = {International Business Machines Corporation},
year = 2017,
}
@manual{ibm-2020-cplex,
title = {V20.1: User’s Manual for CPLEX},
author = {CPLEX, IBM ILOG},
journal = {International Business Machines Corporation},
year = 2020,
}
@inproceedings{ingmar-2020-diverse,
author = {Linnea Ingmar and Maria Garcia de la Banda and Peter J. Stuckey and
Guido Tack},
@ -822,6 +825,21 @@
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@article{miller-1960-subtour,
author = {C. E. Miller and A. W. Tucker and R. A. Zemlin},
title = {Integer Programming Formulation of Traveling Salesman Problems},
journal = {J. {ACM}},
volume = {7},
number = {4},
pages = {326--329},
year = {1960},
url = {https://doi.org/10.1145/321043.321046},
doi = {10.1145/321043.321046},
timestamp = {Wed, 14 Nov 2018 10:35:26 +0100},
biburl = {https://dblp.org/rec/journals/jacm/MillerTZ60.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
}
@software{minizinc-2021-minizinc,
author = {{MiniZinc Team}},
title = {MiniZinc: a free and open-source constraint modeling language},

61
assets/glossary.tex
View File

@ -21,10 +21,10 @@
\newglossaryentry{assignment}{
name={assignment},
description={
A mapping from \glspl{parameter} or \glspl{variable} to values.
An assignment is referred to as \gls{partial} when it maps only a subset of the \glspl{parameter} and \glspl{variable} of a \gls{model}.
A \gls{parameter-assignment} is an \gls{partial} \gls{assignment} that maps only the \glspl{parameter}, a \gls{variable-assignment} maps only the \glspl{variable}.
A complete \gls{parameter-assignment} maps all \glspl{parameter} of a \gls{model}, a complete \gls{variable-assignment} maps all \glspl{variable} of a \gls{model}
A mapping from \glspl{prb-par} or \glspl{variable} to values.
An assignment is referred to as \gls{partial} when it maps only a subset of the \glspl{prb-par} and \glspl{variable} of a \gls{model}.
A \gls{parameter-assignment} is an \gls{partial} \gls{assignment} that maps only the \glspl{prb-par}, a \gls{variable-assignment} maps only the \glspl{variable}.
A complete \gls{parameter-assignment} maps all \glspl{prb-par} of a \gls{model}, a complete \gls{variable-assignment} maps all \glspl{variable} of a \gls{model}
},
}
@ -45,7 +45,15 @@
\newglossaryentry{array}{
name={array},
description={A data structure that holds a collection of elements (\glspl{parameter} or \glspl{variable}), each identified by an index. Provided the index of an element, the array can retrieve the element},
description={A data structure that holds a collection of elements, each identified by an index. Provided the index of an element, the array can retrieve the element},
}
\newglossaryentry{avar}{
name={auxiliary variable},
description={
A \gls{variable} not explicitly defined in a \gls{model}, but rather introduced in the \gls{rewriting} of an \gls{instance}.
Auxiliary \glspl{variable} are generally introduced to redefine an existing \gls{variable} using \glspl{variable} of a different type, to represent an sub-expression, or to connect \glspl{constraint} in a \gls{decomp}
},
}
\newglossaryentry{backtrack}{
@ -118,7 +126,7 @@
name={constraint modelling language},
description={
A computer language used to define \glspl{model}.
Constraint modelling languages allow modellers to define \glspl{model} in terms of \glspl{parameter}, \gls{variable} and \glspl{constraint}.
Constraint modelling languages allow modellers to define \glspl{model} in terms of \glspl{prb-par}, \gls{variable} and \glspl{constraint}.
Together with a complete \gls{parameter-assignment} a \gls{model} forms an \gls{instance}.
Through the process of \gls{rewriting} the \gls{instance} is transformed into a \gls{slv-mod}, for which a \gls{solver} can find \glspl{sol}
},
@ -126,7 +134,7 @@
\newglossaryentry{cplex}{
name={CPLEX},
description={A well-known proprietary \gls{mip} \gls{solver} developed by IBM \autocite{cplex-2020-cplex}},
description={A well-known proprietary \gls{mip} \gls{solver} developed by IBM \autocite{ibm-2020-cplex}},
}
\newglossaryentry{gls-chr}{
@ -161,7 +169,7 @@
\newglossaryentry{cvar}{
name={control variable},
description={
A special form of an \gls{ivar} where the \gls{variable} represent the result of a \gls{reif}
A special form of an \gls{avar} where the \gls{variable} represent the result of a \gls{reif}
},
}
@ -266,17 +274,10 @@
}
\newglossaryentry{half-reified}{
name={half reified},
name={half-reified},
description={See \gls{half-reif}},
}
\newglossaryentry{ivar}{
name={introduced variable},
description={
A \gls{variable} that was created in the reformulation of a \gls{decomp}.
New \gls{variable} are introduced either to redefine an existing \gls{variable} using a different type or to connect newly introduced \glspl{constraint}
},
}
\newglossaryentry{incremental-rewriting}{
name={incremental-rewriting},
@ -362,8 +363,8 @@
description={
A formalisation of a \gls{dec-prb} or an \gls{opt-prb}.
It is defined in terms of formalised decision, \glspl{variable} of different kinds (\eg{} Boolean, integers, or even sets), and \glspl{constraint}, Boolean logic formulas which are forced to hold in any \gls{sol}, and, in case of an \gls{opt-prb}, an \gls{objective}.
Any external data required to formulate the \glspl{constraint} is said to be the \glspl{parameter}.
The combination of a constraint model and \gls{assignment}s for its \glspl{parameter} is said to be an \gls{instance} of the constraint model
Any external data required to formulate the \glspl{constraint} is said to be the \glspl{prb-par}.
The combination of a constraint model and \gls{assignment}s for its \glspl{prb-par} is said to be an \gls{instance} of the constraint model
},
}
@ -384,7 +385,7 @@
\newglossaryentry{gls-mip}{
name={mixed integer programming},
description={
A solving technique tries to find the \gls{opt-sol} for a \cmodel{} containing a mixture of Integer and floating point \glspl{variable} subject to \glspl{constraint} in the form of linear equations.
A solving technique tries to find the \gls{opt-sol} for a \cmodel{} containing a mixture of Integer and floating point \glspl{variable} subject to \glspl{constraint} in the form of linear (in-)equations.
Mixed integer programming is extensively studied and there are many successful \glspl{solver} dedicated to solving mixed integer programs.
See \cref{subsec:back-mip}
},
@ -437,7 +438,7 @@
\newglossaryentry{optional}{
name={optional},
description={When it is not certain if a value, either \gls{variable} or \gls{parameter}, will exist in a \gls{minizinc} model, its type is marked as optional (\mzninline{opt}). If the value does not occur it is said to be absent.},
description={When it is not certain if a value, either \gls{variable} or \gls{parameter}, will exist in a \gls{minizinc} \instance{}, its type is marked as optional (\mzninline{opt}). If the value does not occur it is said to be absent.},
}
\newglossaryentry{opt-sol}{
@ -517,11 +518,11 @@
}
\newglossaryentry{parameter}{
name={problem parameter},
name={parameter},
description={
Problem parameters are part of the external input for a \gls{model}.
They can be used as immutable data used to define \glspl{constraint} or provide structural information about an \gls{instance}.
For example, a problem parameter can influence the number of \glspl{constraint} in an \gls{instance}
Parameter variables, shortened to parameters, are variables in the sense of programming languages, and are not to be confused with \glspl{variable}.
In \minizinc{}, a parameter variable represents a value that will be known during \gls{rewriting}.
Examples of such values are \glspl{prb-par}, the result of introspection (such as \mzninline{dom(x)}, returning the current domain of a \gls{variable} \mzninline{x}), or the result of calculations over other parameter variables.
},
}
@ -532,9 +533,19 @@
\newglossaryentry{partial}{
name={partial},
description={A function is said to be partial when it does not have a defined result for every possible input. Similarly, an \gls{assignment} is said to be partial when it maps only a subset of the \glspl{parameter} and \glspl{variable} in a \gls{model}.},
description={A function is said to be partial when it does not have a defined result for every possible input. Similarly, an \gls{assignment} is said to be partial when it maps only a subset of the \glspl{prb-par} and \glspl{variable} in a \gls{model}.},
}
\newglossaryentry{prb-par}{
name={problem parameter},
description={
Problem parameters are part of the external input for a \gls{model}.
They can be used as immutable data used to define \glspl{constraint} or provide structural information about an \gls{instance}.
For example, a problem parameter can influence the number of \glspl{constraint} in an \gls{instance}
},
}
\newglossaryentry{propagation}{
name={constraint propagation},
description={The removal of values from \glspl{domain} of \glspl{variable} that violate a \gls{constraint}. See \cref{subsec:back-cp}},

2
assets/listing/back_sgp.mzn
View File

@ -4,7 +4,7 @@ include "globals.mzn";
1..infinity: ngroups;
1..infinity: size;
enum: golfers = anon_enum(ngroups * size);
enum golfers = anon_enum(ngroups * size);
set of int: groups = 1..g;
set of int: Rounds = 1..w;

11
assets/listing/back_tsp.mod
View File

@ -4,15 +4,12 @@ param cost {Paths} >= 0;@\Vlabel{line:back:ampl:parend}@
var Take {Paths} binary;@\Vlabel{line:back:ampl:var}@
param n := card {Cities};@\Vlabel{line:back:ampl:compstart}@
set SubSets := 0 .. (2**n - 1);
set PowerSet {k in SubSets} := {i in Cities: (k div 2**(ord(i)-1)) mod 2 = 1};@\Vlabel{line:back:ampl:compend}@
minimize TotalCost: sum {(i,j) in Paths} cost[i,j] * Take[i,j];@\Vlabel{line:back:ampl:goal}@
subj to Tour {i in S}:@\Vlabel{line:back:ampl:con1}@
sum {(i,j) in Paths} Take[i,j] + sum {(j,i) in Paths} Take[j,i] = 2;
subj to SubtourElimation {k in SubSet diff {0,2**n-1}}:@\Vlabel{line:back:ampl:con2}@
sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (i,j) in Paths} X[i,j] +
sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (j,i) in Paths} X[j,i] >= 2;
var Order {Cities} >= 1, <= card(Cities);@\Vlabel{line:back:ampl:compstart}@
let Order[first(Cities)] = 1;
subj to SubtourElimation {(i,j) in Cities: ord(i) < ord(j)}:
(Order[i] - Order[j] + card(Cities)*Take[i,j]) <= (card(Cities) - 1);@\Vlabel{line:back:ampl:compend}@

2
assets/shorthands.tex
View File

@ -26,6 +26,8 @@
\newcommand*{\cmodel}{\gls{model}\xspace}
\newcommand*{\cmodels}[0]{\glspl{model}\xspace}
\newcommand*{\nanozinc}{\gls{nanozinc}\xspace}
\newcommand*{\prbpar}{\gls{prb-par}\xspace}
\newcommand*{\prbpars}{\glspl{prb-par}\xspace}
\newcommand*{\parameters}{\glspl{parameter}\xspace}
\newcommand*{\parameter}{\gls{parameter}\xspace}
\newcommand*{\reified}{\gls{reified}\xspace}

14
chapters/1_introduction.tex
View File

@ -30,8 +30,8 @@ Two \solvers{} designed to solve the same problem class can perform very differe
\Cmls{} have been designed to tackle these issues.
They serve as a level of abstraction between the user and the \solver{}.
Instead of providing a flat list of \variables{} and \constraints{}, the user can create a \cmodel{} using the more natural syntax of the \cml{}.
A \cmodel{} can generally describe a class of problems through the use of \parameters{}, values assigned by external input.
Once given a complete \gls{assignment} of the \parameters{}, the \cmodel{} forms an \instance{}.
A \cmodel{} can generally describe a class of problems through the use of \prbpars{}, values assigned by external input.
Once given a complete \gls{assignment} of the \prbpars{}, the \cmodel{} forms an \instance{}.
The \instance{} is transformed into a \gls{slv-mod} through a process class \gls{rewriting}.
A commonly used \cml{} is \glsxtrshort{ampl} \autocite{fourer-2003-ampl}.
@ -56,7 +56,7 @@ As an \gls{opt-prb}, our goal is to find a schedule that minimises the finishing
\end{listing}
\Cref{lst:intro-open-shop} shows an \glsxtrshort{ampl} model for the open shop problem.
In order of occurence, \lrefrange{line:intro:param:start}{line:intro:param:end} show the declarations of the \parameters{}.
In order of occurence, \lrefrange{line:intro:param:start}{line:intro:param:end} show the declarations of the \prbpars{}.
To create an \instance{} of the problem, the user provides the number of jobs and machines that are considered, and the duration of each task.
\Lrefrange{line:intro:var:start}{line:intro:var:end} show the \variable{} declarations: for each task we decide on its start time.
Additionally, we declare the end time of the last task as a \variable{}, to ease the modelling of the problem.
@ -108,7 +108,7 @@ As such, a \gls{clp} program is not \solver{}-independent.
Like \glsxtrshort{ampl}, it is a \solver{}-independent \cml{}.
And like \gls{clp} languages, modellers can declare common concepts and control the encoding into the \gls{slv-mod}.
The latter is accomplished through the use of function definitions.
For example, a user could create the following \minizinc{} function to express the non-overlapping relationship.
For example, a user could create the following \minizinc{} function to express the non-overlapping relation.
\begin{mzn}
function var bool: non_overlap(
@ -173,7 +173,7 @@ In particular:
\begin{itemize}
\item The \minizinc{} \compiler{} is inefficient.
\item The existing implementation of \minizinc{} is inefficient.
It does a surprisingly large amount of work for each expression (especially resolving sub-typing and overloading), which may be repeated many times.
And as models generated for low-level \solver{} technologies can be quite large, the resulting \gls{rewriting} procedure can be intolerably slow.
As the model transformations implemented in \minizinc{} become more sophisticated, these performance problems are simply magnified.
@ -236,7 +236,7 @@ Overall, this thesis makes the following contributions:
\item It presents a design and implementation of techniques to automatically introduce \gls{half-reif} of \constraints{} in \minizinc{}.
\item It develops a technique to simplify problem specifications by efficiently eliminating implication chains.
\item It develops a technique to simplify \glspl{slv-mod} by efficiently eliminating \glspl{implication-chain}.
\item It proposes two novel methods to reduce the overhead of using \cmls{} in incremental techniques: \gls{rbmo} and the \gls{incremental-rewriting} of changing \instances{}.
@ -251,7 +251,7 @@ First, it introduces the reader to \minizinc{}, how its models are formulated, a
Then, we review different solving methods such as \gls{sat}, \gls{mip}, and \gls{cp}.
This is followed by a comparison of \minizinc{} with other \cmls{}.
This chapter also reviews techniques that are closely related to \cmls{}.
We conclude this chapter with a description of the current \minizinc{} compiler and the techniques it uses to simplify the \solver{} specifications it produces.
We conclude this chapter with a description of the current \minizinc{} compiler and the techniques it uses to simplify the \glspl{slv-mod} it produces.
\emph{\Cref{ch:rewriting}} presents a formal execution model for \minizinc{} and the core of our new architecture.
We construct a set of formal rewriting rules for a subset of \minizinc{} called \microzinc{}.

638
chapters/2_background.tex
View File

File diff suppressed because it is too large Load Diff

8
chapters/2_background_preamble.tex
View File

@ -1,4 +1,4 @@
This research presented in this thesis investigates the process of \gls{rewriting} \cmls{} to address both the lack of information about this process and to improve this process to meet its modern day requirements.
The research presented in this thesis investigates the process of \gls{rewriting} \cmls{}.
This chapter provides the required background information to understand \cmls{}:
\begin{itemize}
@ -15,8 +15,8 @@ Finally, the chapter analyses the existing approach to \gls{rewriting} \minizinc
The overview of \cmls{} presented in this chapter supports the research and discussion presented in subsequent chapters.
In the remainder of this chapter we first, in \cref{sec:back-intro} introduce the reader to \cmls{} and their purpose.
\Cref{sec:back-minizinc} summarised the syntax and functionality of \minizinc{}, the leading \cml{} used within this thesis.
\Cref{sec:back-minizinc} summarises the syntax and functionality of \minizinc{}, the \cml{} used within this thesis.
In \cref{sec:back-solving} we discuss how \gls{cp}, \gls{mip}, and \gls{sat} are used to solve a \gls{slv-mod}.
\Cref{sec:back-other-languages} introduces alternative \cmls{} and compares their functionality to \minizinc{}.
Then, \cref{sec:back-term} survey the closely related technologies in the field of \glspl{trs}.
Finally, \cref{sec:back-mzn-interpreter} explores the process that the current \minizinc{} \interpreter{} uses to translate a \minizinc{} \instance{} into a \gls{slv-mod}.
Then, \cref{sec:back-term} surveys the closely related technologies in the field of \glspl{trs}.
Finally, \cref{sec:back-mzn-interpreter} explores the process that the existing \minizinc{} implementation uses to translate a \minizinc{} \instance{} into a \gls{slv-mod}.

16
chapters/3_rewriting.tex
View File

@ -53,7 +53,7 @@ This section introduces the two sub-languages of \minizinc{} at the core of the
\microzinc{} is a simple language used to define transformations to be performed by the \interpreter{}.
It is simplified subset of \minizinc{}.
The transformation are represented in the language through the use of function definitions.
A function of type \mzninline{var bool}, describing a relationship, can be defined as a \gls{native} \constraint{}.
A function of type \mzninline{var bool}, describing a relation, can be defined as a \gls{native} \constraint{}.
Otherwise, a function body must be provided for \gls{rewriting}.
The function body can use a restriction of the \minizinc{} expression language.
@ -72,7 +72,7 @@ The core of the syntax of \microzinc{} is defined in \cref{fig:rew-uzn-syntax}.
In \microzinc{} it is specifically used to mark functions that are \gls{native} to the target \solver{}.
We have omitted the definitions of \syntax{<mzn-type-inst>} and \syntax{<ident>}, which can be assumed to be the same as the definition of \syntax{<type-inst>} and \syntax{<ident>} in the \minizinc{} grammar, see \cref{ch:minizinc-grammar}.
While we omit the typing rules here for space reasons, we will assume that in well-typed \microzinc{} programs conditions of expressions are \parameters{}.
This means that the where conditions \syntax{<exp>} in \glspl{comprehension}, the conditions \syntax{<exp>} in if-then-else expressions, and the \syntax{<literal>} index in \gls{array} accesses must have \mzninline{par} type.
This means that the where conditions \syntax{<exp>} in \glspl{comprehension}, the conditions \syntax{<exp>} in \gls{conditional} expressions, and the \syntax{<literal>} index in \gls{array} accesses must have \mzninline{par} type.
In \minizinc{} the use of \variables{} in these positions is allowed and these expressions are rewritten to function calls.
We will discuss how the same transformation takes place in when translating \minizinc{} to \microzinc{}.
@ -284,7 +284,7 @@ In order to track these dependencies, \nanozinc{} attaches \constraints{} that d
A \nanozinc{} program (\cref{fig:rew-nzn-syntax}) consists of a topologically-ordered list of declarations of \variables{} and \constraints{}.
\Variables{} are declared with an identifier, a domain, and are associated with a list of attached \constraints{}.
\Constraints{} can also occur at the top-level of the \nanozinc{} program.
These are said to be the ``root-context'' \constraints{} of the \cmodel{}, \ie{} those that have to hold globally and are not just used to define an \gls{ivar}.
These are said to be the ``root-context'' \constraints{} of the \cmodel{}, \ie{} those that have to hold globally and are not just used to define an \gls{avar}.
Only root-context \constraints{} can effectively constrain the overall problem.
\Constraints{} attached to \variables{} originate from function calls, and since all functions are guaranteed to be total, attached \constraints{} can only define the function result.
@ -350,7 +350,7 @@ The rule evaluates the function body \(\ptinline{E}\) where the formal parameter
The (CallBuiltin) rule applies to ``built-in'' functions that can be evaluated directly, such as arithmetic and Boolean operations on fixed values.
The rule simply returns the result of evaluating the built-in function on the evaluated parameter values.
The (CallNative) rule applies to calls to \mzninline{var bool} functions, that describe relationships, that have been marked as \constraints{} \gls{native} to the \solver{}.
The (CallNative) rule applies to calls to \mzninline{var bool} functions, that describe relations, that have been marked as \constraints{} \gls{native} to the \solver{}.
Since these are directly supported by the \solver{}, they simply need to be transferred into the \nanozinc{} program.
\begin{figure*}[p]
@ -555,9 +555,9 @@ The \constraints{} directly succeeding the declaration prepended by \texttt{↳}
\end{example}
It is important to notice the difference between \constraints{} that appear at the top level and \constraints{} that appear as part of the attached \constraints{} of a \variable{}.
Top-level \constraints{} help define the problem, they are globally enforced and cannot be removed from the problem unless it can be proved that its relationships are already enforced.
Top-level \constraints{} help define the problem, they are globally enforced and cannot be removed from the problem unless it can be proved that its relations are already enforced.
\Constraints{} attached to a \variable{}, on the other hand, are used to define a \variable{}.
\Constraints{} are generally attached when they stem from a functional relationship, like \mzninline{abs(x)} in the example, or from a \gls{reif}, like \mzninline{abs(x) > y} when used in the disjunction with \mzninline{c}.
\Constraints{} are generally attached when they stem from a functional relation, like \mzninline{abs(x)} in the example, or from a \gls{reif}, like \mzninline{abs(x) > y} when used in the disjunction with \mzninline{c}.
In this thesis we will follow the same naming standard as \minizinc{}, where a \gls{reif} of a \constraint{} has the same name as the original \constraint{} with \texttt{\_reif} appended.
\begin{example}
@ -752,12 +752,12 @@ This allows us to disable the \gls{cse} when it is guaranteed to be unnecessary.
\label{subsec:rew-aggregation}
In our new system it is still possible to support \gls{aggregation}.
We aggregate \constraints{} by combining \constraints{} connected through attached \constraints{}, eliminating the need for \glspl{ivar} to which they are attached.
We aggregate \constraints{} by combining \constraints{} connected through attached \constraints{}, eliminating the need for \gls{avar} to which they are attached.
To aggregate a certain kind of \constraint{}, it is marked as a \gls{native} \constraint{}.
These functional definitions are kept in the \nanozinc{} program until a top-level \constraint{} is posted that uses the \variables{} to which they are attached.
Once this happens, the interpreter will employ dedicated \gls{aggregation} logic to visit the attached \constraints{} and combine them.
The top-level \gls{constraint} is then replaced by the combined \gls{constraint}.
When the \glspl{ivar} become unused, they will be removed using the normal mechanisms.
When the \gls{avar} become unused, they will be removed using the normal mechanisms.
\begin{example} For example, let us reconsider the linear \constraint{} from \cref{ex:back-agg}: \mzninline{x + 2*y <= z}.
The constraint will result in the following \nanozinc{}.

2
chapters/4_half_reif.tex
View File

@ -728,7 +728,7 @@ In the case where a \variable{} has one incoming edge, but it is marked as used
When using full \gls{reif}, all \glspl{reif} are stored in the \gls{cse} table.
This ensure that if the same expression is \gls{reified} twice, then the resulting \gls{reif} will be reused.
This avoids that the solver has to enforce the same functional relationship twice.
This avoids that the solver has to enforce the same functional relation twice.
If the \gls{rewriting} uses \gls{half-reif}, in addition to full \gls{reif}, then \gls{cse} needs to ensure not just that the expressions are equivalent, but also that the context of the two expressions are compatible.
For example, if an expression was first found in a \posc{} context and later found in a \mixc{} context, then the resulting \gls{half-reif} from the first cannot be used for the second expression.

2
chapters/6_conclusions.tex
View File

@ -36,7 +36,7 @@ Crucially, the architecture is easily extended with well-known simplification te
\item \Gls{cse} is used to detect any duplicate calls.
We describe how it can be employed both during the compilation from \minizinc{} to \microzinc{}, and in the evaluation of \microzinc{}.
\item When it is beneficial, the architecture can utilize \gls{aggregation} to combine certain \constraints{} and eliminate \glspl{ivar}.
\item When it is beneficial, the architecture can utilize \gls{aggregation} to combine certain \constraints{} and eliminate \gls{avar}.
\item Finally, \constraints{} can be marked for \gls{del-rew}.
This implores to \microzinc{} \interpreter{} to delay the \gls{rewriting} of a certain call until all possible information is available.

2
chapters/A2_benchmark.tex
View File

@ -141,7 +141,7 @@ In this thesis we use four different versions of the \gls{gecode} solver:
\end{itemize}
\paragraph{IBM CPLEX} is a proprietary \gls{mip} \solver{} \autocite{cplex-2020-cplex}.
\paragraph{IBM CPLEX} is a proprietary \gls{mip} \solver{} \autocite{ibm-2020-cplex}.
In this thesis we use \gls{cplex} version 20.1 under an academic license in our experiments.
\paragraph{OpenWBO} is a open source \gls{maxsat} \solver{} \autocite{martins-2014-openwbo}.