diff --git a/assets/acronyms.tex b/assets/acronyms.tex
index 4c63e47..bd43a6a 100644
--- a/assets/acronyms.tex
+++ b/assets/acronyms.tex
@@ -1,28 +1,48 @@
+\newacronym[see={[Glossary:]{gls-ampl}}]{ampl}{AMPL\glsadd{gls-cbls}}{A
+  Mathematical Programming Language}
+
 \newacronym[see={[Glossary:]{gls-cbls}}]{cbls}{CBLS\glsadd{gls-cbls}}{Constraint-Based
   Local Search}
+
 \newacronym[see={[Glossary:]{gls-chr}}]{chr}{CHR\glsadd{gls-chr}}{Constraint
   Handling Rules}
+
 \newacronym[see={[Glossary:]{gls-clp}}]{clp}{CLP\glsadd{gls-clp}}{Constraint
   Logic Programming}
+
 \newacronym[see={[Glossary:]{gls-cp}}]{cp}{CP\glsadd{gls-cp}}{Constraint
   Programming}
+
 \newacronym[see={[Glossary:]{gls-cse}}]{cse}{CSE\glsadd{gls-cse}}{Common
   Sub-expression Elimination}
+
 \newacronym[see={[Glossary:]{gls-csp}}]{csp}{CSP\glsadd{gls-csp}}{Constraint
   Satisfaction Problem}
+
 \newacronym[see={[Glossary:]{gls-cop}}]{cop}{COP\glsadd{gls-cop}}{Constraint
   Optimisation Problem}
+
+\newacronym{cpu}{CPU}{Central Processing Unit}
+
 \newacronym[see={[Glossary:]{gls-gbac}}]{gbac}{GBAC\glsadd{gls-gbac}}{Generalised
   Balanced Academic Curriculum}
+
 \newacronym[see={[Glossary:]{gls-lcg}}]{lcg}{LCG\glsadd{gls-lcg}}{Lazy Clause
   Generation}
+
 \newacronym[see={[Glossary:]{gls-lns}}]{lns}{LNS\glsadd{gls-lns}}{Large
   Neighbourhood Search}
+
 \newacronym[see={[Glossary:]{gls-mip}}]{mip}{MIP\glsadd{gls-mip}}{Mixed Integer
   Programming}
+
 \newacronym[see={[Glossary:]{gls-opl}}]{opl}{OPL\glsadd{gls-opl}}{The OPL
   Optimisation Programming Language}
+
+\newacronym{ram}{RAM}{Random Access Memory}
+
 \newacronym[see={[Glossary:]{gls-sat}}]{sat}{SAT\glsadd{gls-sat}}{Boolean
   Satisfiability}
+
 \newacronym[see={[Glossary:]{gls-trs}}]{trs}{TRS\glsadd{gls-trs}}{Term Rewriting
   System}
diff --git a/assets/bibliography/references.bib b/assets/bibliography/references.bib
index be781f4..48cb98c 100644
--- a/assets/bibliography/references.bib
+++ b/assets/bibliography/references.bib
@@ -890,6 +890,27 @@
   publisher       = {MIT Press}
 }
 
