dekker-phd-thesis/chapters/6_conclusions.tex

%************************************************
\chapter{Conclusions}\label{ch:conclusions}
%************************************************

\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 \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: \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 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 architecture is easily extended with well-known simplification techniques to improve the quality of the produced \solver{} specifications.

\begin{itemize}

	\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 \glspl{ivar}.

	\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.

\end{itemize}

Two prototype programs were developed to evaluate this architecture:

\begin{itemize}
	\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 architecture shines through in the performance tests.

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 \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 defining \constraints{} once their \variable{} has been fixed (under certain circumstances).

\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.

Our method introduces an 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{}.
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 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 \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 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 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 \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 \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 \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 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 \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 \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 \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 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 \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 \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.