diff --git a/chapters/6_conclusions.tex b/chapters/6_conclusions.tex index b31093b..98b1018 100644 --- a/chapters/6_conclusions.tex +++ b/chapters/6_conclusions.tex @@ -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.