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

Incorporate Guido's feedback on the Conclusions

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-23 16:16:19 +10:00
parent 7a7069dcc4
commit 88d1fb41af
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
1 changed files with 49 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

94
chapters/6_conclusions.tex
View File

@ -5,24 +5,24 @@
\noindent{}\Gls{rewriting} in \cmls{}, such as \minizinc{}, makes it easier to express \glspl{dec-prb}. \noindent{}\Gls{rewriting} in \cmls{}, such as \minizinc{}, makes it easier to express \glspl{dec-prb}.
They allow the modeller to reason at a high-level when specifying the problem. They allow the modeller to reason at a high-level when specifying the problem.
\Gls{rewriting} is then able to create a model for a range of potential \solvers{}. \Gls{rewriting} is then able to create a model for a range of potential \solvers{}.
Although the importance of creating \gls{slv-mod} that can be solved efficiently is well-known, changes in the usage of these languages are raising questions about the time required to perform this transformation. Although the importance of creating \glspl{slv-mod} that can be solved efficiently is well-known, changes in the usage of these languages are raising questions about the time required to perform this transformation.
First, \constraint{} models are now often solved using low-level \solvers{}, such as \gls{mip} and \gls{sat}. First, \constraint{} models are now often solved using low-level \solvers{}, such as \gls{mip} and \gls{sat}.
\Glspl{slv-mod} for these \solvers{} are more sizable and the process to reach them is more complex. \Glspl{slv-mod} for these \solvers{} are more sizeable and the process to translate a high-level \cmodel{} into the low-level format required by these \solvers{} is complex.
Second, we have seen a development of the use of \gls{meta-optimisation}. Second, we have seen a development of the use of \gls{meta-optimisation}.
\Gls{meta-optimisation} is often implemented by incrementally adjusting \instances{}, after which it has to be rewritten to be solved. \Gls{meta-optimisation} is often implemented by incrementally adjusting \instances{}, after which those \instances{} have to be rewritten to be solved.
Both these methods put additional pressure on the \gls{rewriting} process, which can often be a bottle-neck in the overall process. Both these methods put additional pressure on the \gls{rewriting} process, which can often be a bottleneck in the overall process.
In the previous chapters of this thesis, we have explored in detail and presented improvements to the process of \gls{rewriting} \instances{} of \cmodels{} into \glspl{slv-mod}. In this thesis, we have explored in detail and presented improvements to the process of \gls{rewriting} \instances{} of \cmodels{} into \glspl{slv-mod}.
These improvements focus on the performance of the \gls{rewriting} process in general, the quality of the produce \glspl{slv-mod}, and the incremental usage of \cmls{}. These improvements focus on the performance of the \gls{rewriting} process in general, the quality of the produced \glspl{slv-mod}, and the incremental usage of \cmls{}.
This chapter presents the conclusions of this thesis. This chapter presents the conclusions of this thesis.
We present a summary of the research and its contributions and discuss the future work arising from them. We present a summary of the research and its contributions and discuss the future work arising from them.
\paragraph{Rewriting Architecture} In \cref{ch:rewriting}, we presented the principle contribution of this thesis: \textbf{an architectural design for the rewriting of a \cml{}}. \paragraph{Rewriting Architecture} In \cref{ch:rewriting}, we presented the principle contribution of this thesis: \textbf{an architectural design for the rewriting of a \cml{}}.
We introduced a transformation language \microzinc{}, a minimal describe to describe how an \instance{} is transformed into a \gls{slv-mod}. We introduced a transformation language \microzinc{}, a minimal language used to describe how different expressions are rewritten into a \gls{slv-mod}.
At the core of this architecture lie formal rewriting rules for the \microzinc{} against which an implementation can be checked. At the core of this architecture lie formal rewriting rules for \microzinc{} against which an implementation can be checked.
The transformation required for a complex \cml{}, such as \minizinc{}, can be reduced to \microzinc{} and as such enjoy the same guarantees.
The architecture operates on \nanozinc{}, a language that expresses (partial) \gls{slv-mod}. The \gls{rewriting} process of a \minizinc{} \instance{} into a \gls{slv-mod} then consists of two steps: the translation of \minizinc{} model transformations into \microzinc{}, implemented by a \compiler{}; and the iterative \gls{rewriting} using these \microzinc{} transformations to arrive at a \gls{slv-mod}, implemented using an \interpreter{}.
The latter operates on (partial) \glspl{slv-mod}, expressed using the \nanozinc{} language.
Distinctively, \nanozinc{} has the ability to attach \constraints{} to a \variable{}. Distinctively, \nanozinc{} has the ability to attach \constraints{} to a \variable{}.
During \gls{rewriting} \constraints{} introduced to define a \variable{} are attached to it. During \gls{rewriting} \constraints{} introduced to define a \variable{} are attached to it.
This ensures that if it is discovered that a \variable{} is no longer required (\ie{} it is no longer referred to by any \constraints{}), it can correctly be removed. This ensures that if it is discovered that a \variable{} is no longer required (\ie{} it is no longer referred to by any \constraints{}), it can correctly be removed.
@ -31,7 +31,7 @@ Crucially, the architecture is easily extended with well-known simplification te
\begin{itemize} \begin{itemize}
\item \Gls{propagation} can actively simplify the both \constraints{} and the \glspl{domain} of \variables{} in \glspl{slv-mod}. \item \Gls{propagation} can actively simplify both \constraints{} and the \glspl{domain} of \variables{} in \glspl{slv-mod}.
\item \Gls{cse} is used to detect any duplicate calls. \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{}. We describe how it can be employed both during the compilation from \minizinc{} to \microzinc{}, and in the evaluation of \microzinc{}.
@ -39,7 +39,7 @@ Crucially, the architecture is easily extended with well-known simplification te
\item When it is beneficial, the architecture can utilize \gls{aggregation} to combine certain \constraints{} and eliminate \gls{avar}. \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}. \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. This suggests to the \microzinc{} \interpreter{} to delay the \gls{rewriting} of a certain call until all possible information is available.
\end{itemize} \end{itemize}
@ -50,42 +50,45 @@ Two prototype programs were developed to evaluate this architecture:
\item and a \microzinc{} \gls{byte-code} \interpreter{} that produces a \nanozinc{} \gls{slv-mod}. \item and a \microzinc{} \gls{byte-code} \interpreter{} that produces a \nanozinc{} \gls{slv-mod}.
\end{itemize} \end{itemize}
Even though the implementation of these prototypes lacks the maturity of the existing \minizinc{} compiler, the performance of the design of the architecture shines through in the performance tests. The implementation of these prototypes lacks the maturity of the existing \minizinc{} \compiler{}.
However, the performance of these prototypes already surpasses the existing implementation, averaging a more than ten times speed-up.
This architecture enables many avenues of further research. This architecture enables many avenues of further research.
For one, the formal rewriting rules presented open up possibilities to more extended formal reasoning about \cmls{}. For one, the formal rewriting rules presented open up possibilities to more extended formal reasoning about \cmls{}.
This could potentially lead to the ability to proof certain properties of the \gls{rewriting} process. This could potentially lead to the ability to prove certain properties of the \gls{rewriting} process.
Additionally, the architecture introduces reasoning about the transition from \minizinc{} \instances{} to \gls{slv-mod} as two different levels: the transition from \minizinc{} to \microzinc{} and the evaluation of the \nanozinc{} program to create a \gls{slv-mod}. Additionally, the architecture introduces reasoning about the transition from \minizinc{} \instances{} to \gls{slv-mod} as two different levels: the transition from \minizinc{} to \microzinc{} and the evaluation of the \nanozinc{} program to create a \gls{slv-mod}.
In our prototype we have presented techniques to help improve the quality of the \gls{slv-mod}, but many improvements to these techniques and other techniques may be possible. In our prototype we have presented techniques to help improve the quality of the \gls{slv-mod}, but many improvements to these techniques and other techniques may be possible.
Finally, we use \nanozinc{} to track \constraints{} that are introduced to define a \variable{}. Finally, we use \nanozinc{} to track \constraints{} that are introduced to define a \variable{}.
Although we have showed how this helps when a \variable{} becomes unused, we have yet to discover its uses within the \solvers{} themselves. Although we have showed how this helps when a \variable{} becomes unused, we not yet investigated if the same information might help improve \solver{} performance.
In \gls{cp} \solvers, for example, it is no longer has to required propagate defining \constraints{} once their \variable{} has been fixed (under certain circumstances). A possible example of where this information can be useful is found in \gls{cp} \solvers{}.
In these \solvers{}, a functionally defined \variable{} can become unused when the \constraints{} that use \variable{} have already been \gls{satisfied}, independent of its \gls{fixed} value.
Like we can remove the defining \constraint{} during \gls{rewriting}, in a \gls{cp} \solver{} we could stop further \gls{propagation} of this \constraint{} and possibly speed up the solving.
\paragraph{Reasoning about Reification} Whether to a \constraint{} is \gls{reified} is a crucial decision that has to be made during \gls{rewriting}. \paragraph{Reasoning about Reification} Whether to a \constraint{} is \gls{reified} is a crucial decision that has to be made during \gls{rewriting}.
Making the wrong decision can significantly impact \gls{solver} performance. Making the wrong decision can significantly impact \gls{solver} performance.
In \cref{ch:half-reif}, we extend our architecture with our secondary contribution: \textbf{a formal analysis to reason about the \gls{reif} of \constraints{}}. In \cref{ch:half-reif}, we extend our architecture with our second contribution: \textbf{a formal analysis to reason about the \gls{reif} of \constraints{}}.
Not only does this analysis reduce the number of required \glspl{reif}, it is the first implementation that also automatically introduces \glspl{half-reif} when possible. Not only does this analysis reduce the number of required \glspl{reif}, it is the first implementation that also automatically introduces \glspl{half-reif} when possible.
Our method introduces an new analysis step after the compilation from \minizinc{} to \microzinc{}. Our method introduces a new analysis step after the compilation from \minizinc{} to \microzinc{}.
To determine whether a \constraint{} has to be \gls{reified}, this analysis determines the context of each \constraint{}. To determine whether a \constraint{} has to be \gls{reified}, this analysis determines the context of each \constraint{}.
Crucially, our analysis considers the possibility of identifiers being used in multiple positions, and the usage of user-defined \constraints{}. Crucially, our analysis considers the possibility of identifiers being used in multiple positions, and the usage of user-defined \constraints{}.
Depending on the context of a \constraint, we can decide if a \gls{reif} can be avoided, if a \gls{half-reif} can be used, or if we have to use a full \gls{reif}. Depending on the context of a \constraint, we can decide if a \gls{reif} can be avoided, if a \gls{half-reif} can be used, or if we have to use a full \gls{reif}.
We noted that the usage of \gls{half-reif} interacts with some of the existing simplification techniques in the architecture and propose alterations to accommodate for them. We noted that the usage of \gls{half-reif} interacts with some of the existing simplification techniques in the architecture and propose alterations to accommodate them.
Foremost, \gls{cse} can no longer always reuse the same results for identical \constraint{}, it must now consider the context of the \constraint{}. Foremost, \gls{cse} can no longer always reuse the same results for identical \constraints{}, it must now consider the context of the \constraint{}.
For \constraints{} were \gls{cse} is triggered in multiple context, we propose rules to either use the result that is acceptable in both contexts, or create such a result. For \constraints{} were \gls{cse} is triggered in multiple contexts, we propose rules to either use the result that is acceptable in both contexts, or create such a result.
Using this adjustment we ensure that identical \constraints{} still have a single result. Using this adjustment we ensure that identical \constraints{} are not duplicated and re-use the same \gls{cvar}, even when they occurred in different contexts.
The usage of \gls{propagation} can change the context of a \constraint{} during the \gls{rewriting} process. The usage of \gls{propagation} can change the context of a \constraint{} during the \gls{rewriting} process.
We described how we can communicate this change through the \glspl{cvar} of (half-)\glspl{reif}. We described how we can communicate this change through the \glspl{cvar} of (half-)\glspl{reif}.
Lastly, \glspl{half-reif} can introduce \glspl{implication-chain}, forming a barrier for \gls{propagation}. Lastly, \glspl{half-reif} can introduce \glspl{implication-chain} that can degrade the performance of the \solver{}.
We described a new simplification technique called \gls{chain-compression} that efficiently eliminates these \glspl{implication-chain} where possible. We described a new simplification technique called \gls{chain-compression} that efficiently eliminates these \glspl{implication-chain} where possible.
The techniques to automatically introduce \glspl{half-reif} and the simplification techniques have been implemented in both our prototype rewriting architecture and the existing \minizinc{} \compiler{}. The techniques to automatically introduce \glspl{half-reif} and the simplification techniques have been implemented in both our prototype \gls{rewriting} architecture and the existing \minizinc{} \compiler{}.
These techniques were included in the official release in version 2.3.0. These techniques were included in the official release in version 2.3.0.
In extension, we have adjusted the \gls{rewriting} libraries for existing \minizinc{} \solvers{} to use \gls{half-reif}. In support of this, we have modified the \gls{rewriting} libraries of existing \minizinc{} \solvers{} to use \gls{half-reif}.
Notably, we have implemented explicit \glspl{decomp} of \gls{half-reified} \constraints{} for \gls{mip} and \gls{sat} \solvers{}. Notably, we have implemented explicit \glspl{decomp} of \gls{half-reified} \constraints{} for \gls{mip} and \gls{sat} \solvers{}.
The usage of these \gls{decomp} significantly reduces the number of \constraints{} in the \gls{slv-mod}. The usage of these \glspl{decomp} significantly reduces the number of \constraints{} in the \gls{slv-mod}.
Additionally, we implemented two \gls{propagator} of \gls{half-reif} \constraints{}, \mzninline{all_different} and \mzninline{element}, in a state-of-the-art \gls{cp} \solver{}, \gls{chuffed}, to re-evaluate the claims of the original \gls{half-reif} paper. Additionally, we implemented two \glspl{propagator} for \gls{half-reif} \constraints{}, \mzninline{all_different} and \mzninline{element}, in a state-of-the-art \gls{cp} \solver{}, \gls{chuffed}, to re-evaluate the claims of the original \gls{half-reif} paper.
In our experiments, we reaffirmed the effectiveness of the \glspl{propagator}, but we showed mixed results for the use of automatic \gls{half-reif} on a bigger scale. In our experiments, we reaffirmed the effectiveness of the \glspl{propagator}, but we showed mixed results for the use of automatic \gls{half-reif} on a bigger scale.
While it was clearly beneficial for \gls{sat}, other \solvers{} did not seem to enjoy the same benefit and in some cases were even negatively impacted. While it was clearly beneficial for \gls{sat}, other \solvers{} did not seem to enjoy the same benefit and in some cases were even negatively impacted.
@ -93,51 +96,52 @@ Although \gls{half-reif} is not a new technique, there is still a lot left to ex
In particular, our research raises the questions about its effectiveness for \gls{mip} solvers. In particular, our research raises the questions about its effectiveness for \gls{mip} solvers.
It is clear that the use of \gls{half-reif} is beneficial in some cases, but it seems to have a negative effect in other cases. It is clear that the use of \gls{half-reif} is beneficial in some cases, but it seems to have a negative effect in other cases.
It is thus important that we achieve a better understanding of when the latter occurs. It is thus important that we achieve a better understanding of when the latter occurs.
As also discussed by \textcite{feydy-2011-half-reif}, we see that \gls{cp} solvers are sometimes negatively impacted because \gls{half-reif} do not fix their \gls{cvar}, requiring more search. As also discussed by \textcite{feydy-2011-half-reif}, we see that \gls{cp} solvers are sometimes negatively impacted because \glspl{half-reif} do not fix their \gls{cvar}, requiring more search.
As a solution to this problem we could consider a form in between \gls{half-reif} and full \gls{reif}. As a solution to this problem we could consider a form in between \gls{half-reif} and full \gls{reif}.
In this form the propagator would set the \gls{cvar} to \mzninline{true} if the \constraint{} holds, but does not propagate the negation of the \constraint{} when it is set to \mzninline{false}. In this form the propagator would set the \gls{cvar} to \mzninline{true} if the \constraint{} holds, but does not propagate the negation of the \constraint{} when it is set to \mzninline{false}.
The downside of this form is that it is no longer equivalent to a logical implication (and, for example, \gls{chain-compression} would no longer be applicable), but \glspl{propagator} for this form are still easy to design/implement and they ensure that the \gls{cvar} is fixed through \gls{propagation}. The downside of this form is that it is no longer equivalent to a logical implication (and, for example, \gls{chain-compression} would no longer be applicable), but \glspl{propagator} for this form are still easy to design/implement and they ensure that the \gls{cvar} is fixed through \gls{propagation}.
Finally, the usage of automated \gls{half-reif} in \minizinc{} will allow new solving performance improvements by allowing \solver{} implementers to experiment with \glspl{decomp} or \glspl{propagator} for \gls{half-reified} \constraints{}. Finally, the usage of automated \gls{half-reif} in \minizinc{} will allow new solving performance improvements by allowing \solver{} implementers to experiment with \glspl{decomp} or \glspl{propagator} for \gls{half-reified} \constraints{}.
\paragraph{Incremental Solving} Using a \cml{} instead of a \solver{} as part of a \gls{meta-optimisation} toolchain can be very intuitive and open up new opportunities. \paragraph{Incremental Solving} Using a \cml{} as the interface for a \gls{meta-optimisation} toolchain can be very intuitive and open up new opportunities.
The modeller would describe the process as a changing \cmodel{}. The modeller can describe the process as a changing \cmodel{}.
The overhead of the repeated \gls{rewriting} process to arrive at a \gls{slv-mod} can, however, be a hindrance. The overhead of the repeated \gls{rewriting} process to arrive at a \gls{slv-mod} can, however, be a hindrance.
\Cref{ch:incremental} presents our final contribution: \textbf{two methods to practically eliminate the overhead of using \cmls{} in \gls{meta-optimisation}}. \Cref{ch:incremental} presents our final contribution: \textbf{two methods to practically eliminate the overhead of using \cmls{} in \gls{meta-optimisation}}.
Our primary method, restart-based \gls{meta-optimisation}, allows modellers to describe \gls{meta-optimisation} methods, the iterative changes to their model, as part of their \minizinc{} model. Our primary method, \gls{rbmo}, allows modellers to describe \gls{meta-optimisation} algorithms, the iterative changes to their model, as part of their \minizinc{} model.
These descriptions are rewritten into a small set of new \gls{native} \constraints{} that the \solver{} has to support. These descriptions are rewritten into a small set of new \gls{native} \constraints{} that the \solver{} has to support.
Although this method requires \solvers{} to be slightly extended, this method eliminates the need for repeated \gls{rewriting}. Although this method requires \solvers{} to be slightly extended, it eliminates the need for repeated \gls{rewriting}.
Only a single \gls{slv-mod} is created. Only a single \gls{slv-mod} is created.
The changes to the \gls{slv-mod} are iteratively applied within the \solver{}. The changes to the \gls{slv-mod} are iteratively applied within the \solver{}.
In our experiments, we have shown that his method is highly effective. In our experiments, we have shown that his method is highly effective.
Even compared to an ``oracle'' approach, where the changes are merely read and not computed, this approach is only slightly worse. Even compared to an ``oracle'' approach, where the changes are merely read and not computed, this approach is only slightly slower.
Meanwhile, the time required to rewrite the \gls{meta-optimisation} descriptions is negligible. Meanwhile, the time required to rewrite the \gls{meta-optimisation} descriptions is negligible.
It is not always possible to extend a \solver{}, for these cases we have defined a second method. It is not always possible to extend a \solver{}, so for these cases we have defined a second method.
This method significantly reduces the overhead of \gls{rewriting} when incrementally changing \instances{}. This method significantly reduces the overhead of \gls{rewriting} when incrementally changing \instances{}.
We have defined an interface for \cmls{}. We have defined an incremental interface for \cmls{}.
A modeller can repeatedly add \constraints{} and \variables{} to an \instance{} and, crucially, the additions to the \instance{} can be retracted in reverse order through the use of a \gls{trail}. A modeller can repeatedly add \constraints{} and \variables{} to an \instance{} and, crucially, the additions to the \instance{} can be retracted in reverse order through the use of a \gls{trail}.
Each of these changes to the \instance{} is incrementally applied to the \gls{slv-mod}. Each of these changes to the \instance{} is incrementally applied to the \gls{slv-mod}.
Since multiple generations of \gls{meta-optimisation} share large parts of their \instance{}, this significantly reduces the amount work required in the \gls{rewriting} process. Since multiple iterations of \gls{meta-optimisation} typically share large parts of their \instance{}, this significantly reduces the amount of work required in the \gls{rewriting} process.
As an additional improvement, the changes observed in the \gls{slv-mod} can be incrementally applied within the \solver{}. As an additional improvement, the changes observed in the \gls{slv-mod} can be incrementally applied within the \solver{}.
Ideally, the \solver{} can fully support the incremental changes made to the \gls{slv-mod}. Ideally, the \solver{} can fully support the incremental changes made to the \gls{slv-mod}.
This avoids the overhead of re-initialisation and allows the solver to retain all search information. This avoids the overhead of re-initialisation and allows the solver to retain all search information.
Otherwise, the \solver{} can still be warm-started. Otherwise, the \solver{} can still be warm-started.
Instead of starting the search without any information, the \solver{} is given information about the previous \gls{sol} to speed up it search. Instead of starting the search without any information, the \solver{} is given information about the previous \gls{sol} to speed up its search.
Although our experiments show that this method is not as effective as the initial method. Our experiments show that this method is not as effective as \gls{rbmo}.
It is still a significant improvement over repeatedly \gls{rewriting} the full \instance{}. It is, however, still a significant improvement over repeatedly \gls{rewriting} the full \instance{} that can be employed even in cases where \gls{rbmo} cannot be used.
The improvements offered by these new method may spark future research. The improvements offered by these new methods may spark future research.
Primarily, it will allow and promote the usage of \gls{meta-optimisation} methods in \cmls{} for new problems. Primarily, they will allow and promote the usage of \gls{meta-optimisation} methods in \cmls{} for new problems.
New \gls{meta-optimisation} techniques could require extensions of the methods presented. It could even be worthwhile to revisit existing applications of incremental constraint modelling.
It would even be possible to revisit existing research that uses the combination of \cmls{} and \gls{meta-optimisation} to study improvements that these methods offer. The utilisation of the presented methods might offer a significant improvement in performance, allowing the solving of more complex problems.
Finally, new \gls{meta-optimisation} techniques could require extensions of the methods presented.
\paragraph{Summary} In conclusion, this thesis presented an architecture for the \gls{rewriting} of \cmls{}. \paragraph{Summary} In conclusion, this thesis presented an architecture for the \gls{rewriting} of \cmls{}.
This architecture has been designed with modern usages of these languages in mind, such as \gls{rewriting} for low-level \solvers{} and \gls{meta-optimisation}. This architecture has been designed with modern usages of these languages in mind, such as \gls{rewriting} for low-level \solvers{} and \gls{meta-optimisation}.
It is efficient and incremental, but easily extendible with many simplification techniques. It is efficient and incremental, but easily extensible with many simplification techniques.
It also includes a formal framework to reason about \gls{reif} that is able to introduce \glspl{half-reif}. It also includes a formal framework to reason about \gls{reif} that is able to introduce \glspl{half-reif}.
Finally, we also presented a novel method to specify a \gls{meta-optimisation} method to be executed within a \solver{}. Finally, we also presented a novel method to specify a \gls{meta-optimisation} method to be executed within a \solver{}.
Together, these contribution make \cmls{} a more powerful tool to help solve complex problems. Together, these contributions make \cmls{} a more powerful tool to help solve complex problems.