dekker.one
Jip Dekker's PhD Thesis
1\noindent{}The research presented in this thesis investigates the process of \gls{rewriting} \cmls{}.
2This chapter provides the required background information to understand constraint modelling languages, including the creation of \cmodels{}, the processes employed to solve a \gls{slv-mod}, and the transformation of a \cmodel{} into a \gls{slv-mod}.
3
4In particular, it gives further information about \minizinc{} and discusses the functionality available to create \cmodels{}.
5It also provides some insight into \solvers{}, discussing the most important techniques used to solve \instances{} of \cmodels{}.
6Additionally, it summarizes the functionality of other \cmls{} to serve as a comparison with \minizinc{}.
7This is followed by a brief overview of other closely related \glspl{trs}.
8Finally, the chapter analyses the existing approach to \gls{rewriting} \minizinc{} and discusses its limitations.
9The overview of \cmls{} presented in this chapter supports the research and discussion presented in subsequent chapters.
10
11This chapter is organized as follows.
12We first introduce the reader to \cmls{} and their purpose.
13\Cref{sec:back-minizinc} summarizes the syntax and functionality of \minizinc{}, the \cml{} used within this thesis.
14In \cref{sec:back-solving} we discuss how \gls{cp}, \gls{mip}, and \gls{sat} are used to solve a \gls{slv-mod}.
15\Cref{sec:back-other-languages} introduces alternative \cmls{} and compares their functionality to \minizinc{}.
16Then, \cref{sec:back-term} surveys the closely related technologies in the field of \glspl{trs}.
17Finally, \cref{sec:back-mzn-interpreter} explores the process that the existing \minizinc{} implementation uses to translate a \minizinc{} \instance{} into a \gls{slv-mod}.