From d771d3ec3eee944cfa29eb19b0648c6a1f39a55b Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Sun, 25 Jul 2021 17:22:30 +1000 Subject: [PATCH] Clear warning on the glossary --- .vscode/ltex.dictionary.en-GB.txt | 1 + .vscode/ltex.hiddenFalsePositives.en-GB.txt | 77 ++++++ assets/glossary.tex | 270 ++++++++++---------- assets/packages.tex | 2 +- 4 files changed, 214 insertions(+), 136 deletions(-) diff --git a/.vscode/ltex.dictionary.en-GB.txt b/.vscode/ltex.dictionary.en-GB.txt index 6c7cc5f..1a9b128 100644 --- a/.vscode/ltex.dictionary.en-GB.txt +++ b/.vscode/ltex.dictionary.en-GB.txt @@ -35,3 +35,4 @@ nullary GBAC RCPSP Reifications +SCIP diff --git a/.vscode/ltex.hiddenFalsePositives.en-GB.txt b/.vscode/ltex.hiddenFalsePositives.en-GB.txt index bb66888..9c21a36 100644 --- a/.vscode/ltex.hiddenFalsePositives.en-GB.txt +++ b/.vscode/ltex.hiddenFalsePositives.en-GB.txt @@ -184,3 +184,80 @@ {"rule":"EN_A_VS_AN","sentence":"^\\QAlthough it does not prove the unsatisfiability of one instance any longer and slightly increases the number of solver errors, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is found for five more instances.\\E$"} {"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qallow us to express important aspects of the meta-optimization algorithm in a more convenient way, and enable a simple \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q scheme that does not require any additional communication with and only small, simple extensions of the target \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} {"rule":"EN_A_VS_AN","sentence":"^\\Q[\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q has not been restarted yet; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q was \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q found a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q found and proved an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in its \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q did not find a solution, but did not exhaust its \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qgls-ast name=Abstract Syntax Tree, description=A tree structure representing the syntactic structure of a piece of computer language.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qavar name=auxiliary variable, description= A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q not explicitly defined in a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, but rather introduced in the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qaggregation name=constraint aggregation, description=A technique that combines many smaller Dummies into a one or, by exception, a few larger Dummies.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-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.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qassignment name=assignment, description= A mapping from Dummies or Dummies to values.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qbacktrack name=backtrack, description=A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is said to backtrack when it revisits a search decision (e.g. a value assumed during search).\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qbnb name=branch and bound, description=A search method to find a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qbooleanization name=Booleanization, description=The process of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q or \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q problem.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-cbc name=COIN-OR Branch-and-Cut, description=A well-known open source \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-cbls name=constraint-based local search, description=A form of local search using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q violations as its \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qcml name=constraint modelling language, description= A computer language used to define Dummies.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qcplex name=CPLEX, description=A well-known proprietary \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q developed by IBM \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-chr name=constraint handling rules, description=A non-deterministic declarative rule based programming language to maintain or improve a constraint store.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-cp name=constraint programming, description= A general technique to find Dummies to Dummies of Dummies.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-cse name=common sub-expression elimination, description=A technique stemming from programming language to avoid duplicate computation.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-clp name=constraint logic programming, description=An extension of logic programming to include the concepts of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qgls-cse name=common sub-expression elimination, description=A technique stemming from programming language to avoid duplicate computation.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qcvar name=control variable, description= A special form of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q represent the result of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"EN_A_VS_AN","sentence":"^\\Qcvar name=control variable, description= A special form of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q represent the result of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qcompiler 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”.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qcompiling name=compiling, description=see \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qdec-prb name=decision problem, description= A problem which can be defined as making a set of decisions under a certain set of rules.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qdecomp name=decomposition, description= A formulation of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in terms of other Dummies in order to reach \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Dummies.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qdel-rew name=delayed rewriting, description=A technique using during \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qeqsat name=equisatisfiable, description=Two Dummies are equisatisfiable when a bijective function can be defined to map the Dummies of one \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q onto the Dummies of the other.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qfixpoint 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.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qflatzinc name=FlatZinc, description=A subset of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q chosen to represent Dummies.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgecode name=Gecode, description=A well-known open source \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qgurobi name=Gurobi, description=A well-known proprietary \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qhalf-reif name=half-reification, description=A half-reification is a variation of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where for a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q it enforces that a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q b represents the logical implication of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"EN_A_VS_AN","sentence":"^\\Qincremental-rewriting name=incremental-rewriting, description=The \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that is continuously changed.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qint-sol name=intermediate solution, description=A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that is not (yet) proven to be the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"EN_A_VS_AN","sentence":"^\\Qint-sol name=intermediate solution, description=A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that is not (yet) proven to be the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qkleene-sem name=Kleene semantic, description= A semantic model for treating undefined behaviour in Dummies.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qlinearization name=linearization, description=The process of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to a mixed integer program.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-lcg name=lazy clause generation, description=Types of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that extend \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q solving with \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q capabilities.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-lns name=large neighbourhood search, description= A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q strategy that repeatedly reduces the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q by applying different Dummies often based on a previous \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qmeta-optimization name=meta-optimization, description= Methods used to improve on the general techniques used by Dummies to look for Dummies, such as \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qmicrozinc name=MicroZinc, description=A subset of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q used to describe transformations performed during \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qminisearch name=MiniSearch, description= \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q introduced MiniSearch as a way to describe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q methods from within a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qmodel name=constraint model, description= A formalization of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q or an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"EN_A_VS_AN","sentence":"^\\QThe combination of a constraint model and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Qs for its Dummies is said to be an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the constraint model.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qminizinc name=MiniZinc, description= The primary \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q studied in this thesis.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qnormal-form name=normal form, description=A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q has reached its normal form when none of the rewriting rules can be applied.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-mip name=mixed integer programming, description= A solving technique tries to find the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q containing a mixture of Integer and floating point Dummies subject to Dummies in the form of linear (in-)equations.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qnative name=native, description=Dummies and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q types are said to be native to a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q when they can be directly used as input for the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qnanozinc name=NanoZinc, description=A language to represent the current state of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q during \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"EN_A_VS_AN","sentence":"^\\Qnanozinc name=NanoZinc, description=A language to represent the current state of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q during \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qopenwbo name=OpenWBO, description=A well-known \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-opl name=OPL: The optimization modelling language, description=A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q aimed at combining the powers of mathematical programming and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qopt-prb name=optimization problem, description= A decision problem with an additional \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"EN_A_VS_AN","sentence":"^\\QFor such a problem, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q with the highest quality.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qoptional name=optional, description=When it is not certain if a value, either \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q or \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, will exist in a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, its type is marked as optional (\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q).\\E$"} +{"rule":"EN_A_VS_AN","sentence":"^\\Qopt-sol name=optimal solution, description=A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for which it has been proven that other \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of higher quality do not exist.,\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qrbmo name=restart based meta-optimization, description= A technique to apply \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q methods within the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qgls-sat name=boolean satisfiability, description= A problem class that tries to find a valid \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for a set of Boolean Dummies subject to a logical formula.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qsearch-decision name=search decision, description= Dummies generally make search decisions when they can not directly infer a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qsearch-heuristic name=search heuristic, description= A specification of how to make Dummies in an effort to find Dummies in a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qsearch-space name=search space, description= The set of possible Dummies in the current state of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qsol name=solution, description=A complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q such that all Dummies are satisfied.,\\E$"} +{"rule":"EN_A_VS_AN","sentence":"^\\Qsol name=solution, description=A complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q such that all Dummies are satisfied.,\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qstrict-sem name=strict semantic, description= A semantic model for treating undefined behaviour in Dummies.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qparameter name=parameter, description= Parameter variables, shortened to parameters, are variables in the sense of programming languages, and are not to be confused with Dummies.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qparameter-assignment name=parameter assignment, description=see \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q,\\E$"} +{"rule":"EN_A_VS_AN","sentence":"^\\QSimilarly, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is said to be partial when it maps only a subset of the Dummies and Dummies in a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"EN_A_VS_AN","sentence":"^\\QFor example, a problem parameter can influence the number of Dummies in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qprb-par name=problem parameter, description= Problem parameters are part of the external input for a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qpropagation name=constraint propagation, description=The removal of values from Dummies of Dummies that violate a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qreif name=reification, description=A reification is a special form of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where, instead of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q being enforced in the Dummies, it enforces that a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q b represents whether the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q holds or not: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qrel-sem name=relational semantic, description= A semantic model for treating undefined behaviour in Dummies.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qrewriting name=rewriting, description= The process of transforming a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q into an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is referred to as rewriting.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qsatisfied name=satisfied, description= A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is said to be satisfied when its logical expression is proven to hold.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qslv-mod name=solver model, description= A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where all Dummies and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q types are \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for the targeted \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qscip name=SCIP, description=A well-known open source \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qtrs name=term rewriting system, description=A computational model that expresses computation through the application of rewriting rules.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qunsat name=unsatisfiable, description=An \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, or a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, is unsatisfiable when a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q cannot exist.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qvariable-assignment name=variable assignment, description=see \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} diff --git a/assets/glossary.tex b/assets/glossary.tex index 7c4b609..2f30e12 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -3,19 +3,19 @@ \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}}, + 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}}, + 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 - }, + 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}{ @@ -24,102 +24,102 @@ 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} - }, + 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}}, + 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}, + 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}}, + 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}, + 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} - }, + 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}, + 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}}, + 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}}, + 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}, + 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}, + 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}}, + 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}}, + 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}, + 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}}, + 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}}, + 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}}, + 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}}, + 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}, + description={A formalized rule of a problem. Constraints are generally expressed in terms of Boolean logic.}, } \newglossaryentry{cml}{ @@ -128,23 +128,23 @@ 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} - }, + 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}}, + 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}}, + 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}}, + 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}{ @@ -152,38 +152,38 @@ 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} - }, + 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}}, + 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}}, + 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} - }, + 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 - }, + The goal of this transformation is generally to create an executable version of the program. + } } \newglossaryentry{compiling}{ name={compiling}, - description={see \gls{compiler}}, + description={see \gls{compiler}.}, } \newglossaryentry{dec-prb}{ @@ -191,60 +191,60 @@ 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 - }, + 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}, + 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}, + 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}}, + 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}}, + 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}, + 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}, + 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}, + 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}}, + 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}}, + description={A well-known open source \gls{cp} \gls{solver} \autocite{gecode-2021-gecode}.}, } \newglossaryentry{generator}{ @@ -259,81 +259,81 @@ 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} - }, + 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}}, + 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\)}, + 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}}, + description={See \gls{half-reif}.}, } \newglossaryentry{incremental-rewriting}{ name={incremental-rewriting}, - description={The \gls{rewriting} of an \gls{instance} that is continuously changed}, + 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}}, + 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}}, + 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}}, + 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 - }, + 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 - }, + 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}, + 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}, + 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}, + 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 - }, + 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}{ @@ -341,21 +341,21 @@ 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} - }, + 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} }, + 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 - }, + 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}{ @@ -364,8 +364,8 @@ 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 - }, + 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}{ @@ -373,13 +373,13 @@ 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} - }, + 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}, + description={A \gls{trs} has reached its normal form when none of the rewriting rules can be applied.}, } \newglossaryentry{gls-mip}{ @@ -387,43 +387,43 @@ 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} - }, + 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}}, + 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}}, + 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}}, + 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}}, + 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}}, + 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}, + 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}}, + 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}{ @@ -432,26 +432,26 @@ 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 - }, + 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}, + 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}, + 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} - }, + This can be useful when extra information has come to light in the search for a \gls{sol}. + } } \newglossaryentry{rbmo}{ @@ -459,8 +459,8 @@ 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} - }, + See \cref{sec:inc-modelling,sec:inc-solver-extension}. + } } \newglossaryentry{gls-sat}{ @@ -468,8 +468,8 @@ 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} - }, + See \cref{subsec:back-sat}. + } } \newglossaryentry{search-decision}{ @@ -477,27 +477,27 @@ 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 - }, + 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{} - }, + 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}, + description={A complete \gls{variable-assignment} for an \gls{instance} such that all \glspl{constraint} are satisfied.}, } \newglossaryentry{solver}{ @@ -505,16 +505,16 @@ 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} - }, + 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 - }, + Under strict semantics any occurrence of undefined behaviour will cause the result of the \gls{instance} to be undefined. + } } \newglossaryentry{parameter}{ @@ -523,7 +523,7 @@ 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}{ @@ -533,7 +533,7 @@ \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}}, + 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}{ @@ -541,91 +541,91 @@ 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} - }, + 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}}, + 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}}, + 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\)}, + 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}}, + 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} - }, + 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} - }, + 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 - }, + 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} - }, + \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}}, + 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}, + 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}}, + 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})}, + 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}, + 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}}, + 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}{ @@ -634,21 +634,21 @@ 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} - }, + 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}}, + 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}, + 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}, + 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.}, } diff --git a/assets/packages.tex b/assets/packages.tex index 360bc90..8f47578 100644 --- a/assets/packages.tex +++ b/assets/packages.tex @@ -62,7 +62,7 @@ \usepackage{booktabs} % Glossary / Acronyms -\usepackage[acronym,toc]{glossaries} +\usepackage[acronym,toc,nopostdot]{glossaries} \glsdisablehyper % Comment for debugging \usepackage[stylemods=bookindex]{glossaries-extra} \usepackage{titlecaps}