More work on the glossary

assets/glossary.tex

@@ -10,8 +10,8 @@
 % }
 
 \newglossaryentry{aggregation}{
-  name={aggregation},
+  name={constraint aggregation},
-  description={},
+  description={This technique combines many smaller \glspl{constraint} into a one or, by exception, a few larger \glspl{constraint}},
 }
 
 \newglossaryentry{gls-ampl}{
@@ -19,6 +19,16 @@
   description={},
 }
 
+\newglossaryentry{assignment}{
+  name={assignment},
+  description={
+		A mapping from \glspl{parameter} or \glspl{variable} to values.
+		An assignment is referred to as \gls{partial} when it maps only a subset of the \glspl{parameter} and \glspl{variable} of a \gls{model}.
+		A \gls{parameter-assignment} is an \gls{partial} \gls{assignment} that maps only the \glspl{parameter}, a \gls{variable-assignment} maps only the \glspl{variable}.
+		A complete \gls{parameter-assignment} maps all \glspl{parameter} of a \gls{model}, a complete \gls{variable-assignment} maps all \glspl{variable} of a \gls{model}
+	},
+}
+
 \newglossaryentry{gls-ast}{
   name={Abstract Syntax Tree},
   description={},
@@ -77,7 +87,7 @@
 \newglossaryentry{cml}{
   name={constraint modelling language},
   description={
-		A constraint modelling language is a computer language used to define \glspl{model}.
+		A computer language used to define \glspl{model}.
 		Low-level constraint modelling languages allow modellers to define \glspl{model} in terms of \gls{native} \glspl{constraint} and \gls{variable} types.
 		To create a \gls{slv-mod} the language merely assigns the \glspl{parameter}, (almost) no \gls{rewriting} is required.
 		In contrast, high-level constraint modelling languages provide \glspl{global}, allowing modellers to reason at a level different from the targeted \gls{solver}
@@ -132,10 +142,23 @@
 \newglossaryentry{cvar}{
   name={control variable},
   description={
-		A control variable is a special form of an \gls{ivar} where the \gls{variable} represent the result of a \gls{reification}
+		A special form of an \gls{ivar} where the \gls{variable} represent the result of a \gls{reification}
 	},
 }
 
+\newglossaryentry{compiler}{
+  name={compiler},
+  description={
+		A computer program that transforms a program in a computer language, referred to as the \emph{source}, into a different language (or instruction set), the \emph{target}.
+		The goal of this transformation is generally to create an executable version of the program
+	},
+}
+
+\newglossaryentry{compiling}{
+  name={compiling},
+  description={see \gls{compiler}},
+}
+
 \newglossaryentry{dec-prb}{
   name={decision problem},
 	description={
@@ -147,7 +170,7 @@
 \newglossaryentry{decomp}{
   name={decomposition},
 	description={
-		A decomposition formulates a \gls{constraint} in terms of other \glspl{constraint} in order to reach \gls{native} \glspl{constraint}.
+		A formulation of a \gls{constraint} in terms of other \glspl{constraint} in order to reach \gls{native} \glspl{constraint}.
 		Note that the new \glspl{constraint} might represent the same decisions using a different \glspl{variable}, possibly of different types
 	},
 }
@@ -159,7 +182,7 @@
 
 \newglossaryentry{domain}{
   name={domain},
-  description={A domain is a set of value that a \gls{variable} can take without violating any \glspl{constraint} in the problem},
+  description={A set of value that a \gls{variable} can take without violating any \glspl{constraint} in the problem},
 }
 
 \newglossaryentry{domain-con}{
@@ -174,7 +197,7 @@
 
 \newglossaryentry{eqsat}{
   name={equisatisfiable},
-  description={Two \glspl{model} are equisatisfiable when a bijective function can be defined to map the \glspl{sol} of one \gls{model} onto the \glspl{sol} of the other.},
+  description={Two \glspl{model} are equisatisfiable when a bijective function can be defined to map the \glspl{sol} of one \gls{model} onto the \glspl{sol} of the other},
 }
 
 \newglossaryentry{fixed}{
@@ -215,7 +238,7 @@
 \newglossaryentry{global}{
   name={global constraint},
   description={
-		A global constraint is a common \gls{constraint} pattern.
+		A common \gls{constraint} pattern.
 		These patterns can generally span any number of \glspl{variable}.
 		For example, the well-known global constraint \( \textsc{All\_Different}(\ldots) \) requires all its arguments to take a different value.
 		Global constraints are usually not \gls{native} to a \gls{solver}.
@@ -241,19 +264,26 @@
 \newglossaryentry{ivar}{
   name={introduced variable},
   description={
-		An introduced variable is a \gls{variable} that was created in the reformulation of a \gls{decomp}.
+		A \gls{variable} that was created in the reformulation of a \gls{decomp}.
 		New \gls{variable} are introduced either to redefine an existing \gls{variable} using a different type or to connect newly introduced \glspl{constraint}
 	},
 }
 
-\newglossaryentry{interval}{
+\newglossaryentry{int-sol}{
-  name={interval},
+  name={intermediate solution},
-  description={},
+  description={A \gls{sol} in an \gls{opt-prb} that is not (yet) proven to be the \gls{opt-sol}},
 }
 
 \newglossaryentry{instance}{
   name={instance},
-  description={A \gls{model} with assignments for all its \glspl{parameter}},
+  description={A \gls{model} with a complete \gls{parameter-assignment}},
+}
+
+\newglossaryentry{interpreter}{
+  name={interpreter},
+  description={
+		A computer program that directly executes instructions one at a time
+	},
 }
 
 \newglossaryentry{knapsack}{
@@ -295,7 +325,7 @@
 \newglossaryentry{model}{
   name={constraint model},
   description={
-		A constraint model is a formalisation of a \gls{dec-prb} or an \gls{opt-prb}.
+		A formalisation of a \gls{dec-prb} or an \gls{opt-prb}.
 		It is defined in terms of formalised decision, \glspl{variable} of different kinds (\eg{} Boolean, integers, or even sets), and \glspl{constraint}, Boolean logic formulas which are forced to hold in any \gls{sol}, and, in case of an \gls{opt-prb}, an \gls{objective}.
 		Any external data required to formulate the \glspl{constraint} is said to be the \glspl{parameter}.
 		The combination of a constraint model and assignments for its \glspl{parameter} is said to be an \gls{instance} of the constraint model.
@@ -334,7 +364,7 @@
 
 \newglossaryentry{objective}{
   name={objective function},
-  description={An objective function is a function defined over the \glspl{variable} of a \gls{model} to assign a numeric value to the quality of the \gls{sol}.},
+  description={A function defined over the \glspl{variable} of a \gls{model} to assign a numeric value to the quality of the \gls{sol}},
 }
 
 \newglossaryentry{operator}{
@@ -364,7 +394,7 @@
 
 \newglossaryentry{opt-sol}{
   name={optimal solution},
-  description={An \gls{sol} in an \gls{opt-prb} for which it has been proven that no other \gls{sol} exist of higher quality},
+  description={A \gls{sol} in an \gls{opt-prb} for which it has been proven that no other \gls{sol} exist of higher quality},
 }
 
 \newglossaryentry{restart}{
@@ -384,13 +414,13 @@
 
 \newglossaryentry{sol}{
   name={solution},
-  description={A solution is an assignment for all \glspl{variable} in an \gls{instance} such that no \gls{constraint} is violated},
+  description={A complete \gls{variable-assignment} for an \gls{instance} such that all \glspl{constraint} are satisfied},
 }
 
 \newglossaryentry{solver}{
   name={solver},
   description={
-		A solver is a computer program that is designed to solve certain types of \gls{dec-prb} and/or \gls{opt-prb}.
+		A computer program that is designed to solve certain types of \gls{dec-prb} and/or \gls{opt-prb}.
 		Given a \gls{slv-mod}, in a specified format, a solver will (eventually) produce a \gls{sol} for it.
 		When solving a \gls{opt-prb}, solvers often produce intermediate \glspl{sol} before producing the \gls{opt-sol}
 	},
@@ -399,12 +429,22 @@
 \newglossaryentry{parameter}{
   name={problem parameter},
   description={
-		A problem parameter is immutable data used to define one or more \glspl{constraint}.
+		Problem parameters are part of the external input for a \gls{model}.
-		Parameters are part of the external input for a \gls{model}.
+		They can be used as immutable data used to define \glspl{constraint} or provide structural information about an \gls{instance}.
-		The combination of a \gls{model} and assignment for all its problem parameters is referred to as an \gls{instance} of a \gls{model}
+		For example, a problem parameter might influence the number of \glspl{constraint} in an \gls{instance}
 	},
 }
 
+\newglossaryentry{parameter-assignment}{
+  name={parameter assignment},
+  description={see \gls{assignment}},
+}
+
+\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 },
+}
+
 \newglossaryentry{propagation}{
   name={constraint propagation},
   description={},
@@ -494,6 +534,16 @@
 	},
 }
 
+\newglossaryentry{variable-assignment}{
+  name={variable assignment},
+  description={see \gls{assignment}},
+}
+
+\newglossaryentry{violated}{
+  name={violated},
+  description={A \gls{constraint} is said to be violated when its logical expression is known to be false},
+}
+
 \newglossaryentry{zinc}{
   name={Zinc},
   description={},

chapters/2_background.tex

@@ -836,7 +836,7 @@ 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 \constraints{} in an incremental and more natural fashion.
-When solving a scheduling problem, the \gls{opl} makes use of specialised \gls{interval} \variables{}, which represent when a task will be scheduled.
+When solving a scheduling problem, the \gls{opl} makes use of specialised interval \variables{}, which represent when a task will be scheduled.
 
 \begin{example}
 
@@ -1372,7 +1372,7 @@ These \solvers{} would likely perform better had they directly received the equi
 
 Since many solvers support linear constraints, it is often an additional burden to have intermediate values that have to be given a value in the solution.
 
-This can be resolved using the \gls{aggregation} of constraints.
+This can be resolved using the \gls{aggregation}.
 When we aggregate constraints we collect multiple \minizinc\ expressions, that would each have been separately translated, and combine them into a singular structure that eliminates the need for intermediate \variables{}.
 For example, the arithmetic definitions can be combined into linear constraints, Boolean logic can be combined into clauses, and counting constraints can be combined into global cardinality constraints.
 

chapters/3_rewriting.tex

@@ -736,7 +736,7 @@ These \nanozinc\ definitions are correct, but, at least for \gls{mip} solvers \j
 These \glspl{solver} would likely perform better had they received the linear constraint \mzninline{int_lin_le([1,2,-1],  [x,y,z], 0)} directly, which corresponds to \mzninline{1*x + 2*y - z <= 0}.
 Since many solvers support linear constraints, it is often an additional burden to have intermediate values that have to be given a value in the solution.
 
-This can be resolved using the \gls{aggregation} of constraints.
+This can be resolved using the \gls{aggregation}.
 When we aggregate constraints we combine constraints connected through functional definitions into one or multiple constraints eliminating the need for intermediate variables.
 For example, the arithmetic definitions can be combined into linear constraints, Boolean logic can be combined into clauses, and counting constraints can be combined into global cardinality constraints.
 
@@ -850,7 +850,7 @@ These are very encouraging results, given that we are comparing a largely unopti
 % When a redefinition of a constraint requires the introspection into the current domain of a variable, it is often important to have the tightest possible domain.
 % Hence, we discuss how in choosing the next \nanozinc\ constraint to rewrite, the interpreter can sometimes delay the rewriting of certain constraints to ensure the most amount of information is available.
 % \Gls{cse}, our next optimisation technique, ensures that we do not create or evaluate the same constraint or function twice and reuse variables where possible.
-% Finally, the last optimisation technique we discuss is the use of constraint \gls{aggregation}.
+% Finally, the last optimisation technique we discuss is the use of \gls{aggregation}.
 % The use of \gls{aggregation} ensures that individual functional constraints can be collected and combined into an aggregated form.
 % This allows us to avoid the existence of intermediate variables in some cases.
 % This optimisation is very important for \gls{mip} solvers.

chapters/4_half_reif.tex

@@ -969,7 +969,7 @@ However, we can imagine that the removed constraints might in some cases help th
 An important technique used by \gls{mip} solvers is to detect certain pattern, such as cliques, during the pre-processing of the \gls{mip} instance.
 Some patterns might only be detected when using a full \gls{reification}.
 Furthermore, the performance of \gls{mip} solvers is often dependent on the order and form in which the constraints are given.
-\jip{TODO:\ Is there a citation for this?} With the usage of the \constraint{} \gls{aggregation} and \gls{del-rew}, these can be exceedingly different when using \gls{half-reif}.
+\jip{TODO:\ Is there a citation for this?} With the usage of the \gls{aggregation} and \gls{del-rew}, these can be exceedingly different when using \gls{half-reif}.
 
 \jip{TODO: \gls{sat} number are still preliminary, but look optimistic.
 Only one case where the solver time is severely impacted.}

chapters/6_conclusions.tex

@@ -35,7 +35,7 @@ Crucially, the framework is easily extended with well-known techniques to improv
 	\item \Gls{cse} is used to detect any duplicate calls.
 		We describe how it can be employed both during the compilation from \minizinc{} to \microzinc{}, and in the evaluation of \microzinc{}.
 
-	\item When it is beneficial, the architecture can utilize \constraint{} \gls{aggregation} to combine certain constraints and eliminate \variables{} that would have represented intermediate results.
+	\item When it is beneficial, the architecture can utilize \gls{aggregation} to combine certain constraints and eliminate \variables{} that would have represented intermediate results.
 
 	\item Finally, \constraints{} can be marked for \gls{del-rew}.
 		This implores to \microzinc{} interpreter to delay the evaluation of a certain call until all possible information is available.