dekker-phd-thesis/assets/glossary.tex

% Note: glossary entries for terms that are acronyms should be prefixed 'gls-'
% so the non-prefixed reference is used to refer to the acronym

\newglossaryentry{aggregation}{
  name={constraint aggregation},
  description={A technique that combines many smaller \glspl{constraint} into a one or, by exception, a few larger \glspl{constraint}.},
}

\newglossaryentry{gls-ampl}{
  name={AMPL:\ A Mathematical Programming Language},
  description={AMPL is a \gls{cml} originally designed to serve as a common input language for mathematical \glspl{solver} (\eg{} \gls{lp} and \gls{mip}). It has later been extended for other types of \glspl{solver}. See \cref{sub:back-ampl}.},
}

\newglossaryentry{gls-api}{
  name={Application Programming Interface (API)},
  description={
		A particular set of rules and specifications that a software program can follow to access and make use of the services and resources provided by another particular software program that implements that API.
	}
}

\newglossaryentry{assignment}{
  name={assignment},
  description={
		A mapping from \glspl{prb-par} or \glspl{variable} to values.
		An assignment is referred to as \gls{partial} when it maps only a subset of the \glspl{prb-par} and \glspl{variable} of a \gls{model}.
		A \gls{parameter-assignment} is a \gls{partial} \gls{assignment} that maps only the \glspl{prb-par}, a \gls{variable-assignment} maps only the \glspl{variable}.
		A complete \gls{parameter-assignment} maps all \glspl{prb-par} 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={A tree structure representing the syntactic structure of a piece of computer language. These structures are often used in a \gls{compiler} or \gls{interpreter}.},
}

\newglossaryentry{annotation}{
  name={annotation},
  description={Extra information added to \gls{minizinc} items or expressions. \gls{minizinc} can be \gls{annotated} to provide information or hints to the targeted \gls{solver} or the \gls{rewriting} process.},
}

\newglossaryentry{annotated}{
  name={annotated},
  description={See \gls{annotation}.},
}

\newglossaryentry{array}{
  name={array},
  description={A data structure that holds a collection of elements, each identified by an index. Provided the index of an element, the array can retrieve the element.},
}

\newglossaryentry{avar}{
  name={auxiliary variable},
  description={
    A \gls{variable} not explicitly defined in a \gls{model}, but rather introduced in the \gls{rewriting} of an \gls{instance}.
		Auxiliary \glspl{variable} are generally introduced to redefine an existing \gls{variable} using \glspl{variable} of a different type, to represent a sub-expression, or to connect \glspl{constraint} in a \gls{decomp}.
	}
}

\newglossaryentry{backtrack}{
  name={backtrack},
  description={A \gls{solver} is said to backtrack when it revisits a search decision (\eg{} a value assumed during search). Notably the action of backtracking generally involves invalidating all effects of the revisited and subsequent search decisions.},
}

\newglossaryentry{binding}{
  name={binding},
  description={A \gls{variable} is said to have a binding \gls{domain} when it is tighter than the bounds that can be computed from its defining expression. A binding \gls{domain} is a \gls{constraint} of the overall \gls{model}.},
}

\newglossaryentry{bnb}{
  name={branch and bound},
  description={A search method to find a \gls{opt-sol}. After an initial \gls{sol} is found, the search continuously looks for \glspl{sol} for which the \gls{objective} will return a better value than the incumbent \gls{sol}. If it is such a \gls{sol} cannot exist, then the final incumbent \gls{sol} is a \gls{opt-sol}.},
}

\newglossaryentry{byte-code}{
  name={byte-code},
  description={A set of instructions designed to be efficiently executed by an \gls{interpreter}. Distinctive from other computer languages a byte code has a very compact representation, \eg{} using only numbers, and can not be directly read by humans.},
}

\newglossaryentry{booleanization}{
  name={Booleanization},
  description={The process of \gls{rewriting} a \gls{model} to a \gls{sat} or \gls{maxsat} problem.},
}


\newglossaryentry{bounds-con}{
  name={bounds consistent},
  description={A \gls{propagator} is bounds consistent when it reduces the minimum and maximum values of \domains{} that do not occur in a \gls{sol}.},
}

\newglossaryentry{gls-cbc}{
  name={COIN-OR Branch-and-Cut},
  description={A well-known open source \gls{mip} \gls{solver} \autocite{forrest-2020-cbc}.},
}

\newglossaryentry{gls-cbls}{
  name={constraint-based local search},
  description={A form of local search using \gls{constraint} violations as its \gls{objective}. The search method estimate the amount a \gls{constraint} is \gls{violated} in terms of a numeric value, the objective of the search is to minimize this value. Generally \constraints{} can also offer ``search steps'' that can be taken that do not introduce new violations.},
}

\newglossaryentry{chain-compression}{
  name={chain compression},
  description={A technique used to simplify \glspl{implication-chain}. See \cref{subsec:half-compress}.},
}

\newglossaryentry{chuffed}{
  name={Chuffed},
  description={A well-known open source \gls{lcg} \gls{solver} \autocite{chuffed-2021-chuffed}.},
}

\newglossaryentry{comprehension}{
  name={comprehension},
  description={A syntactic construct available in \minizinc{} to construct sets and \glspl{array}. It constructs the elements based on an expression initialized by a \gls{generator}.},
}

\newglossaryentry{conditional}{
  name={conditional},
  description={A type of expression that makes a choice between two or more expressions. In \minizinc{} these expressions take the form \mzninline{if @\(B\)@ then @\(X\)@ else @\(Y\)@endif}.},
}

\newglossaryentry{constraint}{
  name={constraint},
  description={A formalized rule of a problem. Constraints are generally expressed in terms of Boolean logic.},
}

\newglossaryentry{cml}{
  name={constraint modelling language},
  description={
		A computer language used to define \glspl{model}.
		Constraint modelling languages allow modellers to define \glspl{model} in terms of \glspl{prb-par}, \gls{variable} and \glspl{constraint}.
		Together with a complete \gls{parameter-assignment} a \gls{model} forms an \gls{instance}.
		Through the process of \gls{rewriting} the \gls{instance} is transformed into a \gls{slv-mod}, for which a \gls{solver} can find \glspl{sol}.
	}
}

\newglossaryentry{cplex}{
  name={CPLEX},
  description={A well-known proprietary \gls{mip} \gls{solver} developed by IBM \autocite{ibm-2020-cplex}.},
}

\newglossaryentry{gls-chr}{
  name={constraint handling rules},
  description={A non-deterministic declarative rule based programming language to maintain or improve a constraint store. Constraint handling rules are often used as an extension of \gls{clp}. See \cref{sub:back-chr}.},
}

\newglossaryentry{gls-clp}{
  name={constraint logic programming},
  description={An extension of logic programming to include the concepts of \gls{cp}. A constraint logic program manipulates a \gls{constraint} store to find relevant variants where all \glspl{constraint} contained in the store are \gls{satisfied}. See \cref{subsec:back-clp}.},
}

\newglossaryentry{gls-cp}{
  name={constraint programming},
  description={
		A general technique to find \glspl{sol} to \glspl{instance} of \glspl{model}.
		A constraint programming solver interleaves \gls{propagation} with making \glspl{search-decision} to reduce the \gls{search-space}.
    See \cref{subsec:back-cp}.
	}
}

\newglossaryentry{gls-cse}{
  name={common sub-expression elimination},
  description={A technique stemming from programming language to avoid duplicate computation. In \glspl{cml} this technique is used to avoid the creation of duplicate \glspl{variable} and \glspl{constraint}. See \cref{subsec:back-cse}.},
}

\newglossaryentry{confluence}{
  name={confluence},
  description={A property of a \gls{trs}. The system is said to be confluent if it always arrives at the same \gls{normal-form}.},
}

\newglossaryentry{cvar}{
  name={control variable},
  description={
		A special form of an \gls{avar} where the \gls{variable} represent the result of a \gls{reif}.
	}
}

\newglossaryentry{compiler}{
  name={compiler},
  description={
		A computer program that transforms a program in a computer language, referred to as the ``source'', into a different language (or instruction set), the ``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={
		A problem which can be defined as making a set of decisions under a certain set of rules.
		Decisions problems can be formalized as \glspl{model}.
	}
}

\newglossaryentry{decomp}{
  name={decomposition},
	description={
		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} can represent the same decisions using different \glspl{variable}, possibly of different types.
	}
}

\newglossaryentry{del-rew}{
  name={delayed rewriting},
  description={A technique using during \gls{rewriting}. It delays the \gls{rewriting} of \glspl{constraint} whose \gls{decomp} might change based on information that can become available later during the process.},
}

\newglossaryentry{domain}{
  name={domain},
  description={A set of value that a \gls{variable} can take without violating any \glspl{constraint} in the problem.},
}

\newglossaryentry{domain-con}{
  name={domain consistent},
  description={A \gls{propagator} is domain consistent if it is able to remove all values from \domains{} that do not occur in a \gls{sol}.},
}

\newglossaryentry{essence}{
  name={Essence},
  description={A \gls{cml} known for its high-level \gls{variable} types. The rewriting process of Essence first transforms an Essence model into \gls{ess-prime}. A \instance{} formed with an \gls{ess-prime} model is then rewritten into a \gls{slv-mod}. See \cref{sub:back-essence}.},
}

\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.},
}

