40 lines
3.0 KiB
TeX
40 lines
3.0 KiB
TeX
\noindent{}Rewriting a high-level constraint model down into an equivalent solver-level constraint model might often seem like a simple term rewriting system.
|
|
In reality, however, simple rewriting of the model will often result in sub-optimal solver-level model and this might result in exponentially more work for the solver.
|
|
To combat this problem many techniques have been developed to create more efficient solver-level models such as: continuously updating variable domains according to the constraints, correctly resolving constraint sub-typing when variables get fixed, removing any variables and constraints that have become unused, detecting duplicate constraints, and reusing duplicate functional definitions.
|
|
|
|
The application of all these optimisations can, however, be time intensive during the rewriting process.
|
|
And although this was not a problem when high-level \cmls\ were targeting \gls{cp} solvers, where the solver-level constraint model stays relatively small, this poses a big problem for \gls{mip} and \gls{sat} solvers, whose solver-level constraint models are significantly larger.
|
|
|
|
In this chapter, we revisit the rewriting of high-level \cmls\ into solver-level constraint models.
|
|
We describe a new \textbf{systematic view of the execution of \minizinc{}} and build on this to propose a new tool chain.
|
|
We show how this tool chain allows us to:
|
|
|
|
\begin{itemize}
|
|
|
|
\item efficiently rewrite high-level constraint models with \textbf{minimal overhead},
|
|
|
|
\item easily integrate a range of \textbf{optimisation and simplification} techniques,
|
|
|
|
\item and effectively \textbf{detect and eliminate dead code} introduced by functional definitions
|
|
|
|
\end{itemize}
|
|
|
|
The new architecture is shown in \Cref{fig:rew-comp}.
|
|
A constraint model is first compiled into a smaller constraint language called \microzinc{}, independent of the data.
|
|
After the \microzinc{} is transformed into a byte code, it is interpreted with the data to produce \nanozinc\ code, an extension of the existing \flatzinc\ format.
|
|
The interpreter can even be made incremental: in \cref{ch:incremental} we discuss how in meta optimisation, no recompilation is required.
|
|
|
|
We have developed a prototype of this tool chain, and present experimental validation of these advantages.
|
|
The prototype is still very experimental, but preliminary results suggest the new tool chain can perform flattening much faster, and produce better models, than the current \minizinc\ compiler.
|
|
|
|
This chapter is organised as follows.
|
|
\Cref{sec:4-micronano} introduces the \microzinc\ and \nanozinc\ languages, the new intermediate representation we propose that enables more efficient flattening.
|
|
\Cref{sec:4-simplification} describes how we can perform various processing and simplification steps on this representation, and in \cref{sec:rew-experiments} we report on the experimental results of the prototype implementation.
|
|
|
|
\begin{figure}
|
|
\centering
|
|
\includegraphics[width=\linewidth]{assets/img/rew_compilation_structure}
|
|
\caption{\label{fig:rew-comp} The proposed process for the compilation of \minizinc\ instances.}
|
|
\end{figure}
|
|
|