CML flow figure and more details when comparing languages

assets/acronyms.tex

@@ -24,6 +24,8 @@
 
 \newacronym{cpu}{CPU}{Central Processing Unit}
 
+\newacronym{jsp}{JSP}{Job Shop Problem}
+
 \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}
@@ -54,7 +56,9 @@
 
 \newacronym[see={[Glossary:]{gls-sat}}]{sat}{SAT\glsadd{gls-sat}}{Boolean Satisfiability}
 
+\newacronym{sgp}{SGP}{Social Golfer Problem}
+
 \newacronym[see={[Glossary:]{gls-trs}}]{trs}{TRS\glsadd{gls-trs}}{Term Rewriting System}
 
-\newacronym{tsp}{TSP\glsadd{gls-trs}}{Travelling Salesperson Problem}
+\newacronym{tsp}{TSP}{Travelling Salesperson Problem}
 

assets/glossary.tex

@@ -466,11 +466,11 @@
 
 \newglossaryentry{partial}{
   name={partial},
-  description={A function is said to be partial when it does not have a defined result for every possible input. Similarly, an \gls{assignment} is said to be partial when it maps only a subset of the \glspl{parameter} and \glspl{variable} in a },
+  description={A function is said to be partial when it does not have a defined result for every possible input. Similarly, an \gls{assignment} is said to be partial when it maps only a subset of the \glspl{parameter} and \glspl{variable} in a \gls{model}.},
 }
 
 \newglossaryentry{propagation}{
-  name={constraint pro\-pa\-ga\-tion},
+  name={constraint propagation},
   description={},
 }
 
@@ -485,7 +485,7 @@
 }
 
 \newglossaryentry{reif}{
-  name={reif},
+  name={reification},
   description={A reification is a special form of a \gls{constraint} where, instead of the \gls{constraint} being enforced in the \glspl{sol}, it enforces that a \gls{cvar} represents whether the \gls{constraint} holds or not},
 }
 

assets/listing/back_jsp.mod

@@ -0,0 +1,18 @@
+ScheduleHorizon = sum(j in Jobs, t in Tasks) duration[j, t];@\Vlabel{line:back:opl:horizon}@
+Activity task[j in Jobs, t in Tasks] (duration[j,t]);@\Vlabel{line:back:opl:task}@
+Activity makespan;@\Vlabel{line:back:opl:makespan}@
+UnaryResource tool[Machines];@\Vlabel{line:back:opl:resources}@
+
+minimize makespan.end@\Vlabel{line:back:opl:goal}@
+subject to {
+	forall (j in Jobs)@\Vlabel{line:back:opl:con2}@
+		forall (t in 1..nbTasks-1)
+			task[j, t] precedes task[j, t+1];
+
+	forall (j in Jobs) @\Vlabel{line:back:opl:con1}@
+		task[j,nbTasks] precedes makespan;
+
+	forall (j in Jobs)@\Vlabel{line:back:opl:con3}@
+		forall (t in Tasks)
+			task[j, t] requires tool[resource[j, t]];
+};

assets/listing/back_jsp.mzn

@@ -0,0 +1,20 @@
+int: horizon = sum(j in Jobs, t in Tasks)(duration[j,t]);
+var 0..horizon: makespan;
+array[JOB,TASK] of var 0..horizon: 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;

assets/listing/back_sgp.essence

@@ -0,0 +1,11 @@
+language Essence 1.3
+
+given nweeks, ngroups, size : int(1..)@\Vlabel{line:back:essence:pars}@
+
+letting Golfers be new type of size ngroups * size@\Vlabel{line:back:essence:ntype}@
+
+find sched : set (size weeks) of@\Vlabel{line:back:essence:var}@
+	partition (regular, numParts ngroups, partSize size) from Golfers
+
+such that forAll g1, g2 : Golfers, g1 < g2 .@\Vlabel{line:back:essence:con}@
+	(sum week in sched . toInt(together({g1, g2}, week))) <= 1

assets/listing/back_sgp.mzn