\newglossaryentry{fixed}{
  name={fixed},
  description={A \gls{variable} is said to be fixed when there is only a single possible value that it can take.},
}

\newglossaryentry{fixpoint}{
  name={fix-point},
  description={A set of algorithms is set to be at fix-point when none of the algorithms can further change the overall state.},
}

\newglossaryentry{flatzinc}{
  name={Flat\-Zinc},
  description={A subset of \gls{minizinc} chosen to represent \glspl{slv-mod}. It is the standard format in which \gls{minizinc} communicates with its \glspl{solver}.},
}

\newglossaryentry{gecode}{
  name={Gecode},
  description={A well-known open source \gls{cp} \gls{solver} \autocite{gecode-2021-gecode}.},
}

\newglossaryentry{generator}{
  name={generator},
  description={An expression in \gls{minizinc} that evaluates to a sequence of elements. These elements are then generally used to instantiate an identifier in a \gls{comprehension} expression.},
}

\newglossaryentry{global}{
  name={global constraint},
  description={
		A common \gls{constraint} pattern.
		These patterns can generally extend to any number of \glspl{variable}.
		For example, the well-known global constraint \( AllDifferent(\ldots) \) requires all its arguments to take a different value.
		Global constraints are usually not \gls{native} to a \gls{solver}.
		Instead, the \gls{rewriting} process can enforce the global constraint using a \gls{decomp}.
	}
}

