Some work on CLP

assets/glossary.tex

@@ -34,6 +34,11 @@
   description={},
 }
 
+\newglossaryentry{backtrack}{
+  name={backtrack},
+  description={},
+}
+
 \newglossaryentry{gls-cbls}{
   name={constraint-based local search},
   description={},

chapters/2_background.tex

@@ -7,7 +7,7 @@ abstraction: an assembly language allows you to abstract from the binary
 instructions and memory positions; Low-level imperial languages, like FORTRAN,
 were the first to allow you to abstract from the processor architecture of the
 target machine; and nowadays writing a program requires little knowledge of the
-actual workings of the hardware.
+actual workings of the hardware on which the program is executed.
 
 Freuder states that the ``Holy Grail'' of programming languages would be where
 the user merely states the problem, and the computer solves it and that
@@ -906,14 +906,46 @@ repeat rule \(r_{3}\) an infinite amount of times. The system, however, is
 confluent as, if it arrives at the same \gls{normal-form}: if the term contains
 any \(0\), then the result will be \(0\); otherwise, the result will be \(1\).
 
-\subsection{Constraint Handling Rules}%
+In \minizinc\ the flattening process is forced to be confluent. Through the
-\label{sub:back-chr}
+function definitions in the language and the type system, \minizinc{} ensures
+that there is at most one applicable rule for any expression. This means that
+given the same \minizinc\ model and solver library, the flattening process will
+result in the same solver level constraint model.
 
-\gls{chr} are a special kind of \glspl{trs} designed to work on constraint models.
+The flattening process is, however, not guaranteed to terminate. When using
+recursive functions, it is possible to create a \minizinc\ model that never
+reaches a flat state. In practice, however, function definitions generally do
+not contain any recursive definitions. In the absence of recursive functions the
+flattening of a model is guaranteed to terminate.
 
 \subsection{Constraint Logic Programming}%
 \label{subsec:back-clp}
 
+\gls{clp} \autocite{marriott-1998-clp} can be seen as a predecessor of \cmls{}
+like \minizinc. A constraint logic program describes the process in which a high
+level constraint model is eventually rewritten into a solver level constraints
+and added to a \gls{solver}. Different from \minizinc{}, the programmer can
+define constraints that can be rewritten in multiple ways. When such a
+constraint occurs in the constraint model, referred to as the goal, the
+constraint logic program will try a different way whenever the problem becomes
+unsatisfiable.
+
+To implement this mechanism there is a tight integration between the solver,
+referred to as the constraint store, and constraint logic program. In addition
+to just adding constraints, the program can also inspect the status of the
+constraint and retract constraints from the constraint store. This allows the
+program to detect when the constraint store has become unsatisfiable and then
+\gls{backtrack} the constraint store to the last decision (\ie, restore the
+constraint store to its state before the last decision was made).
+
+
+
+
+\subsection{Constraint Handling Rules}%
+\label{sub:back-chr}
+
+\gls{chr} are a special kind of \glspl{trs} designed to
+
 \subsection{ACD Term Rewriting}%
 \label{subsec:back-acd}