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

First draft of the conclusions

Browse Source
This commit is contained in:
Jip J. Dekker 2021-06-24 19:39:22 +10:00
parent 03e917dbce
commit 574a40ea43
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
1 changed files with 85 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

121
chapters/6_conclusions.tex
View File

@ -19,73 +19,122 @@ We present a summary of the research and its contributions and discuss the futur
\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{}.
This framework offers the first \jip{something}.
A complex \cml{}, such as \minizinc{}, can be reduced to \microzinc{} and as such enjoy the same guarantees \jip{blah}.
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.
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.
Crucially, the framework is easily extended with well-known techniques to improve the quality of the produced \solver{} specifications.
\begin{itemize}
\item We described how \constraint{} \gls{propagation} can actively simplify the both \constraints{} and the \glspl{domain} of \variables{} during the rewriting process.
\item \Gls{constraint} \gls{propagation} can actively simplify the both \constraints{} and the \glspl{domain} of \variables{} in our architecture.
\item \gls{cse}
\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 \constraint{} \gls{aggregation}
\item When it is beneficial, the architecture can utilize \constraint{} \gls{aggregation} to combine certain constraints and eliminate \variables{} that would have represented intermediate results.
\item \gls{del-rew}
\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.
\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{} byte-code interpreter that produces \nanozinc{} specifications
\item a compiler that translates \minizinc{} models to a \microzinc{} bytecode,
\item a \microzinc{} byte-code interpreter that produces \nanozinc{} specifications.
\end{itemize}
\jip{This should probably say something about its performance}
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.
This framework 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.
We introduce
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 might be beneficial.
Finally, we use our language \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).
\paragraph{Half Reification} \Cref{ch:half-reif} we further the
\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{Incremental}
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.
\paragraph{Summary}
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.
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 \constraint{} \gls{propagation} might 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{reification}.
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.
\par\noindent\rule{\textwidth}{0.4pt}
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.
This section should probably have the following components:
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 a solution to this problem we could consider a form in between \gls{half-reif} and full \gls{reification}.
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{}.
\begin{itemize}
\item Quick restatement of problem/importance/motivation
\item Contributions, preferably discussed per section. Relate them back to the research objectives.
\item Limitation and Future work. This can also focus on what my work makes possible, not just what to explore next.
\item Concluding remarks. Maybe a summary of the findings.
\end{itemize}
\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.
Our final contribution, presented in \cref{ch:incremental}, are \emph{two methods to practically eliminate the overhead of using \cmls{} in meta-search}.
\par\noindent\rule{\textwidth}{0.4pt}
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.
The work conducted during my candidature presents significant improvements in the infrastructure surrounding the use of high-level constraint modelling languages.
The implementation of my work can significantly reduce the overhead of the use of these languages.
This will both improve the current usage of these languages and will allow the uses of these languages to continue to grow.
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.
Although the results for the investigated areas of research are very positive, the experiments were all conducted as a comparison to the current status quo.
To provide a more complete analysis of the work conducted, additional comparisons need to be added to compare between the different prototypes created during my candidature (e.g., comparing the different meta-search approaches) and to compare with other constraint modelling systems.
Even the comparison with low-level constraint modelling languages might be beneficial as a upper bound on the performance that could be achieved.
It might not always be 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 trailing.
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.
In the area of the compilation of constraint modelling languages, there is much room for future work that will not be part of my candidature.
The prototype tool chain that we have developed for \minizinc\ is incomplete and leaves out some parts of the complete \minizinc\ language.
In particular, float and set types are only partially supported.
In addition to the implementation of all currently accepted \minizinc\ types, there is room for a more formal exploration of the type systems employed in constraint modelling languages.
An interesting phenomenon that occurs is that certain types, that are not supported by the underlying solver technology, will be replaced by a collection of values of another type.
Similarly, our architecture describes where various kinds of simplifications and optimisations can be applied, but we do not fully explore the almost endless list of possible compilation optimisation, partial evaluation, and redefinition approaches that could potentially be applied.
Finally, the improvements in the meta-search capabilities of high-level constraint modelling languages should allow for more applications of meta-search from these languages.
These capabilities could likely improve existing systems based on these languages.
As an additional improvement, the changes observed in the \solver{} specification might also be incrementally applied within the \solver{}.
Ideally, the solver can fully support the incremental changes made to the specification.
This avoids the overhead of re-initialisation and allows the solver to retain all search information.
Otherwise, the solver might 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.
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.
The improvements offered by these new method might spark future research.
Primarily, it will allow and promote the usage of meta-optimisation methods in \cmls{} for new problems.
New meta-optimisation techniques might 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.
\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.