\newglossaryentry{gurobi}{
  name={Gurobi},
  description={A well-known proprietary \gls{mip} \gls{solver} \autocite{gurobi-2021-gurobi}.},
}

\newglossaryentry{half-reif}{
  name={half-reification},
  description={A half-reification is a variation of a \gls{reif} where for a \gls{constraint} \(c\) it enforces that a \gls{cvar} \texttt{b} represents the logical implication of the \gls{constraint}: \(\texttt{b} \rightarrow{} c\).},
}

\newglossaryentry{half-reified}{
  name={half-reified},
  description={See \gls{half-reif}.},
}


\newglossaryentry{incremental-rewriting}{
  name={incremental-rewriting},
  description={The \gls{rewriting} of an \gls{instance} that is continuously changed.},
}

\newglossaryentry{implication-chain}{
  name={implication chain},
  description={Multiple implication \glspl{constraint} linked together through a \glspl{variable} on opposite sides of the implication, such as \mzninline{A -> B} and \mzninline{B -> C}. When a linking \gls{variable} is not used, the \glspl{constraint} can be simplified through the use of \gls{chain-compression}.},
}

\newglossaryentry{int-sol}{
  name={intermediate solution},
  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 a complete \gls{parameter-assignment}.},
}

\newglossaryentry{interpreter}{
  name={interpreter},
  description={
		A computer program that directly executes instructions one at a time.
	}
}

\newglossaryentry{kleene-sem}{
  name={Kleene semantic},
  description={
		A semantic model for treating undefined behaviour in \glspl{cml}.
		Under Kleene semantics an occurrence of undefined behaviour will only cause its surrounding expression to be undefined when its value is required to compute its result.
	}
}

\newglossaryentry{linearization}{
  name={linearization},
  description={The process of \gls{rewriting} a \gls{model} to a mixed integer program.},
}

