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

Grammar pass over Half Reification

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-25 10:24:42 +10:00
parent e3a864effe
commit 31770d0c98
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
2 changed files with 45 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

68
chapters/4_half_reif.tex
View File

@ -92,21 +92,21 @@ Since Boolean expressions in \minizinc{} can be used in, for example, integer ex
\end{example}
To systematically analyse whether Boolean expressions can be \gls{half-reified}, we study the \emph{monotonicity} of \constraints{} \wrt{} an expression.
A relation \( r( a_{n}, \ldots{}, a_{i}, \ldots{} , a_{m}) \) is said to be \emph{monotone} with regards to its argument \(a_{i}\) when given two possible values for \(a_{i}\), \(x\) and \(y\), if \(x > y\), then \(r( a_{n}, \ldots{}, x, \ldots{} , a_{m}) \geq{} r( a_{n}, \ldots{}, y, \ldots{} , a_{m})\), independent of other arguments.
Contrariwise, a relation \( r( a_{n}, \ldots{}, a_{i}, \ldots{} , a_{m}) \) is said to be \emph{antitone} with regards to its argument \(a_{i}\) if given two possible values for \(a_{i}\), \(x\) and \(y\), if \(x > y\), then \(r( a_{n}, \ldots{}, x, \ldots{} , a_{m}) \leq{} r( a_{n}, \ldots{}, y, \ldots{} , a_{m}) \), independent of the other arguments.
A relation \( r( a_{n}, \ldots{}, a_{i}, \ldots{} , a_{m}) \) is said to be \emph{monotone} \wrt{} its argument \(a_{i}\) when given two possible values for \(a_{i}\), \(x\) and \(y\), if \(x > y\), then \(r( a_{n}, \ldots{}, x, \ldots{} , a_{m}) \geq{} r( a_{n}, \ldots{}, y, \ldots{} , a_{m})\), independent of other arguments.
Contrariwise, a relation \( r( a_{n}, \ldots{}, a_{i}, \ldots{} , a_{m}) \) is said to be \emph{antitone} \wrt{} its argument \(a_{i}\) if given two possible values for \(a_{i}\), \(x\) and \(y\), if \(x > y\), then \(r( a_{n}, \ldots{}, x, \ldots{} , a_{m}) \leq{} r( a_{n}, \ldots{}, y, \ldots{} , a_{m}) \), independent of the other arguments.
Where, for clarification, we assume \( \text{false} < \text{true} \).
Using these definitions, we introduce extra distinctions in the context of expressions.
Before, we would merely distinguish between \rootc{} context and non-\rootc{} context.
Now, we will categorise the latter into the following three contexts.
Now, we will categorize the latter into the following three contexts.
\begin{description}
\item[\posc{}] An expression is in \posc{} context when its enclosing \constraint{} (in \rootc{} context) is \textbf{monotone} \wrt{} the expression.
\item[\posc{}] An expression is in \posc{} context when the enclosing \constraint{} (in \rootc{} context) is \textbf{monotone} \wrt{} the expression.
\item[\negc{}] An expression is in \negc{} context when its enclosing \constraint{} (in \rootc{} context) is \textbf{antitone} \wrt{} the expression.
\item[\negc{}] An expression is in \negc{} context when the enclosing \constraint{} (in \rootc{} context) is \textbf{antitone} \wrt{} the expression.
\item[\mixc{}] An expression is in \mixc{} context when its enclosing \constraint{} (in \rootc{} context) it is \textbf{neither} monotone, nor antitone \wrt{} the expression.
\item[\mixc{}] An expression is in \mixc{} context when the enclosing \constraint{} (in \rootc{} context) it is \textbf{neither} monotone, nor antitone \wrt{} the expression.
\end{description}
@ -202,13 +202,13 @@ Instead, this process can be implicit.
The \gls{propagator} merely prunes the \glspl{domain} of the \variables{}.
When a \gls{domain} is found to be empty, then the \gls{propagator} declares the current state \gls{unsat}.
It is not possible to construct the \gls{half-reified} \gls{propagator} from such an implicit \(check\) operation.
Instead a new explicit \(check\) method has to be devised to implement the \gls{propagator} of the \gls{half-reif} \constraint{}.
Instead, a new explicit \(check\) method has to be devised to implement the \gls{propagator} of the \gls{half-reif} \constraint{}.
In comparison, a \gls{propagator} for the \gls{reif} of \(c\) cannot be created from these three logical task.
In addition, we require the logical task from a \gls{propagator} of \(\neg{} c\): \(checkNeg\), \(pruneNeg\), and \(entailedNeg\).
Using these additional functions, we can define an algorithm for the \gls{propagator}, shown in \cref{alg:reif-prop}
Although this might seem reasonable for small \constraints{}, such as integer equality, for many \glspl{global} their negation is hard to define.
\todo{insert good example of global constraint.}
\todo{Insert good example of global constraint.}
\begin{algorithm}[t]
@ -246,7 +246,7 @@ When a full \gls{reif} is required, we can still use \gls{half-reified} \glspl{p
A full \gls{reif} \mzninline{x <-> pred(...)} can be propagated using its \gls{half-reified} \gls{propagator}, \mzninline{x -> pred(...)}, the \gls{half-reified} \gls{propagator} of its negation, \mzninline{y -> not pred(...)}, and the \constraint{} \mzninline{x <-> not y}.
This does not lose \gls{propagation} strength.
For Booleans appearing in \posc{} context we can make the \gls{propagator} of the negated \gls{half-reif} run at the lowest priority, since it will never detect if the state is \gls{unsat}.
Similarly in \negc{} context we can make the propagator \mzninline{b -> pred(...)} run at the lowest priority.
Similarly, in \negc{} context we can make the propagator \mzninline{b -> pred(...)} run at the lowest priority.
This means that the \glspl{cvar} are still fixed at the same time, but there is less overhead.
In \cref{sec:half-experiments} we assess the implementation of \glspl{propagator} for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element} based on these principles.
@ -264,7 +264,7 @@ If, however, a \gls{reif} is replaced by a \gls{half-reif}, then only one of the
\begin{example}
Consider the \gls{reif} of the \constraint{} \mzninline{i <= 4} using the \gls{cvar} \mzninline{b}, where \mzninline{i} can take values in the domain \mzninline{0..10}.
If the target \solver{} is a \gls{mip} \solver{}, then this \gls{reif} would be linearised.
If the target \solver{} is a \gls{mip} \solver{}, then this \gls{reif} would be linearized.
It would take the following form.
\begin{mzn}
@ -318,7 +318,7 @@ Expressions bound to an identifier can be used multiple times in expressions tha
If \mzninline{x} is only used in a \posc{} context, then the call itself is in a \posc{} context as well.
As such, the call could then be \gls{half-reified}.
Although this is the case in the left side of the conjunction, the other side uses \mzninline{x} in a \negc{} context.
Although this is the case on the left side of the conjunction, the other side uses \mzninline{x} in a \negc{} context.
This means that \mzninline{pred(a, b, c)} is in a \mixc{} context and must be fully \gls{reified}.
\end{example}
@ -329,7 +329,7 @@ In this scenario, we prefer to create the full \gls{reif} as it decreases the nu
When taking into account the possible undefinedness of an expression, every expression in a \minizinc{} model has two different contexts: the context in which the expression itself occurs, its \emph{value context}, and the context in which the partiality of the expression is captured, its \emph{partiality context}.
As described in \cref{subsec:back-mzn-partial}, \minizinc{} uses \glspl{rel-sem} for partial functions.
This means that if a function if the result of a function is undefined, then its nearest enclosing Boolean expression becomes false.
This means that if the result of a function is undefined, then its nearest enclosing Boolean expression becomes false.
In practice, this means that a condition that tests if the function will return a value is added to the nearest enclosing Boolean expression.
The partiality context is the context in which this condition is placed.
@ -342,7 +342,7 @@ The partiality context is the context in which this condition is placed.
\end{mzn}
In this fragment, we study the context of the division expression \mzninline{y div x}.
The expression itself return a integer \variable{} and it used on the left-hand side of a less than \constraint{}.
The expression itself return an integer \variable{}, and it used on the left-hand side of a less than \constraint{}.
This result is therefore in a \negc{} context: it is only forced to take a smaller value.
This is its value context.
@ -467,7 +467,7 @@ However, we currently do not provide such analysis and annotate functions by han
\end{listing}
\begin{algorithm}
\KwIn{A \minizinc\ operator \(op\) and calling context \(ctx\)}
\KwIn{A \minizinc{} operator \(op\) and calling context \(ctx\)}
\KwOut{A tuple containing the contexts of the arguments \(\tuple{ctx_{1}, \ldots{}, ctx_{n}}\)}
@ -582,12 +582,12 @@ Since all expressions in well-formed \microzinc{} are total, the \constraint{} c
And, unlike \minizinc{}, the \constraint{} is not dependent on the context of the \gls{let}.
The \constraint{}'s expression is evaluated in \rootc{} context.
The (Assign) rule reasons about declarations that have a right hand side.
The (Assign) rule reasons about declarations that have a right-hand side.
The expression that is assigned to the identifier must be evaluated in the combined context of its usages.
As previously discussed, the contexts in which the identifier was used can be retrieved using the ``collectCtx'' function.
These contexts are then combined using a ``join'' function.
This function repeatedly applies the symmetric join operation described by \cref{fig:half-join}.
The right hand expression of the item is then evaluated in the resulting context.
The right-hand expression of the item is then evaluated in the resulting context.
\begin{figure*}
\begin{center}
@ -696,7 +696,7 @@ Otherwise, it will act as a normal \rootc{} context.
\Cref{fig:half-analysis-maybe-root} shows the additional inference rules for \gls{array} access and \gls{conditional} expressions.
Looking back at \cref{ex:half-maybe-root}, these additional rules and updated join operation will ensure that the first case will correctly use \rootc{} context calls.
For the second case, however, it detects that \mzninline{p} is used in both \posc{} and \mayberootc{} context.
Therefore, it will output the \posc{} call for the right hand side of \mzninline{p}, even when \mzninline{b} evaluates to \mzninline{true}.
Therefore, it will output the \posc{} call for the right-hand side of \mzninline{p}, even when \mzninline{b} evaluates to \mzninline{true}.
At compile time, this is the only correct context to use.
We will, however, discuss how to adjust contexts dynamically during \gls{rewriting} in \cref{subsec:half-dyn-context}.
@ -754,13 +754,13 @@ During the \gls{rewriting} process the contexts assigned to the different expres
\end{example}
As this example shows, the use of \gls{half-reif} can form so called \glspl{implication-chain}.
This happens when the right hand side of an implication is \gls{half-reified} and a \gls{cvar} is created to represent the expression.
Instead, we could have used the left hand side of the implication as the \gls{cvar} of the \gls{half-reified} \constraint{}.
As this example shows, the use of \gls{half-reif} can form so-called \glspl{implication-chain}.
This happens when the right-hand side of an implication is \gls{half-reified} and a \gls{cvar} is created to represent the expression.
Instead, we could have used the left-hand side of the implication as the \gls{cvar} of the \gls{half-reified} \constraint{}.
In next section, we present a new post-processing method we call \gls{chain-compression}.
It can be used to eliminate these \glspl{implication-chain}.
The \gls{rewriting} with \gls{half-reif} also interacts with some of the optimisation methods used during the \gls{rewriting} process.
The \gls{rewriting} with \gls{half-reif} also interacts with some simplification methods used during the \gls{rewriting} process.
Most importantly, \gls{half-reif} has to be considered when using \gls{cse}, and \gls{propagation} can change the context of an expression.
In \cref{subsec:half-cse} we will discuss how \gls{cse} can be adjusted to handle \gls{half-reif}.
Finally, in \cref{subsec:half-dyn-context} we will discuss how the context in which an expression is evaluated can be adjusted during the \gls{rewriting} process.
@ -770,7 +770,7 @@ Finally, in \cref{subsec:half-dyn-context} we will discuss how the context in wh
\Gls{rewriting} with \gls{half-reif} will in many cases result in \glspl{implication-chain}: \mzninline{b1 -> b2 /\ b2 -> c}, where \texttt{b2} has no other occurrences.
In this case the conjunction can be replaced by \mzninline{b1 -> c} and \texttt{b2} can be removed from the \cmodel{}.
The case shown in the example can be generalised to
The case shown in the example can be generalized to
\begin{mzn}
constraint b1 -> b2 /\ forall(i in N)(b2 -> c[i])
@ -896,7 +896,7 @@ Since a \constraint{} and its negation cannot both hold at the same time, this i
\label{subsec:half-dyn-context}
In \cref{subsec:half-?root} we discussed the fact that the correct context of an expression is not always known when analysing \microzinc{}.
The context may depends on data that is only known at an \instance{} level.
The context may depend on data that is only known at an \instance{} level.
The same situation can be caused by \gls{propagation}.
\begin{example}
@ -962,13 +962,13 @@ A description of the used computational environment, \minizinc{} instances, and
\label{sec:half-exp-prop}
Our first experiment considers the QCP-max quasi-group completion problem.
In this problem, we need to decide the value of an \((n \times n)\) matrix of integer \variables{}, with \domains{} \mzninline{1..n}.
In this problem, we need to decide the value of a \((n \times n)\) matrix of integer \variables{}, with \domains{} \mzninline{1..n}.
The aim of the problem is to create as many rows and columns as possible where all \variables{} take a unique value.
In each \instance{} certain values have already been fixed.
It is not always possible for all rows and columns to contain only distinct values.
In \minizinc{} counting the number of rows/columns with all different values can be accomplished using a \gls{reified} \mzninline{all_different} \constraint{}.
Since the goal of the problem is to maximise the number of \mzninline{all_different} \constraints{} that hold, these \constraints{} are never forced to be \mzninline{false}.
Since the goal of the problem is to maximize the number of \mzninline{all_different} \constraints{} that hold, these \constraints{} are never forced to be \mzninline{false}.
This means these \constraints{} are in \posc{} context and can be \gls{half-reified}.
\Cref{tab:half-qcp} shows the comparison of two solving configurations in \gls{chuffed} for the QCP-max problem.
@ -980,7 +980,7 @@ This \gls{propagator} is an adjusted version from the existing \gls{bounds-con}
The implementation of the \gls{propagator} was already split into parts that check the violation of the \constraint{} and parts that prune the \glspl{domain} of the \variables{}.
Therefore, the transformation described in \cref{sec:half-propagation} can be directly applied.
Since \gls{chuffed} is a \gls{lcg} \solver{}, the explanations created by the \gls{propagator} have to be adjusted as well.
These adjustments happen in a similar fashion to the adjustments of the general algorithm: explanations used for the violation\glsadd{violated} of the \constraint{} can now be used to set the \gls{cvar} to \mzninline{false}, and the explanations given to prune a \variable{} are extended with a literal that ensures the \gls{cvar} is \mzninline{true}.
These adjustments happen similar to the adjustments of the general algorithm: explanations used for the violation\glsadd{violated} of the \constraint{} can now be used to set the \gls{cvar} to \mzninline{false}, and the explanations given to prune a \variable{} are extended with a literal that ensures the \gls{cvar} is \mzninline{true}.
In our second configuration the \mzninline{all_different} \constraint{} is enforced using the \gls{decomp} shown in \cref{lst:half-alldiff}.
The \mzninline{!=} \constraints{} produced by this redefinition are \gls{reified}.
@ -1001,14 +1001,14 @@ Their conjunction then represent the \gls{reif} of the \mzninline{all_different}
\end{center}
\end{table}
The results in \cref{tab:half-qcp} show that the specialised \gls{propagator} has a significant advantage over the use of the \gls{decomp}.
The results in \cref{tab:half-qcp} show that the specialized \gls{propagator} has a significant advantage over the use of the \gls{decomp}.
Although it only allows us to solve one extra instance, there is a significant reduction in solving time for most \instances{}.
Note that the qcp-15 \instances{} are the only exception.
It appears that none of the \instances{} in this group proved to be a real challenge to either method and we see similar solve times between the two methods.
It appears that none of the \instances{} in this group proved to be a real challenge to either method, and we see similar solve times between the two methods.
In addition, we consider a variation on the prize collecting travelling salesman problem \autocite{balas-1989-pctsp} referred to as the ``prize collecting path'' problem.
In the problem we are given a graph with weighted edges, both positive and negative.
The aim of the problem is to find the optimal acyclic path from a given start node that maximises the weights on the path.
The aim of the problem is to find the optimal acyclic path from a given start node that maximizes the weights on the path.
It is not required to visit every node.
In this experiment we can show how \gls{half-reif} can reduce the overhead of handling partial functions correctly.
@ -1016,7 +1016,7 @@ The \minizinc{} model for this problem contains an \gls{array} lookup \mzninline
We compare safe \gls{decomp} of this \mzninline{element} \constraint{} against a \gls{propagator} of its \gls{half-reif}.
The \gls{decomp} creates a new \variable{} that takes the value of the index only when it is within the index set of the \gls{array}.
Otherwise, it will set its surrounding context to \mzninline{false}.
The \gls{half-reif} implicitly performs the same task by setting its \gls{cvar} to \mzninline{false} whenever the resulting \variable{} does not not equal the element to which the index \variable{} points, or when the index points outside the \gls{array}.
The \gls{half-reif} implicitly performs the same task by setting its \gls{cvar} to \mzninline{false} whenever the resulting \variable{} does not equal the element to which the index \variable{} points, or when the index points outside the \gls{array}.
Again, for the implementation of the \gls{propagator} of the \gls{half-reif} \constraint{} we adjust the direct \gls{propagator} as described above.
\begin{table}
@ -1076,7 +1076,7 @@ The \gls{rewriting} statistics for the \gls{gecode} \solver{} library, shown in
Although the total number of \constraints{} remains stable, we see that well over half of all \glspl{reif} are replaced by \glspl{half-reif}.
This replacement happens mostly 1-for-1; the difference between the number of \glspl{half-reif} introduced and the number of \glspl{reif} reduced is only 20. In comparison, the number of implications removed by \gls{chain-compression} looks small, but this number is highly dependent on the \minizinc{} model.
In many models, no implications can be removed, but for some problems an implication is removed for every \gls{half-reif} that is introduced.
Finally, the overhead of the introduction of \gls{half-reif} and the newly introduced optimisation techniques is minimal.
Finally, the overhead of the introduction of \gls{half-reif} and the newly introduced optimization techniques is minimal.
The \Cref{subtab:half-flat-lin} paints an equally positive picture of \glspl{half-reif} for linearization.
Since both \glspl{reif} and \glspl{half-reif} are decomposed during the \gls{rewriting} process, \gls{half-reif} is able to remove almost 7.5\% of the overall \constraints{}.
@ -1084,7 +1084,7 @@ The ratio of \glspl{reif} that is replaced with \glspl{half-reif} is not as high
This is caused by the fact that the linearization process requires full \gls{reif} in the decomposition of many \glspl{global}.
Similar to \gls{gecode}, the number of implications that is removed is dependent on the problem.
Lastly, the \gls{rewriting} time slightly increases for the linearization process.
Since there are many more \constraints{}, the introduced optimisation mechanisms have a slightly higher overhead.
Since there are many more \constraints{}, the introduced optimization mechanisms have a slightly higher overhead.
Finally, statistics for \gls{rewriting} the \instances{} for a \gls{maxsat} \solver{} are shown in \cref{subtab:half-flat-bool}.
Unlike linearization, \gls{half-reif} does not significantly reduce the number of \constraints{} and, although still significant, the number of \glspl{reif} is reduced by only slightly over ten percent.
@ -1094,7 +1094,7 @@ Even when we do not automatically introduce \glspl{half-reif}, they are still in
Furthermore, \gls{chain-compression} does not seem to have any effect.
Since all \glspl{half-reif} are defined in terms of clauses, the implications normally removed using \gls{chain-compression} are instead aggregated into bigger clauses.
Surprisingly, \gls{half-reif} slightly reduces the \gls{rewriting} time as it reduces the workload.
The relatively small changes shown might indicate that additional work might be warranted in the Booleanisation library.
The relatively small changes shown might indicate that additional work might be warranted in the \gls{booleanization} library.
It might be possible to create more dedicated \glspl{decomp} for \gls{half-reified} \constraints{}, and to analyse the library to see if \glspl{annotation} could be added to more function arguments to retain \posc{} contexts.
\begin{table}
@ -1117,7 +1117,7 @@ It might be possible to create more dedicated \glspl{decomp} for \gls{half-reifi
The results shown in this table are very mixed.
For \gls{gecode}, \gls{half-reif} does not seem to impact its solving performance.
We would have hoped that \glspl{propagators} for \glspl{half-reif} would be more efficient and reduce the number of \glspl{propagator} scheduled in general.
However, neither number of \instances{} solved, nor the solving time required improved.
However, neither number of \instances{} solved, nor the required solving time improved.
A single \instance{}, however, is negatively impacted by the change; an \gls{opt-sol} for this \instance{} is no longer found.
We expect that this \instance{} has benefited from the increased Boolean \gls{propagation} that is caused by full \gls{reif}.
Overall, these results do not show any significant positive or negative effects in \gls{gecode}'s performance when using \gls{half-reif}.

10
chapters/4_half_reif_preamble.tex
View File

@ -2,20 +2,20 @@
\minizinc{} allows us to write complex \constraints{} that in the process of \gls{rewriting} result in multiple \constraints{} that reason about each other.
However, using a \gls{reif} \(b \leftrightarrow{} c\), that determines whether a \constraint{} \(c\) holds, can slow the \solver{} down.
Even in \gls{cp} \solvers{}, not many \glspl{reif} are \gls{native} to the \solvers{}, and the \glspl{propagator}, for the ones that are, are often weak.
Generally, the \glspl{decomp} of \gls{reified} \constraint{} also result a large number of \gls{native} \constraints{} and \variables{}.
Generally, the \glspl{decomp} of \gls{reified} \constraint{} also result numerous \gls{native} \constraints{} and \variables{}.
It is thus important that \gls{rewriting} avoids the use of \gls{reif}, whenever it is not required.
In this chapter we present an extended \gls{reif} analysis to help minimise the required \solver{} effort.
In this chapter we present an extended \gls{reif} analysis to help minimize the required \solver{} effort.
Not only does it consider if a \constraint{} must be \gls{reified} or not, but it also considers whether it could instead be \gls{half-reified}.
The notion of \gls{half-reif} \(b \rightarrow{} c\) for a \constraint{} \(c\) was introduced by \textcite{feydy-2011-half-reif}.
It is shown \gls{half-reif} can mitigate some of the problems and expenses of the use of \gls{reif}.
It is shown \gls{half-reif} can mitigate some problems and expenses of the use of \gls{reif}.
It is not always possible, however, to use a \gls{half-reif} instead of a \gls{reif}.
The authors identify the conditions required for its usage and provide an algorithm that rewrites a subset of the \minizinc{} language using the technique.
Crucially, because of the omission of \gls{let} and multiple occurrences of identifiers, this algorithm does not directly generalise to the full \minizinc{} language.
Crucially, because of the omission of \gls{let} and multiple occurrences of identifiers, this algorithm does not directly generalize to the full \minizinc{} language.
This chapter re-evaluates \gls{half-reif} and extends the \gls{rewriting} process to fully support \gls{half-reif} in \minizinc{}.
This chapter is organised as follows.
This chapter is organized as follows.
In \cref{sec:half-intro,sec:half-propagation} we introduce the core concepts of \gls{half-reif} and \glspl{propagator} for \gls{half-reified} \constraints{}, as discussed by \textcite{feydy-2011-half-reif}.
An additional benefit of \gls{half-reif} is that its \gls{decomp} can be significantly smaller than the \gls{decomp} of a \gls{reif}.
\Cref{sec:half-decomposition} shows the benefits of \gls{half-reif} when writing \glspl{decomp} for \gls{mip} and \gls{sat} \solvers{}.