+@article{van-hentenryck-2000-opl-search,
+  author          = {Van Hentenryck, Pascal and Perron, Laurent and Puget,
+                  Jean-Fran\c{c}ois},
+  title           = {Search and Strategies in OPL},
+  year            = 2000,
+  issue_date      = {Oct. 2000},
+  publisher       = {Association for Computing Machinery},
+  address         = {New York, NY, USA},
+  volume          = 1,
+  number          = 2,
+  issn            = {1529-3785},
+  url             = {https://doi.org/10.1145/359496.359529},
+  doi             = {10.1145/359496.359529},
+  journal         = {ACM Trans. Comput. Logic},
+  month           = oct,
+  pages           = {285–320},
+  numpages        = 36,
+  keywords        = {search, modeling languages, constraint programming,
+                  combinatorial optimization}
+}
+
 @book{wallis-2011-combinatorics,
   title           = {Introduction to Combinatorics},
   author          = {Wallis, W.D. and George, J.},
diff --git a/assets/glossary.tex b/assets/glossary.tex
index ce0ff13..612bec6 100644
--- a/assets/glossary.tex
+++ b/assets/glossary.tex
@@ -14,6 +14,16 @@
   description={},
 }
 
+\newglossaryentry{gls-ampl}{
+  name={AMPL: A Mathematical Programming Language},
+  description={},
+}
+
+\newglossaryentry{annotation}{
+  name={annotation},
+  description={},
+}
+
 \newglossaryentry{array}{
   name={array},
   description={},
@@ -89,6 +99,11 @@
   description={},
 }
 
+\newglossaryentry{essence}{
+  name={Essence},
+  description={},
+}
+
 \newglossaryentry{flatzinc}{
   name={Flat\-Zinc},
   description={},
@@ -114,6 +129,11 @@
   description={},
 }
 
+\newglossaryentry{interval}{
+  name={interval},
+  description={},
+}
+
 \newglossaryentry{knapsack}{
   name={knapsack problem},
   description={},
@@ -210,6 +230,11 @@
   description={},
 }
 
+\newglossaryentry{search-heuristic}{
+  name={search heuristic},
+  description={},
+}
+
 \newglossaryentry{solver}{
   name={solver},
   description={},
diff --git a/chapters/2_background.tex b/chapters/2_background.tex
index cb6a8ed..df94846 100644
--- a/chapters/2_background.tex
+++ b/chapters/2_background.tex
@@ -229,6 +229,9 @@ assignment to the \glspl{variable} that satisfies the constraints and minimises
 the value of a \gls{variable}, \mzninline{solve minimize x;}, or similarly
 maximises the value of a \gls{variable}, \mzninline{solve maximize x;}.
 
+\jip{TODO:\@ add some information about search in \minizinc{}. It's probably
+  pretty relevant.}
+
 Common structures in \minizinc\ can be captured using function declarations. A
 user can declare a function \mzninline{function @\(T\)@: @\(I\)@(@\(P\)@) = E;}.
 In the function declaration \(T\) is the type of the result of the function,
@@ -548,7 +551,7 @@ following stages:
   declarations and is allowed in the locations where they are used. \\ In the
   process of type checking the model, all identifiers and calls are connected to
   the declaration that they refer to.
-  \item[Flattening] \jip{TODO: This should have something}
+  \item[Flattening] \jip{TODO:\@ This should have something}
   \item[Optimisation] Given the generated \flatzinc{} model, \texttt{minizinc}
   will try optimise this model to try and reduce the number of
   \glspl{constraint} and size of the \glspl{domain} of \glspl{variable} in the
@@ -557,30 +560,221 @@ following stages:
   Any solutions found by the \gls{solver} are communicated back to the user.
 \end{description}
 
-\jip{TODO: Description of the flattening process}
+\jip{TODO:\@ Description of the flattening process}
 
-\jip{TODO: Description of the techniques used during the optimisation phase}
+\jip{TODO:\@ Description of the techniques used during the optimisation phase}
 
-\subsection{Propagation}
+\subsection{Propagation}%
 \label{sub:back-propagation}
 
 \section{Other Constraint Modelling Languages}%
 \label{sec:back-other-languages}
 
+Although \minizinc\ is the \cml\ that is the primary focus of this thesis, there
+are many other \cmls{}. Each \cml{} has its own focus and purpose and comes with
+its own strength and weaknesses. Most of the techniques that are discusses in
+this thesis can be adapted to these languages.
+
+We will now discuss some of the other prominent \cmls{} and will compare them to
+\minizinc\ to indicate to the reader where techniques might have to be adjusted
+to fit other languages.
+
 \subsection{AMPL}%
 \label{sub:back-ampl}
 
 \subsection{OPL}%
-\label{sub:back-}
+\label{sub:back-opl}
+
+\glsaccesslong{opl} \autocite{van-hentenryck-1999-opl} is a \cml\ that has a
+focus aims to combine the strengths of mathematical programming languages like
+\gls{ampl} with the strengths of \gls{cp}. The syntax of \gls{opl} is very
+similar to the \minizinc\ syntax.
+
+Where the \gls{opl} really shines is when modelling scheduling problems.
+Resources and activities are separate objects in the \gls{opl}. This allows
+users express resource scheduling \glspl{constraint} in an incremental and more
+natural fashion. When solving a scheduling problem, the \gls{opl} makes use of
+specialised \gls{interval} \glspl{variable}, which represent when a task will be
+scheduled. For example the \gls{variable} declarations and \glspl{constraint}
+for a jobshop problem would look like this in an \gls{opl} model:
+
+\begin{minted}[autogobble=true]{text}
+  ScheduleHorizon = sum(j in Jobs, t in Tasks) duration[j, t];
+  Activity task[j in Jobs, t in Tasks] (duration[j,t]);
+  Activity makespan;
+  UnaryResource tool[Machines];
+
+  minimize makespan.end
+  subject to {
+    forall (j in Jobs)
+      task[j,nbTasks] precedes makespan;
+
+    forall (j in Jobs)
+      forall (t in 1..nbTasks-1)
+        task[j, t] precedes task[j, t+1];
+
+    forall (j in Jobs)
+      forall (t in Tasks)
+        task[j, t] requires tool[resource[j, t]];
+  };
+\end{minted}
+
+The equivalent declarations and \glspl{constraint} would look like this in
+\minizinc{}:
+
+\begin{mzn}
+  int: horizon = sum(j in Jobs, t in Tasks)(duration[j,t]);
+  var 0..horizon: makespan;
+  array[JOB,TASK] of var 0..maxt: start;
+
+  constraint forall(j in Jobs, t in 1..nbTasks-1) (
+    start[j,t] + duration[j,t] <= start[j,t+1]
+  );
+
+  constraint forall(j in Jobs) (
+    start[j, nbTasks] + duration[j, nbTasks] <= makespan
+  );
+
+  constraint forall(m in Machines) (
+    disjunctive(
+      [start[j,t] | j in Jobs, t in Tasks where resource[j,t] == m],
+      [duration[j,t] | j in Jobs, t in Tasks where resource[j,t] == m],
+    )
+  );
+
+  solve minimize makespan;
+\end{mzn}
+
+Note that the \minizinc{} model does not have explicit Activity variables. It
+must instead use \glspl{variable} that represent the start times of the activity
+and a \gls{variable} to represent the time at which all activities are finished.
+The \gls{opl} model also has the advantage that it can first create resource
+objects and then use the \texttt{requires} keyword to force tasks on the same
+machine to be mutually exclusive. In \minizinc{} the same requirement is
+implemented through the use of \mzninline{disjunctive} constraints. Although
+this has the same effect, all mutually exclusive jobs have to be combined in a
+single statement in the model. This can make it harder in \minizinc\ to write
+the correct \gls{constraint} and its meaning might be less clear.
+
+The \gls{opl} also contains a specialised search syntax that can be used to
+instruct its solvers \autocite{van-hentenryck-2000-opl-search}. This syntax
+allows the modellers full programmatic control over how the solver will explore
+the search space depending on the current state of the variables. This offers to
+modeller more control over the search in comparison to the
+\gls{search-heuristic} \glspl{annotation} in \minizinc{}, which only allow
+modellers to select predefined \glspl{search-heuristic} already implemented in
+the solver. Take, for example, the following \gls{opl} search definition:
+
+\begin{minted}[autogobble=true]{text}
+  search {
+    try x < y | y >= x endtry;
+  }
+\end{minted}
+
+This search strategy will ensure that we first try and find a solution where the
+\gls{variable} \mzninline{x} takes a value smaller than \mzninline{y}, if it
+does not find a solution, then it will try finding a solution where the oposite
+is true. This search specification, like many other imaginable, cannot be
+enforce using \minizinc\ \gls{search-heuristic} \glspl{annotation}.
+
+To support \gls{opl}'s dedicated search language, the language is tightly
+integrated with its dedicated \glspl{solver}. Its search syntax requires that
+the \gls{opl} process can directly interact with the \gls{solver}'s internal
+search mechanism and that the \gls{solver} reasons about search on the same
+level as the \gls{opl} model. It is therefore not possible to connect other
+\glspl{solver} to \gls{opl}.
+
+The \gls{opl} does not allow modellers to create their own (user-defined)
+functions. A modeller is restricted to the \gls{global} constraint library
+provided by the \gls{opl}'s standard library.
 
 \subsection{Essence}%
 \label{sub:back-essence}
 
+\gls{essence} \autocite{frisch-2007-essence} is another high-level \cml\ is
+cherished for its adoption of high-level \gls{variable} types. In addition to
+all variable types that are contained in \minizinc{}, \gls{essence} also
+contains:
+
+\begin{itemize}
+  \item finite sets of non-iteger types,
+  \item finite multisets of any type,
+  \item finite (partial) functions,
+  \item and (regular) partitions of finite types.
+\end{itemize}
+
+Since sets, multisets, and functions can be defined on any other type, these
+types can be arbitrary nested and the modeller can define, for example, a
+\gls{variable} that is a set of set of integers. Partitions can be defined for
+finite types. These types in \gls{essence} are restricted to Booleans,
+enumerated types, or a restricted set of integers.
+
+For example, the Social Golfers Problem, can be modelled in \gls{essence} as
+follows:
+
+\begin{minted}[autogobble=true]{text}
+language Essence 1.3
+
+given w, g, s : int(1..)
+
+letting Golfers be new type of size g * s
+
+find sched : set (size w) of
+             partition (regular, numParts g, partSize s) from Golfers
+
+such that
+
+forAll g1, g2 : Golfers, g1 < g2 .
+    (sum week in sched . toInt(together({g1, g2}, week))) <= 1
+\end{minted}
+
+In \minizinc{} the same problem could be modelled as:
+
+\begin{mzn}
+include "globals.mzn";
+
+int: g;
+int: w;
+int: s;
+
+enum: golfers = anon_enum(g * s);
+
+set of int: groups = 1..g;
+set of int: rounds = 1..w;
+array [rounds, groups] of var set of golfers: group;
+
+constraint forall (r in rounds, g in groups) (
+  card(group[r, g]) = s
+);
+
+constraint forall(r in rounds) (
+  all_disjoint(g in groups)(group[r, g])
+);
+
+constraint forall (a, b in golfers where a < b) (
+  sum (r in rounds, g in groups) (
+    {a, b} subset group[r, g]
+  ) <= 1
+);
+\end{mzn}
+
+Note that, through the \gls{essence} type system, the first 2 \glspl{constraint}
+in the \minizinc{} are implied in the \gls{essence} model. This is an example
+where the use of high-level types can help give the modeller create more concise
+models.
+
+These high-level variables are often not directly supported by the
+\glspl{solver} that is employed to solve \gls{essence} instances. To solve the
+problem, not only do the \glspl{constraint} have to be translated to
+\glspl{constraint} supported by the solver, but also all \glspl{variable} have
+to be translated to a combination of \glspl{constraint} and \glspl{variable}
+compatible with the targeted solver.
+
 \section{Term Rewriting}%
 \label{sec:back-term}
 
 At the heart of the flattening process lies a \glsaccesslong{trs}. A \gls{trs}
-\cite{baader-1998-term-rewriting} describes a computational model the full
+\autocite{baader-1998-term-rewriting} describes a computational model the full
 process can be describe as the application of rules \(l \rightarrow r\), that
 replace a \gls{term} \(l\) with another \gls{term} \(r\). A \gls{term} is an
 expression with nested sub-expressions consisting of \emph{function} and