\newglossaryentry{let}{
  name={let expression},
  description={A scoping mechanism for expressions in \gls{minizinc}. A let expression allows the modeller to introduce \glspl{variable}, and constrain them, to be used only in the subsequent expression.},
}

\newglossaryentry{gls-lcg}{
  name={lazy clause generation},
  description={Types of \gls{solver} that extend \gls{cp} solving with \gls{sat} capabilities. Lazy clause generation \glspl{solver} lazily translate a \gls{cp} model for a \gls{sat} backend. As such, they maintain the pruning ability of a \gls{cp} solver while gaining the ability of \gls{sat} solvers to explain any failures in the search.},
}

\newglossaryentry{gls-lns}{
  name={large neighbourhood search},
  description={
		A \gls{meta-optimization} strategy that repeatedly reduces the \gls{search-space} by applying different \glspl{neighbourhood} often based on a previous \gls{sol}. Large neighbourhood search is a well-known method to quickly improve a \gls{sol}. Large neighbourhood search is not guaranteed to find the \gls{opt-sol} and if it does, then it will be unable to prove that it did.
	}
}

\newglossaryentry{meta-optimization}{
  name={meta-optimization},
  description={
		Methods used to improve on the general techniques used by \glspl{solver} to look for \glspl{sol}, such as \gls{bnb}.
		Meta-optimisation can be used for a myriad of reasons, such as to quickly improving on an existing \gls{sol}, to find a set of diverse \glspl{sol}, or to use of complex or multiple \glspl{objective}.
		Although meta-optimization methods can be implemented by adjusting the search method in a \gls{solver}, they are often emulated through the adjustment of \glspl{slv-mod} based on the results from the \gls{solver}.
	}
}

\newglossaryentry{microzinc}{
  name={Micro\-Zinc},
  description={A subset of \gls{minizinc} used to describe transformations performed during \gls{rewriting}. Notably, well-defined \microzinc{} cannot contain partial expressions or conditions that contain \glspl{variable}.},
}

\newglossaryentry{minisearch}{
  name={Mini\-Search},
  description={
		\textcite{rendl-2015-minisearch} introduced MiniSearch as a way to describe \gls{meta-optimization} methods from within a \gls{minizinc} model.
		The specified \gls{meta-optimization} method would be performed either by repeatedly calling a \gls{solver} with an updated \gls{slv-mod} or using a \gls{solver} extended with a MiniSearch interface.
	}
}

\newglossaryentry{model}{
  name={constraint model},
  description={
		A formalization of a \gls{dec-prb} or an \gls{opt-prb}.
		It is defined in terms of formalized 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{prb-par}.
		The combination of a constraint model and \gls{assignment}s for its \glspl{prb-par} is said to be an \gls{instance} of the constraint model.
	}
}

\newglossaryentry{minizinc}{
  name={Mini\-Zinc},
  description={
		The primary \gls{cml} studied in this thesis.
		MiniZinc is the successor to \gls{zinc} introduced in 2007 \autocite{nethercote-2007-minizinc}.
		An open-source implementation of the language is available \autocite{minizinc-2021-minizinc}.
	}
}

\newglossaryentry{normal-form}{
  name={normal form},
  description={A \gls{trs} has reached its normal form when none of the rewriting rules can be applied.},
}

\newglossaryentry{gls-mip}{
  name={mixed integer programming},
  description={
    A solving technique tries to find the \gls{opt-sol} for a \cmodel{} containing a mixture of Integer and floating point \glspl{variable} subject to \glspl{constraint} in the form of linear (in-)equations.
    Mixed integer programming is extensively studied and there are many successful \glspl{solver} dedicated to solving mixed integer programs.
    See \cref{subsec:back-mip}.
	}
}

\newglossaryentry{native}{
  name={native},
  description={\glspl{constraint} and \gls{variable} types are said to be native to a \gls{solver} when they can be directly used as input for the \gls{solver}.},
}

\newglossaryentry{nanozinc}{
  name={Nano\-Zinc},
  description={A language to represent the current state of an \gls{instance} during \gls{rewriting}.},
}

\newglossaryentry{neighbourhood}{
  name={neighbourhood},
  description={A (small) subset of the \gls{search-space}.},
}

