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

Initial rewriting adjustments to match background

Browse Source
This commit is contained in:
Jip J. Dekker 2021-06-26 17:45:04 +10:00
parent eb59f6771f
commit e05140062f
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
2 changed files with 26 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
chapters/2_background.tex
View File

@ -466,7 +466,7 @@ It is clear that when the value \mzninline{a} is known, then the value of \mznin
\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}.
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.
@ -1310,13 +1310,14 @@ Finally, if the stored expression was in reified context and the current context
So \gls{cse} needs to set \mzninline{b0} to \mzninline{true}.
\end{example}
\subsection{Adjusting Domain}%
\subsection{Constraint Propagation}%
\label{subsec:back-adjusting-dom}
As discussed in \cref{subsec:back-cp}, the \glspl{domain} of \variables{} can sometimes be directly changed because of the addition of a \constraint{}.
Similarly, depending on the \glspl{domain} of \variables{} some constraints can be proven \mzninline{true} or \mzninline{false}.
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.
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{}.
This principle also applies during the flattening of a \minizinc\ model.
The principles of \constraint{} propagation can also be applied during the flattening 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.
@ -1383,7 +1384,7 @@ The flattening process continues by flattening this aggregated constraint, which
\subsection{Delayed Rewriting}%
\label{subsec:back-delayed-rew}
Adjusting the \glspl{domain} of variables 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 \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{}.
\begin{example}
The following example is similar to code found in the \minizinc\ libraries of \gls{mip} solvers.

51
chapters/3_rewriting.tex
View File

@ -537,17 +537,15 @@ Since our prototype interpreter uses reference counting, it already accurately t
\subsection{Constraint Propagation}
Another way that variables can become unused is if a constraint can be detected to be true based on its semantics, and the known domains of the 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.
This, in turn, may result in \mzninline{x} or \mzninline{y} becoming unused and also removed (including their auxiliary definitions, if any).
\Gls{constraint} \gls{propagation} is another important technique used to simplify the produced \nanozinc{}.
It allows us to tighten the \glspl{domain} of \variables{} in the \nanozinc{} and remove \constraints{} proven to hold.
This, in turn, offers another way that variables can become unused.
This is a simple form of \gls{propagation}, the main inference method used in constraint solvers \autocite{schulte-2008-propagation}.
\gls{propagation}, in general, can not only detect when constraints are trivially true (or false), but also tighten variable domains.
When using \constraint{} \gls{propagation} for \nanozinc{} simplification, we do have to carefully consider its effects.
For instance, given the constraint \mzninline{x>y}, with initial domains \mzninline{x in 1..10, y in 1..10}, would result in the domains being tightened to \mzninline{x in 2..10, y in 1..9}.
Note, however, that this may now prevent us from removing \mzninline{x} or \mzninline{y}: even if they later become unused, the tightened domains may impose a constraint on their definition.
For instance, if \mzninline{x} is defined as \mzninline{abs(z)}, then any restriction on the domain of \mzninline{x} constrains the possible values of \mzninline{z} through the \mzninline{abs} function.
We therefore need to track whether a variable domain has been enforced through external constraints, or is the consequence of its own definition.
We omit the details of this mechanism for space reasons.
A further effect of \gls{propagation} is the replacement of constraints by simpler versions.
A constraint \mzninline{x=y+z}, where the domain of \mzninline{z} has been tightened to the singleton \mzninline{0..0}, can be rewritten to \mzninline{x=y}.
@ -598,36 +596,25 @@ Efficient \gls{propagation} engines ``wake up'' a constraint only when one of it
To enable this, the interpreter needs to keep a data structure linking variables to the constraints where they appear (in addition to the reverse links from calls to the variables in their arguments).
These links do not take part in the reference counting.
Together with its current \gls{domain}, each \variable{} in the interpreter also contains a Boolean flag.
This flag signifies whether the \gls{domain} of the \variable{} is an additional constraint.
When the flag is set, the \variable{} cannot be removed, even when the reference count is zero.
This happens when a \constraint{} that does not define the variable changes its \gls{domain}.
This \constraint{} might thereafter be removed, if it now proven to hold, but its effects will still be enforced.
If, however, any defining \constraint{} further tightens the \gls{domain}, then its constraint is no longer constraining.
The flag can then be unset and the variable can potentially be removed.
\subsection{Delayed Rewriting}
Adding \gls{propagation} and simplification into the rewriting system means that the system becomes non-confluent, and some orders of execution may produce ``better'', \ie\ more compact or more efficient, \nanozinc{}.
\begin{example}
The following example is similar to code found in the \minizinc\ libraries of 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 upper bound of the domain changed by \constraint{} \gls{propagation}.
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 MIP solvers, it is quite important to enforce \emph{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 all the \gls{propagation} has been performed, 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.
In our \microzinc/\nanozinc\ system, we allow predicates and functions to be \emph{annotated} as potential candidates for \emph{delayed rewriting}.
Any annotated constraint is handled by the (CallPrimitive) rule rather than the (Call) rule, which means that it is simply added as a call into the \nanozinc\ code, without evaluating its body.
When \gls{propagation} reaches a fix-point, all annotations are removed from the current \nanozinc\ program, and evaluation resumes with the predicate bodies.
If more information becomes available (though for example), a better decomposition of a call might become available.
It is therefore important to evaluate calls when all possible information is available to create efficient \nanozinc{}.
As a solution to this problem, in our \microzinc{}/\nanozinc{} system, we allow predicates and functions to be annotated as potential candidates for \gls{del-rew}.
Any annotated constraint is handled by the (CallPrimitive) rule rather than the (Call) rule, which means that it is simply added as a call into the \nanozinc{} code, without evaluating its body.
When \gls{propagation} reaches a fix-point, all annotations are removed from the current \nanozinc{} program, and evaluation resumes with the predicate bodies.
This crucial optimisation enables rewriting in multiple \emph{phases}.
For example, a model targeted at a MIP solver is rewritten into Boolean and reified constraints, whose definitions are annotated to be delayed.
The \nanozinc\ model can then be fully simplified by \gls{propagation}, before the Boolean and reified constraints are rewritten into lower-level linear primitives suitable for MIP\@.
For example, a model targeted at a \gls{mip} solver is rewritten into Boolean and reified constraints, whose definitions are annotated to be delayed.
The \nanozinc\ model can then be fully simplified by \gls{propagation}, before the Boolean and reified constraints are rewritten into lower-level linear primitives suitable for \gls{mip}.
\subsection{Common Sub-expression Elimination}\label{sec:4-cse}