From 39faee6c4032f798c0e9dbcc12b1e07c16e82dca Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Mon, 26 Jul 2021 13:14:37 +1000 Subject: [PATCH] Use sections instead of paragraphs in conclusions --- chapters/6_conclusions.tex | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/chapters/6_conclusions.tex b/chapters/6_conclusions.tex index 4bb1ce5..3b8b5f9 100644 --- a/chapters/6_conclusions.tex +++ b/chapters/6_conclusions.tex @@ -17,7 +17,8 @@ These improvements focus on the performance of the \gls{rewriting} process in ge 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: \textbf{an architectural design for the rewriting of a \cml{}}. +\section*{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 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 \microzinc{} against which an implementation can be checked. @@ -64,7 +65,8 @@ A possible example of where this information can be useful is found in \gls{cp} 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}. +\section*{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 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. @@ -104,7 +106,8 @@ The downside of this form is that it is not equivalent to a logical implication, However, \glspl{propagator} for this form are still easy to design/implement, and they ensure that the \gls{cvar} is fixed through \gls{propagation}. Finally, 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{} as the interface for a \gls{meta-optimization} toolchain can be very intuitive and opens up new opportunities. +\section*{Incremental Solving} +Using a \cml{} as the interface for a \gls{meta-optimization} toolchain can be very intuitive and opens up new opportunities. 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. \Cref{ch:incremental} presents our final contribution: \textbf{two methods to practically eliminate the overhead of using \cmls{} in \gls{meta-optimization}}. @@ -141,7 +144,8 @@ It could even be worthwhile to revisit existing applications of incremental cons The utilization of the presented methods might offer a significant improvement in performance, allowing the solving of more complex problems. Finally, new \gls{meta-optimization} techniques could require extensions of the methods presented. -\paragraph{Summary} In conclusion, this thesis presented an architecture for the \gls{rewriting} of \cmls{}. +\section*{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-optimization}. 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}.