@@ -0,0 +1,25 @@
+include "globals.mzn";
+
+1..infinity: weeks;
+1..infinity: ngroups;
+1..infinity: size;
+
+enum: golfers = anon_enum(ngroups * size);
+
+set of int: groups = 1..g;
+set of int: Rounds = 1..w;
+array [rounds, groups] of var set of golfers: sched;
+
+constraint forall (r in rounds, g in groups) (
+	card(sched[r, g]) = s
+);
+
+constraint forall(r in rounds) (
+	all_disjoint(g in groups)(sched[r, g])
+);
+
+constraint forall (a, b in golfers where a < b) (
+	sum (r in rounds, g in groups) (
+		{a, b} subset sched[r, g]
+	) <= 1
+);

assets/listing/back_tsp.mod

@@ -0,0 +1,18 @@
+set Cities ordered;@\Vlabel{line:back:ampl:parstart}@
+set Paths := {i in Cities, j in Cities: ord(i) < ord(j)};
+param cost {Paths} >= 0;@\Vlabel{line:back:ampl:parend}@
+
+var Take {Paths} binary;@\Vlabel{line:back:ampl:var}@
+
+param n := card {Cities};@\Vlabel{line:back:ampl:compstart}@
+set SubSets := 0 .. (2**n - 1);
+set PowerSet {k in SubSets} := {i in Cities: (k div 2**(ord(i)-1)) mod 2 = 1};@\Vlabel{line:back:ampl:compend}@
+
+minimize TotalCost: sum {(i,j) in Paths} cost[i,j] * Take[i,j];@\Vlabel{line:back:ampl:goal}@
+
+subj to Tour {i in S}:@\Vlabel{line:back:ampl:con1}@
+	sum {(i,j) in Paths} Take[i,j] + sum {(j,i) in Paths} Take[j,i] = 2;
+
+subj to SubtourElimation {k in SubSet diff {0,2**n-1}}:@\Vlabel{line:back:ampl:con2}@
+	sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (i,j) in Paths} X[i,j] +
+	sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (j,i) in Paths} X[j,i] >= 2;

assets/listing/back_tsp.mzn

@@ -0,0 +1,7 @@
+enum CITIES;
+array[CITIES, CITIES] of int: cost;
+
+array[CITIES] of var CITIES: next;
+constraint circuit(next);
+
+solve minimize sum(i in CITIES) (cost[i, next[CITIES]]);

assets/packages.tex

@@ -184,6 +184,7 @@
 	tabsize=2,
 ]{minizinc}}{\end{minted}}
 
