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 \glspl{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 sizeable and the process to translate a high-level \cmodel{} into the low-level format required by these \solvers{} is complex.
Second, we have seen a development of the use of \gls{meta-optimization}.
\Gls{meta-optimization} is often implemented by incrementally adjusting \instances{}, after which those \instances{} have to be rewritten to be solved.
Both these methods put additional pressure on the \gls{rewriting} process, which can often be a bottleneck in the overall process.

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

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

The \gls{rewriting} process of a \minizinc{} \instance{} into a \gls{slv-mod} then consists of two steps: the translation of \minizinc{} model transformations into \microzinc{}, implemented by a \compiler{}; and the iterative \gls{rewriting} using these \microzinc{} transformations to arrive at a \gls{slv-mod}, implemented using an \interpreter{}.
The latter operates on a (partial) \glspl{slv-mod}, expressed using the \nanozinc{} language.
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{} becomes unused (\ie{} it is not referred to by \constraints{} any longer), 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 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{avar}.

	\item Finally, \constraints{} can be marked for \gls{del-rew}.
		This requests the \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}, and
	\item a \microzinc{} \gls{byte-code} \interpreter{} that produces a \nanozinc{} \gls{slv-mod}.
\end{itemize}

The implementation of these prototypes lacks the maturity of the existing \minizinc{} \compiler{}.
However, the performance of these prototypes already surpasses the existing implementation, averaging a more than ten times speed-up.

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 prove 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 not yet investigated if the same information might help improve \solver{} performance.
A possible example of where this information can be useful is found in \gls{cp} \solvers{}.
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.

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

Our method introduces a 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 user-defined functions.
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 \gls{half-reif} interacts with some existing simplification techniques in the architecture and propose alterations to accommodate them.
Foremost, \gls{cse} cannot always reuse the same results for identical \constraints{} any more.
It must now also consider the context of the \constraint{}.
For \constraints{} were \gls{cse} is triggered in multiple contexts, 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{} are not duplicated and re-use the same \gls{cvar}, even when they occurred in different contexts.
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} that can degrade the performance of the \solver{}.
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 \gls{rewriting} architecture and the existing \minizinc{} \compiler{}.
These techniques were included in the official release in version 2.3.0.
In support of this, we have modified the \gls{rewriting} libraries of 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 \glspl{decomp} significantly reduces the number of \constraints{} in the \gls{slv-mod}.
Additionally, we implemented two \glspl{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 larger 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 are still numerous open questions.
In particular, our research was unable to determine the effectiveness of \gls{half-reif} 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 \glspl{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 true if the \constraint{} holds, but does not propagate the negation of the \constraint{} when it is set to false.
The downside of this form is that it is not equivalent to a logical implication, which means that measures such as \gls{chain-compression} would not be applicable.
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{}.

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

Our primary method, \gls{rbmo}, allows modellers to describe \gls{meta-optimization} algorithms, 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, it 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 slower.
Meanwhile, the time required to rewrite the \gls{meta-optimization} descriptions is negligible.

It is not always possible to extend a \solver{}, so 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 incremental 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 iterations of \gls{meta-optimization} typically share large parts of their \instance{}, this significantly reduces the amount of 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 reinitialization 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 its search.

Our experiments show that this method is not as effective as \gls{rbmo}.
It is, however, still a significant improvement over repeatedly \gls{rewriting} the full \instance{} that can be employed even in cases where \gls{rbmo} cannot be used.

The improvements offered by these new methods may spark future research.
Primarily, they will allow and promote using \gls{meta-optimization} algorithms in \cmls{} for new problems.
It could even be worthwhile to revisit existing applications of incremental constraint modelling.
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.

\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}.
Finally, we also presented a novel method to specify a \gls{meta-optimization} method to be executed within a \solver{}.
Together, these contributions make \cmls{} a more powerful tool to help solve complex problems.