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

Work on conclusions

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-18 16:31:34 +10:00
parent b75926195e
commit 13a2416910
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
1 changed files with 86 additions and 83 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

169
chapters/6_conclusions.tex
View File

@ -2,139 +2,142 @@
\chapter{Conclusions}\label{ch:conclusions}
%************************************************
\noindent{}High-level \cmls{} make it easy to express decision problems.
They allow the modeller to reason at the level close to the problem, while the tooling of the language is able to create specifications for a range of potential \solvers{}.
Although the importance of creating specifications 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 solved using low-level \solvers{}, such as \gls{mip} and \gls{sat}.
Because of the level at which these technologies reason, specifications are more sizable and the process to reach them is more complex.
Second, we have seen a development of the use of meta-search heuristics.
These heuristics incrementally adjust the \constraint{} model, after which it has to be rewritten to be solved.
Both these methods put additional pressure on the rewriting process, which can often be a bottle-neck in the overall process.
\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.
\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.
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.
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.
Both these methods put additional pressure on the \gls{rewriting} process, which can often be a bottle-neck in the overall process.
In the previous chapters of this thesis, we have explored in detail and presented improvements to the process of rewriting high-level \constraint{} models into \solver{} specifications.
These improvements focus both on the performance of the rewriting process in general, and for incremental adjustments of \constraint{} models in particular.
Crucially, the proposed improvements in the performance of the rewriting process themselves do not impact the quality of the \solver{} specification constructed.
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}.
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{}.
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.
\paragraph{Rewriting Architecture} In \cref{ch:rewriting}, we presented the principle contribution of this thesis: \emph{an architectural design for the rewriting of a high-level \cml{}}.
To achieve this we introduced an execution framework for \microzinc{}, a minimal \cml{}.
At the core of this framework lie formal rewriting rules against which an implementation can be checked.
A complex \cml{}, such as \minizinc{}, can be reduced to \microzinc{} and as such enjoy the same guarantees.
\paragraph{Rewriting Architecture} In \cref{ch:rewriting}, we presented the principle contribution of this thesis: \textbf{an architectural design for the rewriting of a high-level \cml{}}.
We introduced a transformation language \microzinc{}, a minimal describe to describe how an \instance{} is transformed 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.
The transformation required for a complex \cml{}, such as \minizinc{}, can be reduced to \microzinc{} and as such enjoy the same guarantees.
The framework operates on \nanozinc{}, a language that expresses (partial) \solver{} specifications.
Distinctively, \nanozinc{} has the ability to bind \constraints{} that define a \variable{} to that \variable{}.
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 isn't kept in the model for the \constraints{} that define it.
The architecture operates on \nanozinc{}, a language that expresses (partial) \gls{slv-mod}.
Distinctively, \nanozinc{} has the ability to attach \constraints{} to a \variable{}.
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.
Crucially, the framework is easily extended with well-known techniques to improve the quality of the produced \solver{} specifications.
Crucially, the architecture is easily extended with well-known simplification techniques to improve the quality of the produced \solver{} specifications.
\begin{itemize}
\item \Gls{constraint} \gls{propagation} can actively simplify the both \constraints{} and the \glspl{domain} of \variables{} in our architecture.
\item \Gls{propagation} can actively simplify the both \constraints{} and the \glspl{domain} of \variables{} in \glspl{slv-mod}.
\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 \variables{} that would have represented intermediate results.
\item When it is beneficial, the architecture can utilize \gls{aggregation} to combine certain \constraints{} and eliminate \glspl{ivar}.
\item Finally, \constraints{} can be marked for \gls{del-rew}.
This implores to \microzinc{} interpreter to delay the evaluation of a certain call until all possible information is available.
This implores to \microzinc{} \interpreter{} to delay the \gls{rewriting} of a certain call until all possible information is available.
\end{itemize}
Two prototype programs were developed to evaluate this architecture:
\begin{itemize}
\item a compiler that translates \minizinc{} models to a \microzinc{} bytecode,
\item a \microzinc{} \gls{byte-code} interpreter that produces \nanozinc{} specifications.
\item a \compiler{} that translates \minizinc{} models to a \microzinc{} \gls{byte-code},
\item and a \microzinc{} \gls{byte-code} \interpreter{} that produces a \nanozinc{} \gls{slv-mod}.
\end{itemize}
Even though the implementation of these prototypes lacks the maturity of the existing \minizinc{} compiler, the performance of the design of the framework shines through in the performance tests.
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.
This framework 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{}.
This could potentially lead to the ability to proof certain properties of the rewriting process.
Additionally, the framework introduces reasoning about the transition from \minizinc{} to \solver{} specification as two different levels: the transition from \minizinc{} to \microzinc{} and the evaluation of the \microzinc{} to create a \solver{} specification.
In our prototype we have presented techniques to help improve the quality of the \solver{} specification, but many improvements to these techniques and other techniques may be beneficial.
Finally, we use our language \nanozinc{} to track \constraints{} that are introduced to define a \variable{}.
This could potentially lead to the ability to proof 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}.
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{}.
Although we have showed how this helps when a \variable{} becomes unused, we have yet to discover its uses within the \solvers{} themselves.
In \gls{cp} \solvers, for example, it is no longer has to required propagate these defining \constraints{} once their \variable{} has been fixed (under certain circumstances).
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).
\paragraph{Half Reification} The notion of \gls{half-reif} was introduced many years ago \autocite{feydy-2011-half-reif}.
And, although it was generally seen as an improvement of the status quo, the automatic introduction of \glspl{half-reif} was never implemented in any \cml{}.
\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.
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{}}.
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.
In \cref{ch:half-reif}, we have built upon the framework in the previous chapter for our secondary contribution: \emph{the automatic introduction of \gls{half-reif} of \constraints{}}.
Our method introduces an new analysis step after the compilation from \minizinc{} to \microzinc{}.
To determine whether a \constraint{} can be half-reified, this analysis determines the context of each \constraint{}.
Crucially, our analysis considers the possibility of \constraints{} bound to names being used in multiple positions, and the usage of user-defined \constraints{}.
When the \constraint{} is in the right context, or a context transformation can be applied, a \gls{half-reif} can be used.
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{}.
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 optimisation techniques in the framework 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 for them.
Foremost, \gls{cse} can no longer always reuse the same results for identical \constraint{}, 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.
Using this adjustment we ensure that identical \constraints{} still have a single result.
The usage of \gls{propagation} can change the context of a \constraint{} during the rewriting process.
We described how we can communicate this change through the control variables of (half-)\glspl{reif}.
Lastly, the introduction of a \gls{half-reif} on the right hand side of an logical implication essentially introduce layered implications.
In this case, the created control variable forms an extra barrier in during propagation where the left hand side of the implication could have been used directly.
We described a novel optimisation technique that eliminates these implication chains where possible.
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}.
Lastly, \glspl{half-reif} can introduce \glspl{implication-chain}, forming a barrier for \gls{propagation}.
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 accompanying optimisations have been implemented in both our prototype rewriting architecture and the existing \minizinc{} compiler.
These techniques were included in the official release in version 2.3.0. In extension, we have adjusted the rewriting libraries for existing \minizinc{} solvers to use \gls{half-reif}.
Notably, we have implemented explicit decompositions of half-reified \constraints{} for \gls{mip} and \gls{sat} \solvers{}.
The usage of these decompositions significantly reduces the number of \constraints{} in the \solver{} solver specification.
Additionally, we implemented two propagators 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.
In our experiments, we reaffirmed the effectiveness of the propagators, 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 or were even negatively impacted.
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{}.
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}.
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}.
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.
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.
Although \gls{half-reif} is not a new technique, there is still a lot left to explore.
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 thus important that we achieve a better understanding of when the latter occurs.
As also discussed in the original \gls{half-reif}, we see that \gls{cp} solvers are sometimes negatively impacted because \gls{half-reif} do not fix their control variable, requiring more search.
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 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 control variable 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, chain compression would no longer be applicable), but propagators for this form are still easy to design/implement and they ensure that the control variable is fixed through propagation.
Finally, the implementation of automated \gls{half-reif} will enable new solving performance optimisations by allowing \solver{} implementers to experiment with decompositions or propagators for half-reified \constraints{}.
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}.
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 meta-optimisation toolchain can be very intuitive and open up new opportunities.
The modeller would describe the process as a changing \constraint{} model.
The overhead of the repeated rewriting process to arrive at a \solver{} specification can, however, be a hindrance.
\Cref{ch:incremental} presents our final contribution: \emph{two methods to practically eliminate the overhead of using \cmls{} in meta-search}.
\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.
The modeller would 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.
\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 meta-search, allows modellers to describe meta-optimisation heuristics, the iterative changes to their model, as part of their \minizinc{} model.
These descriptions are rewritten using a small set of new primitives that the \solver{} has to support.
Although this method requires \solvers{} to be slightly extended, this method eliminates the need for repeated rewriting.
Only a single \solver{} specification is created.
The changes to the \constraint{} model are iteratively triggered by the solver.
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.
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}.
Only a single \gls{slv-mod} is created.
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.
Even compared to an ``oracle'' approach, where the changes are merely read and not computed, this approach only slightly underperforms.
Meanwhile, the time required to compile the meta-search description is negligible.
Even compared to an ``oracle'' approach, where the changes are merely read and not computed, this approach is only slightly worse.
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.
This method significantly reduces the overhead of rewriting models that incrementally changes.
In particular we defined an interface for \cmls{}.
A modeller can repeatedly add \constraints{} and \variables{} to the model and, crucially, the additions to the model can retracted in reverse order through the use of \gls{trail}ing.
Each of these changes to the \constraint{} model is incrementally applied to the \solver{} specification.
Since multiple generations of meta-optimisation share large parts of their \constraint{} model, this significantly reduces the amount work required in the rewriting process.
This method significantly reduces the overhead of \gls{rewriting} when incrementally changing \instances{}.
We have defined an 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}.
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.
As an additional improvement, the changes observed in the \solver{} specification can be incrementally applied within the \solver{}.
Ideally, the solver can fully support the incremental changes made to the specification.
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}.
This avoids the overhead of re-initialisation and allows the solver to retain all search information.
Otherwise, the solver can still be warm-started.
Instead of starting the search without any information, the \solver{} is given information about the previous solution to speed up it search.
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.
Although our experiments show that this method is not as effective as the initial method.
It is still a significant improvement over the recompilation approach.
It is still a significant improvement over repeatedly \gls{rewriting} the full \instance{}.
The improvements offered by these new method may spark future research.
Primarily, it will allow and promote the usage of meta-optimisation methods in \cmls{} for new problems.
New meta-optimisation techniques could require extensions of the methods presented.
It would even be possible to revisit existing research that uses the combination of \cmls{} and meta-optimisation to study improvements that these methods offer.
Primarily, it 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 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.
\paragraph{Summary} In conclusion, this thesis presented an architecture for the rewriting of high-level \cmls{}.
This architecture has been designed with modern usages of these languages in mind, such as rewriting for low-level \solvers{} and meta-optimisation.
It is efficient and incremental, but easily extendible with many optimisation techniques.
In addition, we have presented the first full implementation of \gls{half-reif} and a novel method to perform incremental search within a \solver{}.
Together, these contribution make high-level \cmls{} a more powerful tool to help solve complex problems.
\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}.
It is efficient and incremental, but easily extendible with many simplification techniques.
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{}.
Together, these contribution make \cmls{} a more powerful tool to help solve complex problems.