+\newcommand{\plainfile}[1]{\inputminted[autogobble=true,breaklines,breakindent=4em,numbers=left,escapeinside=@@,fontsize=\scriptsize,tabsize=2]{text}{#1}}
 \newenvironment{plain}{\VerbatimEnvironment{}\begin{minted}[
   autogobble=true,
   breaklines,

chapters/1_introduction.tex

@@ -52,7 +52,7 @@ We assume that each job has a task for every machine.
 As an \gls{opt-prb}, our goal is to find an schedule that minimises the finishing time of the last task.
 
 \begin{listing}
-	\pyfile{assets/misc/intro_open_shop.mod}
+	\pyfile{assets/listing/intro_open_shop.mod}
 	\caption{\label{lst:intro-open-shop} An \glsxtrshort{ampl} model of the open shop problem}
 \end{listing}
 

chapters/2_background.tex

@@ -31,10 +31,16 @@ Or, when this is not possible, prove that no such \gls{assignment} exists.
 Many \cmls{} also support the modelling of \gls{opt-prb}, where a \gls{dec-prb} is augmented with an \gls{objective}.
 In this case the goal is to find a \gls{sol} that satisfies all \constraints{} while minimising (or maximising) the value of the \gls{objective}.
 
-\todo{figure that visualises how \cmodels{} + assignments becomes \instance{}, and then rewritten to \gls{slv-mod} and given to a solver.}
-
 Although a \cmodel{} does not contain any instructions on how to find a suitable \gls{sol}, \instances{} of \cmodels{} can generally be given to a dedicated \solver{}.
-The \solver{} uses a dedicated algorithm that finds a \gls{sol} that fits the requirements of the \instance{}.
+To solve these \instances{}, however, they might have to go through a \gls{rewriting} process to arrive at a \gls{slv-mod}, input accepted by a \solver{}.
+The \solver{} then uses a dedicated algorithm that finds a \gls{sol} that fits the requirements of the \instance{}.
+This process of a \cml{} is visualised in \cref{fig:back-cml-flow}.
+
+\begin{figure}
+	\centering
+	\includegraphics[width=\columnwidth]{assets/img/back_cml_flow}
+	\caption{\label{fig:back-cml-flow}A flow diagram of typical process of a \cml{}.}
+\end{figure}
 
 \begin{example}%
 \label{ex:back-knapsack}
@@ -63,12 +69,12 @@ The \solver{} uses a dedicated algorithm that finds a \gls{sol} that fits the re
 	Finally, the \parameter{} \(C\) gives the numeric value of the total space that is left in the car before packing the toys.
 
 	This \cmodel{} gives an abstract mathematical definition of the \gls{opt-prb} that would be easy to adjust to changes in the requirements.
-	To solve \instances{} of this problem, however, these \instances{} have to be rewritten into input accepted by a \solver{}.
+	To solve \instances{} of this problem, however, the \instances{} have to be rewritten into input accepted by a \solver{}.
 	\Cmls{} are designed to allow the modeller to express combinatorial problems similar to the above mathematical definition and generate input that can be directly used by dedicated \solvers{}.
 \end{example}
 
 % \begin{listing}
-% 	\pyfile{assets/py/2_dyn_knapsack.py}
+% 	\pyfile{assets/listing/2_dyn_knapsack.py}
 % 	\caption{\label{lst:2-dyn-knapsack} A Python program that solves a 0-1 knapsack problem using dynamic programming}
 % \end{listing}
 
@@ -100,7 +106,7 @@ Its expressive language and extensive library of \glspl{global} allow users to e
 \end{example}
 
 \begin{listing}
-	\mznfile{assets/mzn/back_knapsack.mzn}
+	\mznfile{assets/listing/back_knapsack.mzn}
 	\caption{\label{lst:back-mzn-knapsack} A \minizinc\ model describing a 0-1 knapsack problem}
 \end{listing}
 
@@ -864,54 +870,56 @@ Different types of \solvers{} can also have access to different types of \constr
 
 \begin{example}
 
-	\todo{explain what the TSP problem actually is. Probably needs a reference}
-	If we consider the well-known travelling salesman problem, then we might model this problem in \gls{ampl} as follows.
+	Let us consider modelling in \gls{ampl} by considering the well-known \gls{tsp}.
+	In the \gls{tsp}, we are given a list of cities and the distances between all cities.
+	The goal of the problem is to find a shortest path that visits all the cities exactly once and returns to its origin.
+	A possible \cmodel{} for this problem in \gls{ampl} is shown in \cref{lst:back-ampl-tsp}.
 
-	\begin{ampl}
-		set Cities ordered;
-		set Paths := {i in Cities, j in Cities: ord(i) < ord(j)};
-		param cost {Paths} >= 0;
-		var Take {Paths} binary;
+	\begin{listing}
+		\amplfile{assets/listing/back_tsp.mod}
+		\caption{\label{lst:back-ampl-tsp} An \gls{ampl} model describing the \gls{tsp}}
+	\end{listing}
 
-		param n := card {Cities};
-		set SubSets := 0 .. (2**n - 1);
-		set PowerSet {k in SubSets} := {i in Cities: (k div 2**(ord(i)-1)) mod 2 = 1};
+	\Lrefrange{line:back:ampl:parstart}{line:back:ampl:parend} declare the \parameters{} of the \cmodel{}.
+	The \gls{ampl} model requires a set of names of cities, \texttt{Cities}, as input.
+	From these cities it declares a set \texttt{Paths} that contain all possible paths between the different cities.
+	Note how its definition uses a \gls{comprehension} to eliminate symmetric paths.
+	For each possible paths the model also requires its cost.
 
-		minimize TotalCost: sum {(i,j) in Paths} cost[i,j] * Take[i,j];
+	On \lref{line:back:ampl:var} we find the declaration for the \variables{} of the model.
+	For each possible path it decides whether the it is used, yes or no.
+	The \constraint{} on \lref{line:back:ampl:con1} ensures that for each city, one possible path to the city and one possible path from the city is taken.
 
-		subj to Tour {i in S}:
-			sum {(i,j) in Paths} Take[i,j] + sum {(j,i) in Paths} Take[j,i] = 2;
+	Crucially, this does yet enforce that the taken variables represent a single path.
+	It is still possible for so-called subtours to exist, multiple unconnected path that together span all the cities.
+	A naive way to eliminate these subtours is by forcing that any subset of the set of cities has at least an incoming and an outgoing path.
+	\Lrefrange{line:back:ampl:compstart}{line:back:ampl:compend} of the model compute all possible subsets of cities.
+	These are then used by the \constraint{} on \lref{line:back:ampl:con2} to ensure they have the required paths going in and out.
 
-		subj to SubtourElimation {k in SubSet diff {0,2**n-1}}:
-			sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (i,j) in Paths} X[i,j] +
-			sum {i in PowerSet[k], j in Cities diff PowerSet[k]: (j,i) in Paths} X[j,i] >= 2;
-	\end{ampl}
+	Finally, \lref{line:back:ampl:goal} sets the goal of the \gls{ampl} model: to minimize the cost of all the paths taken.
 
-
-	\todo{extend this paragraph, go over the ampl model, exactly explain what elements related to what part of the \minizinc{} syntax.}
 	This model shows that the \gls{ampl} syntax has many features similar to \minizinc{}.
 	Like \minizinc{}, \gls{ampl} has an extensive expression language, which includes \gls{generator} expressions and a vast collection of \glspl{operator}.
 	The building block of the model are also similar: \parameter{} declarations, \variable{} declarations, \constraints{}, and a solving goal.
 
-	The same problem can be modelled in \minizinc\ as follows:
+	\begin{listing}
+		\mznfile{assets/listing/back_tsp.mzn}
+		\caption{\label{lst:back-mzn-tsp} An \minizinc{} model describing the \gls{tsp}}
+	\end{listing}
 
-	\begin{mzn}
-		enum CITIES;
-		array[CITIES, CITIES] of int: cost;
+	A \minizinc{} model for the same problem is shown in \cref{lst:back-mzn-tsp}
 
-		array[CITIES] of var CITIES: next;
-
-		constraint circuit(next);
-
-		solve minimize sum(i in CITIES) (cost[i, next[CITIES]]);
-	\end{mzn}
-
-	Even though the \gls{ampl} is similar to \minizinc{}, the models could not be more different.
+	Even though the \gls{ampl} has a similar syntax to \minizinc{}, the models could not be more different.
 	The main reason for this difference is the level at which these models are written.
+
 	The \gls{ampl} model is written to target a \gls{mip} solver.
 	In the \gls{ampl} language this means that you are required to use the language functionality that is compatible with the targeted \solver{}; in this case, all expression have to be linear equations.
+
 	In \minizinc{} the modeller is not constrained in the same way.
-	The modeller is always encouraged to create high-level \cmodels{}.
+	It can use the viewpoint of choosing, from each city, to which city to go next.
+	A \mzninline{circuit} \gls{global} is then used to enforce that these decisions form a single path over all cities.
+
+	In \minizinc{}, the modeller is always encouraged to create high-level \cmodels{}.
 	\minizinc{} then rewrites these models into compatible \glspl{slv-mod}.
 \end{example}
 
@@ -929,63 +937,57 @@ When solving a scheduling problem, the \gls{opl} makes use of specialised interv
 
 \begin{example}
 
-	\todo{explain what the job shop problem actually is. Probably needs a reference}
-	For example the \variable{} declarations and \constraints{} for a job shop problem would look like this in an \gls{opl} model:
+	Let us consider modelling in \gls{opl}, by considering the well-known \gls{jsp}.
+	The \gls{jsp} is similar to the open shop problem discussed in the introduction.
+	Like the open shop problem, we are tasked with scheduling jobs with multiple tasks.
+	Each task must be performed by an assigned machine.
+	A machine can only perform one task at the same time.
+	And, only one task of the same job can be scheduled at the same time.
+	However, in the \gls{jsp}, the tasks within a job also have a specified order.
+	Abstracting from the \parameter{} declarations, the possible formulation of the \variable{} declarations and \constraints{} for the \gls{jsp} in \gls{opl} is shown in \cref{lst:back-opl-jsp}.
 
-	\begin{plain}
-		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];
+	\begin{listing}
+		\plainfile{assets/listing/back_jsp.mod}
+		\caption{\label{lst:back-opl-jsp} An \gls{opl} model describing the \gls{jsp}, abstracting from \parameter{} declarations.}
+	\end{listing}
 
-		minimize makespan.end
-		subject to {
-			forall (j in Jobs)
-				task[j,nbTasks] precedes makespan;
+	\Lref{line:back:opl:task} declares the \texttt{task} \variables{}, the main \variable{} of in model.
+	These \variables{} have the type \texttt{Activity}, a special type used to declare any scheduling event with a begin and end time.
+	\Variables{} of this type are influence by the \texttt{ScheduleHorizon} \parameter{} defined on \lref{line:back:opl:horizon} of the model.
+	This \parameter{} restricts the time span in which all activities in the \cmodel{} must be scheduled.
+	On \lref{line:back:opl:con2}, we enforce the order between the different tasks for the same job.
+	The \constraint{} uses the \texttt{precedes} operator to enforce one activity takes places before another.
 
-			forall (j in Jobs)
-				forall (t in 1..nbTasks-1)
-					task[j, t] precedes task[j, t+1];
+	Another activity is declared on \lref{line:back:opl:makespan}.
+	The \texttt{makespan} \variable{} represents the time spanned by all tasks.
+	This is enforced by the \constraint{} on \lref{line:back:opl:con1}.
+	\Lref{line:back:opl:goal} set the minimisation of \texttt{makespan} to be the goal of the model.
 
-			forall (j in Jobs)
-				forall (t in Tasks)
-					task[j, t] requires tool[resource[j, t]];
-		};
-	\end{plain}
+	Resources are important notions in \gls{opl}.
+	A resource can be any requirement of an activity.
+	On \lref{line:back:opl:resources} a \texttt{UnaryResource} is declared for every machine. 
+	A \texttt{UnaryResource} can be used by at most one activity at a time.
+	The \constraint{} on \lref{line:back:opl:con3} ensures that at most one task activity can use same machine at the same time.
+	The \constraint{} uses the \texttt{requires} operator to bind an activity to a resource.
 
-	\todo{extend this paragraph, go over the opl model, exactly explain what elements related to what part of the \minizinc{} syntax.}
-	The equivalent declarations and \constraints{} would look like this in \minizinc{}:
+	\begin{listing}
+		\mznfile{assets/listing/back_jsp.mzn}
+		\caption{\label{lst:back-mzn-jsp} An \minizinc{} model describing the \gls{jsp}, abstracting from \parameter{} declarations.}
+	\end{listing}
 
-	\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;
+	A fragment of a \minizinc{} model modelling the same parts of \gls{jsp} is shown in \cref{lst:back-mzn-jsp}.
 	
-		constraint forall(j in Jobs, t in 1..nbTasks-1) (
-			start[j,t] + duration[j,t] <= start[j,t+1]
-		);
+	Notably, \minizinc{} does not have explicit activity \variables{}.
+	It instead uses integer \variables{} that represent the start times of the tasks and the time at which all tasks are finished.
+	This means that much of the implicit behaviour of the \texttt{Activity} \variables{} has to be defined explicitly.
+	Where in the \gls{opl} model we could just state a global scheduling horizon, in \minizinc{} it has to be explicitly included in the \domains{} of the time \variables{}.
+	And, instead of a \texttt{precedes} operator, we have to explicitly enforce the precedence of tasks using linear \constraints{}.
 
-		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 \variables{} that represent the start times of the activity and a \variable{} to represent the time at which all activities are finished.
-	The \gls{opl} model also has the advantage that it first states the resource objects and then uses the \texttt{requires} keyword to force tasks on the same machine to be mutually exclusive.
+	The \gls{opl} model also has the advantage of its resource syntax.
+	It first states the resource objects and then merely has to 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 might make it harder in \minizinc{} to write the correct \constraint{} and its meaning might be less clear.
-
 \end{example}
 
 The \gls{opl} also contains a specialised search syntax that is used to instruct its solvers \autocite{van-hentenryck-2000-opl-search}.
@@ -1025,64 +1027,57 @@ Partitions are defined for finite types: Booleans, enumerated types, or a restri
 
 \begin{example}
 
-	\todo{explain what the job shop problem actually is. Probably needs a reference}
-	Consider, for example, the Social Golfers Problem, can be modelled in \gls{essence} as follows:
+	Let us consider modelling in \gls{essence} by considering the well-known \gls{sgp}.
+	The \gls{sgp} considers a community of golfers that plans games of golf for a set number of weeks.
+	Every week all the golfers are split into groups of equal size and each group plays a game of golf.
+	The goals of the problem is find a way to split the groups different every week, such that no two golfers will meet each other twice.
+	Two golfers can only be part of the same group once.
+	A \cmodel{} for the \gls{sgp} in \gls{essence} can be seen in \cref{lst:back-essence-sgp}.
 
-	\begin{plain}
-	language Essence 1.3
+	\begin{listing}
+		\plainfile{assets/listing/back_sgp.essence}
+		\caption{\label{lst:back-essence-sgp} An \gls{essence} model describing the \gls{sgp}}
+	\end{listing}
 
-	given w, g, s : int(1..)
+	The \gls{essence} model starts with the preamble declaring the version of the language that is used.
+	All the \parameters{} of the \cmodel{} are declared on line \lref{line:back:essence:pars}: \texttt{weeks} is the number of weeks to be considered, \texttt{groups} is the number of groups of golfers, and \texttt{size} is the size of each group.
+	The input for the \parameters{} is checked to ensure that they take a value that is one or higher.
+	\Lref{line:back:essence:ntype} then uses the \parameters{} to declares a new type to represent the golfers.
 
-	letting Golfers be new type of size g * s
+	Most of the problem is modelled in the \variable{} declared on \lref{line:back:essence:var}.
+	It declares a \variable{} that is a set of partitions of the golfers.
+	The choice in \variable already contains some of the implied constraints.
+	Because the \variable{} reasons about partitions of the golfers, a correct assignment is already guaranteed to correctly split the golfers into groups.
+	The usage of a set of size \texttt{weeks} means that we directly reason about that number of partitions that have to be unique.
 
-	find sched : set (size w) of
-							partition (regular, numParts g, partSize s) from Golfers
+	The type of the \variable{} does, however, not guarantee that the no two golfers will not meet each other twice.
+	Therefore, a \constraint{} that enforces this is found on \lref{line:back:essence:con}.
+	Notably, the \texttt{together} function tests whether two elements are in the same part of a partition.
 
-	such that
-
-	forAll g1, g2 : Golfers, g1 < g2 .
-			(sum week in sched . toInt(together({g1, g2}, week))) <= 1
-	\end{plain}
-
-	\todo{extend this paragraph, go over the opl model, exactly explain what elements related to what part of the \minizinc{} syntax.}
-	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}
+	A \minizinc{} the same problem could be modelled can be found in \cref{lst:back-mzn-sgp}.
 
+	The \minizinc{} model start similar to the essence model, in the declaration of the \parameters{} and a type for the golfers.
+	The differences start from the declaration of the \variables{}.
+	The \minizinc{} model is unable to use a set of partitions and instead uses a array of sets.
+	Each set represents a single group in a single week.
 	Note that, through the \gls{essence} type system, the first two \constraints{} in the \minizinc{} are implied in the \gls{essence} model.
 	This is an example where the use of high-level types helps give the modeller create more concise models.
+	Apart from syntax and the \variable{} viewpoint, the \constraint{} that enforces that golfers only occur in the same group once is identical.
+
+	\begin{listing}
+		\mznfile{assets/listing/back_sgp.mzn}
+		\caption{\label{lst:back-mzn-sgp} An \minizinc{} model describing the \gls{sgp}}
+	\end{listing}
 
 \end{example}
 
-The high-level \variables{} available in \gls{essence} are often not \gls{native} to \solvers{}.
-To solve an \instance{}, not only do the \constraints{} have to be translated to \constraints{} \gls{native} to the \solver{}, but also all \variables{} have to be translated to a combination of \constraints{} and \variables{} \gls{native} to the \solver{}.
-\todo{This needs a note that though \minizinc{} might also need transformation of the \variables{}, \gls{essence} will need to make more decisions along the way. It is generally easier to turn for example a integer into Booleans than the high-level transformations that they do.}
+\Gls{essence} allows the use of many high-level \variable{} and \constraints{} on these \variables{}.
+Since these types of \variables{} are often not \gls{native} to the \solver{}.
+\Gls{rewriting} will translate these types into \gls{native} \variables{} and \constraints{}.
+However, along the way there can be many decisions about the representation used for the \solver{}.
+There are often multiple ways to represent a high-level \variable{}, or how to enforce its implicit \constraints{}.
+Unlike \minizinc{}, \Gls{essence} does not allow modellers or \solvers{} to influence this process directly.
+The process is internal to the \gls{essence} compiler.
 
 \section{Term Rewriting}%
 \label{sec:back-term}

chapters/5_incremental.tex

@@ -30,12 +30,12 @@ For each decision variable \mzninline{x[i]}, it draws a random number from a uni
 For example, \mzninline{uniform_neighbourhood(x, 0.2)} would result in each variable in the array \mzninline{x} having a 20\% chance of being unconstrained, and an 80\% chance of being assigned to the value it had in the previous solution.
 
 \begin{listing}
-	\mznfile{assets/mzn/6_lns_minisearch_pred.mzn}
+	\mznfile{assets/listing/6_lns_minisearch_pred.mzn}
 	\caption{\label{lst:6-lns-minisearch-pred} A simple random \gls{lns} predicate implemented in \minisearch{}}
 \end{listing}
 
 \begin{listing}
-	\mznfile{assets/mzn/6_lns_minisearch.mzn}
+	\mznfile{assets/listing/6_lns_minisearch.mzn}
 	\caption{\label{lst:6-lns-minisearch} A simple \gls{lns} \gls{meta-search} implemented in \minisearch{}}
 \end{listing}
 
@@ -81,7 +81,7 @@ The other \mzninline{restart_X} annotations define different strategies for rest
 The \mzninline{timeout} annotation gives an overall time limit for the search, whereas \mzninline{restart_limit} stops the search after a fixed number of restarts.
 
 \begin{listing}
-	\mznfile{assets/mzn/6_restart_ann.mzn}
+	\mznfile{assets/listing/6_restart_ann.mzn}
 	\caption{\label{lst:6-restart-ann} New annotations to control the restarting
 		behaviour}
 \end{listing}
@@ -106,7 +106,7 @@ Function \mzninline{status} returns the status of the previous restart, namely:
 Function \mzninline{last_val} (which, like \mzninline{sol}, has versions for all basic variable types) allows modellers to access the last value assigned to a variable (the value is undefined if \mzninline{status()=START}).
 
 \begin{listing}
-	\mznfile{assets/mzn/6_state_access.mzn}
+	\mznfile{assets/listing/6_state_access.mzn}
 	\caption{\label{lst:6-state-access} Functions for accessing previous solver
 		states}
 \end{listing}
@@ -132,7 +132,7 @@ Therefore, users have to define their overall strategy in a new predicate.
 \Cref{lst:6-basic-complete} shows a complete example of a basic \gls{lns} model.
 
 \begin{listing}
-	\mznfile{assets/mzn/6_basic_complete.mzn}
+	\mznfile{assets/listing/6_basic_complete.mzn}
 	\caption{\label{lst:6-basic-complete} Complete \gls{lns} example}
 \end{listing}
 
@@ -147,7 +147,7 @@ In any following restart, \mzninline{select} is incremented modulo \mzninline{N}
 \noindent{}This will activate a different neighbourhood for each restart (\lref{line:6:roundrobin:post}).
 
 \begin{listing}
-	\mznfile{assets/mzn/6_round_robin.mzn}
+	\mznfile{assets/listing/6_round_robin.mzn}
 	\caption{\label{lst:6-round-robin} A predicate providing the round-robin
 		meta-heuristic}
 \end{listing}
@@ -158,7 +158,7 @@ For adaptive \gls{lns}, a simple strategy is to change the size of the neighbour
 \Cref{lst:6-adaptive} shows an adaptive version of the \mzninline{uniform_neighbourhood} that increases the number of free variables when the previous restart failed, and decreases it when it succeeded, within the bounds \([0.6,0.95]\).
 
 \begin{listing}
-	\mznfile{assets/mzn/6_adaptive.mzn}
+	\mznfile{assets/listing/6_adaptive.mzn}
 	\caption{\label{lst:6-adaptive} A simple adaptive neighbourhood}
 \end{listing}
 
@@ -309,7 +309,7 @@ We can compile models that contain the new built-ins by extending the \minizinc\
 It simply replaces the functional form by a predicate \mzninline{status} (declared in \lref{line:6:status}), which constrains its local variable argument \mzninline{stat} to take the status value.
 
 \begin{listing}
-	\mznfile{assets/mzn/6_status.mzn}
+	\mznfile{assets/listing/6_status.mzn}
 	\caption{\label{lst:6-status} MiniZinc definition of the \mzninline{status} function}
 \end{listing}
 
@@ -323,7 +323,7 @@ Otherwise, we replace the function call with a type specific \mzninline{int_sol}
 
 
 \begin{listing}
-	\mznfile{assets/mzn/6_sol_function.mzn}
+	\mznfile{assets/listing/6_sol_function.mzn}
 	\caption{\label{lst:6-int-sol} MiniZinc definition of the \mzninline{sol}
 		function for integer variables}
 \end{listing}
@@ -340,7 +340,7 @@ The MiniZinc definition of the \mzninline{uniform_nbh} function is shown in \Cre
 Note that the function accepts variable arguments \mzninline{l} and \mzninline{u}, so that it can be used in combination with other functions, such as \mzninline{sol}.
 
 \begin{listing}
-	\mznfile{assets/mzn/6_uniform_slv.mzn}
+	\mznfile{assets/listing/6_uniform_slv.mzn}
 	\caption{\label{lst:6-int-rnd} MiniZinc definition of the
 		\mzninline{uniform_nbh} function for floats}
 \end{listing}
@@ -402,7 +402,7 @@ We have omitted the similar code generated for \mzninline{x[2]} to \mzninline{x[
 Note that the \flatzinc\ shown here has been simplified for presentation.
 
 \begin{listing}
-	\mznfile{assets/mzn/6_basic_complete_transformed.mzn}
+	\mznfile{assets/listing/6_basic_complete_transformed.mzn}
 	\caption{\label{lst:6-flat-pred} \flatzinc{} that results from compiling \\
 		\mzninline{basic_lns(uniformNeighbourhood(x,0.2))}.}
 \end{listing}
@@ -648,7 +648,7 @@ The restart strategy is
 
 % GBAC
 \begin{listing}[b]
-	\mznfile{assets/mzn/6_gbac_neighbourhood.mzn}
+	\mznfile{assets/listing/6_gbac_neighbourhood.mzn}
 	\caption{\label{lst:6-free-period}\texttt{gbac}: neighbourhood freeing all courses in a period.}
 \end{listing}
 
@@ -677,7 +677,7 @@ However, \gls{lns} again significantly improves over standard Chuffed.
 \subsubsection{\texttt{steelmillslab}}
 
 \begin{listing}
-	\mznfile{assets/mzn/6_steelmillslab_neighbourhood.mzn}
+	\mznfile{assets/listing/6_steelmillslab_neighbourhood.mzn}
 	\caption{\label{lst:6-free-bin}\texttt{steelmillslab}: Neighbourhood that frees
 		all orders assigned to a selected slab.}
 \end{listing}
@@ -711,7 +711,7 @@ Still, \chuffedMzn\ outperforms \chuffedStd\ by always finding an optimal soluti
 \subsubsection{\texttt{rcpsp-wet}}
 
 \begin{listing}
-	\mznfile{assets/mzn/6_rcpsp_neighbourhood.mzn}
+	\mznfile{assets/listing/6_rcpsp_neighbourhood.mzn}
 	\caption{\label{lst:6-free-timeslot}\texttt{rcpsp-wet}: Neighbourhood freeing
 		all tasks starting in the drawn interval.}
 \end{listing}

chapters/A2_benchmark.tex

@@ -276,7 +276,7 @@ The data and original model are available at:
 \end{center}
 
 \begin{listing}
-	\mznfile{assets/mzn/prize.mzn}
+	\mznfile{assets/listing/prize.mzn}
 	\caption{\label{lst:bench-prize} A \minizinc{} model for the Prize Collecting Path problem}
 \end{listing}
 
@@ -291,7 +291,7 @@ The data and original model are available at:
 \end{center}
 
 \begin{listing}
-	\mznfile{assets/mzn/qcp_max.mzn}
+	\mznfile{assets/listing/qcp_max.mzn}
 	\caption{\label{lst:bench-qcpmax} A \minizinc{} model for the QCP-Max problem}
 \end{listing}