\newglossaryentry{objective}{
  name={objective function},
  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{openwbo}{
  name={OpenWBO},
  description={A well-known \gls{maxsat} \gls{solver} \autocite{martins-2014-openwbo}.},
}

\newglossaryentry{operator}{
  name={operator},
  description={A syntactical symbol used as a shorthand for a function. Prefix operators, such as \mzninline{not}, appear before another expression and are a shorthand for unary functions. Infix operators, such as \mzninline{+}, \mzninline{*}, and \mzninline{div}, appear in between two expressions and are a shorthand for binary functions.},
}

\newglossaryentry{gls-opl}{
  name={OPL:\ The optimization modelling language},
  description={A \gls{cml} aimed at combining the powers of mathematical programming and \gls{cp}. The OPL is excels at the modelling of scheduling problems. See \cref{sub:back-opl}.},
}

\newglossaryentry{opt-prb}{
  name={optimization problem},
  description={
		A decision problem with an additional \gls{objective}.
		It can, likewise, be formalized as a \gls{model}.
		If the problem has multiple \glspl{sol}, then this function can be used to assess the quality on the \gls{sol}.
		For such a problem, an \gls{opt-sol} is a \gls{sol} with the highest quality.
	}
}

\newglossaryentry{optional}{
  name={optional},
  description={When it is not certain if a value, either \gls{variable} or \gls{parameter}, will exist in a \gls{minizinc} \instance{}, its type is marked as optional (\mzninline{opt}). If the value does not occur it is said to be absent.},
}

\newglossaryentry{opt-sol}{
  name={optimal solution},
  description={A \gls{sol} in an \gls{opt-prb} for which it has been proven that other \gls{sol} of higher quality do not exist.},
}

\newglossaryentry{restart}{
  name={restart},
  description={
    A \gls{solver} is said to restart when it abandons all \glspl{search-decision}.
		This can be useful when extra information has come to light in the search for a \gls{sol}.
  }
}

\newglossaryentry{rbmo}{
  name={restart based meta-optimization},
  description={
		A technique to apply \gls{meta-optimization} methods within the \gls{solver}.
		The \gls{solver} is extended with \gls{native} \glspl{constraint} that set \glspl{variable} to a \gls{fixed} value on every \gls{restart}.
		See \cref{sec:inc-modelling,sec:inc-solver-extension}.
  }
}

\newglossaryentry{gls-sat}{
  name={boolean satisfiability},
  description={
    A problem class that tries to find a valid \gls{assignment} for a set of Boolean \glspl{variable} subject to a logical formula.
    Boolean satisfiability is extensively studied and there are many \glspl{solver} dedicated to solving this problem class.
    See \cref{subsec:back-sat}.
  }
}

\newglossaryentry{search-decision}{
  name={search decision},
  description={
    \Glspl{solver} generally make search decisions when they can not directly infer a \gls{sol}.
    The \gls{solver} then assumes a value for a \gls{variable} or adds a \gls{constraint}.
    The decision might have to be revised later.
  }
}

\newglossaryentry{search-heuristic}{
  name={search heuristic},
  description={
    A specification of how to make \glspl{search-decision} in an effort to find \glspl{sol} in a \gls{solver}.
  }
}

\newglossaryentry{search-space}{
  name={search space},
  description={
		The set of possible \glspl{search-decision} in the current state of the \instance{}.
  }
}

\newglossaryentry{sol}{
  name={solution},
  description={A complete \gls{variable-assignment} for an \gls{instance} such that all \glspl{constraint} are satisfied.},
}

\newglossaryentry{solver}{
  name={solver},
  description={
		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}.
	}
}

\newglossaryentry{strict-sem}{
  name={strict semantic},
  description={
		A semantic model for treating undefined behaviour in \glspl{cml}.
		Under strict semantics any occurrence of undefined behaviour will cause the result of the \gls{instance} to be undefined.
	}
}

\newglossaryentry{parameter}{
  name={parameter},
  description={
		Parameter variables, shortened to parameters, are variables in the sense of programming languages, and are not to be confused with \glspl{variable}.
		In \minizinc{}, a parameter variable represents a value that will be known during \gls{rewriting}.
		Examples of such values are \glspl{prb-par}, the result of introspection (such as \mzninline{dom(x)}, returning the current domain of a \gls{variable} \mzninline{x}), or the result of calculations over other parameter variables.
	}
}

