664 lines
28 KiB
TeX
664 lines
28 KiB
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 \gls{domain} 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}{
|
|
name={bounds},
|
|
description={The minimal and maximum value in the \domain{} of a \variable{}, \ie{} the boundaries of the \domain{}.},
|
|
}
|
|
|
|
\newglossaryentry{boundsr-con}{
|
|
name={bounds($\mathbb{R}$) consistent},
|
|
description={A \gls{propagator} is bounds($\mathbb{R}$) consistent when it tightens the \gls{bounds} such that they could satisfy the \gls{constraint} if it where using rational arithmetic.},
|
|
}
|
|
|
|
\newglossaryentry{boundsz-con}{
|
|
name={bounds($\mathbb{Z}$) consistent},
|
|
description={A \gls{propagator} is bounds($\mathbb{Z}$) consistent when it tightens the \gls{bounds} such that they can satisfy the \gls{constraint}.},
|
|
}
|
|
|
|
\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,chu-2011-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{schulte-2019-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 semantics},
|
|
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 semantics},
|
|
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 semantics},
|
|
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 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.},
|
|
}
|