\noindent{}The research presented in this thesis investigates the process of \gls{rewriting} \cmls{}.
This 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}.

In particular, it gives further information about \minizinc{} and discusses the functionality available to create \cmodels{}.
It also provides some insight into \solvers{}, discussing the most important techniques used to solve \instances{} of \cmodels{}.
Additionally, it summarizes the functionality of other \cmls{} to serve as a comparison with \minizinc{}.
This is followed by a brief overview of other closely related \glspl{trs}.
Finally, the chapter analyses the existing approach to \gls{rewriting} \minizinc{} and discusses its limitations.
The overview of \cmls{} presented in this chapter supports the research and discussion presented in subsequent chapters.

This chapter is organized as follows.
We first introduce the reader to \cmls{} and their purpose.
\Cref{sec:back-minizinc} summarizes the syntax and functionality of \minizinc{}, the \cml{} used within this thesis.
In \cref{sec:back-solving} we discuss how \gls{cp}, \gls{mip}, and \gls{sat} are used to solve a \gls{slv-mod}.
\Cref{sec:back-other-languages} introduces alternative \cmls{} and compares their functionality to \minizinc{}.
Then, \cref{sec:back-term} surveys the closely related technologies in the field of \glspl{trs}.
Finally, \cref{sec:back-mzn-interpreter} explores the process that the existing \minizinc{} implementation uses to translate a \minizinc{} \instance{} into a \gls{slv-mod}.