\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{prb-par} and \glspl{variable} in a \gls{model}.},
}

\newglossaryentry{prb-par}{
  name={problem parameter},
  description={
		Problem 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}.
		For example, a problem parameter can influence the number of \glspl{constraint} in an \gls{instance}.
	}
}


\newglossaryentry{propagation}{
  name={constraint propagation},
  description={The removal of values from \glspl{domain} of \glspl{variable} that violate a \gls{constraint}. See \cref{subsec:back-cp}.},
}

\newglossaryentry{propagator}{
  name={propagator},
  description={An algorithm that perform \gls{propagation} for a \gls{constraint}.},
}

\newglossaryentry{reif}{
  name={reification},
  description={A reification is a special form of a \gls{constraint} where, instead of the \gls{constraint} \(c\) being enforced in the \glspl{sol}, it enforces that a \gls{cvar} \texttt{b} represents whether the \gls{constraint} holds or not: \(\texttt{b} \leftrightarrow{} c\).},
}

\newglossaryentry{reified}{
  name={reified},
  description={See \gls{reif}.},
}

\newglossaryentry{rel-sem}{
  name={relational semantic},
  description={
		A semantic model for treating undefined behaviour in \glspl{cml}.
		Under relational semantics an occurrence of undefined behaviour will cause its closest surrounding Boolean expression to be \mzninline{false}.
	}
}

\newglossaryentry{rewriting}{
  name={rewriting},
  description={
		The process of transforming a \gls{model} \gls{instance} into an \gls{eqsat} \gls{slv-mod} is referred to as rewriting.
		This happens primarily through the application of \glspl{decomp}.
	}
}

\newglossaryentry{satisfied}{
  name={satisfied},
  description={
		A \gls{constraint} is said to be satisfied when its logical expression is proven to hold.
		Furthermore, a \gls{dec-prb} is said to be satisfied when all its \glspl{constraint} are satisfied.
	}
}

\newglossaryentry{slv-mod}{
  name={solver model},
  description={
		A \gls{instance} of a \gls{model} where all \glspl{constraint} and \gls{variable} types are \gls{native} for the targeted \gls{solver}.
		\Glspl{instance} of \glspl{model} containing non-native \glspl{constraint} and/or \gls{variable} types can be transformed into solver models through the process of \gls{rewriting}.
	}
}

\newglossaryentry{scip}{
  name={SCIP},
  description={A well-known open source \gls{mip} \gls{solver}.},
}

\newglossaryentry{term}{
  name={term},
  description={An expression in a \gls{trs}. A term can have nested sub-expressions.},
}

\newglossaryentry{termination}{
  name={termination},
  description={A property of a \gls{trs}. A system is terminating if it is guaranteed to eventually arrive at a \gls{normal-form}.},
}

\newglossaryentry{trail}{
  name={trail},
  description={A chronological account of changes to data structures with as goal to possibly reverse these changes. The usage of a trail is a common way for \gls{solver} to revisit search decisions (\ie{} \gls{backtrack}).},
}

\newglossaryentry{trs}{
  name={term rewriting system},
  description={A computational model that expresses computation through the application of rewriting rules. A rewriting rule replaces the \glspl{term} on its left-hand side with the \glspl{term} on its right-hand side.},
}

\newglossaryentry{unsat}{
  name={unsatisfiable},
  description={An \gls{instance}, or a \gls{constraint}, is unsatisfiable when a \gls{sol} cannot exist. All possible \glspl{variable-assignment} would violate at least one \gls{constraint}.},
}

\newglossaryentry{variable}{
  name={decision variable},
  description={
		A formalized decision that is yet to be made.
		When searching for a \gls{sol} a decision variable is said to have a certain \gls{domain}, which contains the values that the decision variable can still take.
		If at any point the \gls{domain} is reduced to a single value, then the decision variable is said to be \gls{fixed}.
		If, however, a decision variable has an empty \gls{domain}, then there does not exist a value that is consistent with the \glspl{constraint}.
	}
}

\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={The predecessor of \gls{minizinc}. In comparison to \gls{minizinc}, Zinc contained more features such as pattern matching and tuples, but was not \gls{solver}-independent.},
}