Grammar check

.vscode/ltex.dictionary.en-GB.txt

@@ -38,3 +38,4 @@ Reifications
 SCIP
 QCP-Max
 SICStus
+Lille

.vscode/ltex.hiddenFalsePositives.en-GB.txt

@@ -329,3 +329,20 @@
 {"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qsicstus name=SICStus Prolog, description=A well-known implementation of the Prolog \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q language and constraint modelling environment \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"}
 {"rule":"MORFOLOGIK_RULE_EN_GB","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":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model can be rewritten by Savile Row into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for a variety of Dummies, including \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Dummies.\\E$"}
+{"rule":"EN_A_VS_AN","sentence":"^\\QEach algorithm solves an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, adds new Dummies, the resulting \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is solved again, and the Dummies may be removed again.\\E$"}
+{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-cnf name=conjunctive normal form, description=The formulation of a Boolean formula as a conjunction of disjunctions of Boolean literals.\\E$"}
+{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qcomet name=COMET, description=A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q with advanced \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q functionality \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
+{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-maxsat name=Maximum Satisfiability, description=An extension of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q problem class into an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
+{"rule":"EN_A_VS_AN","sentence":"^\\Qgls-maxsat name=Maximum Satisfiability, description=An extension of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q problem class into an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
+{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a problem \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q maximizes the weights of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q clauses.,\\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-comb name=search combinators, description=A language extension proposed for Dummies that allows the modeller to describe search conducted by the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
+{"rule":"EN_A_VS_AN","sentence":"^\\QTo create an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the problem, the modeller provides the number of jobs and machines that are considered, and the duration of each task.\\E$"}
+{"rule":"EN_A_VS_AN","sentence":"^\\QMoreover, the process to encode an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q all happens “behind the scenes”.\\E$"}
+{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe definition of nonoverlap requires that either task A precedes task B, or vice versa.\\E$"}
+{"rule":"EN_A_VS_AN","sentence":"^\\Q\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q also determines how an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is encoded for a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q through function definitions.\\E$"}
+{"rule":"WILL_ALLOW","sentence":"^\\QCrucially, this architecture will allow us to:\\E$"}
+{"rule":"EN_A_VS_AN","sentence":"^\\QThe goal of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is to find a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: a complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that satisfies the Dummies, or, when this is not possible, prove that such an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q cannot exist.\\E$"}
+{"rule":"EN_A_VS_AN","sentence":"^\\QIn previous chapters, we explored \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q as a definitive linear process, where an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is translated into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, for which a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q produces Dummies.\\E$"}
+{"rule":"EN_A_VS_AN","sentence":"^\\QWe allow a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q algorithm, implemented in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q or a scripting language, to make incremental changes to an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
+{"rule":"TOO_LONG_SENTENCE","sentence":"^\\QThe next and final chapter presents the conclusions of this thesis, which reiterate the discoveries and contributions of this research to theory and practice, comment on the scope and limitations of the presented architecture, and present further avenues for research in this area.\\E$"}

assets/glossary.tex

@@ -128,7 +128,7 @@
 
 \newglossaryentry{gls-cnf}{
   name={conjunctive normal form},
-  description={The formulation of a Boolean formula as a conjunction of disjunctions of Boolean literals. This a standardized format for \gls{gls-sat} problems.},
+  description={The formulation of a Boolean formula as a conjunction of disjunctions of Boolean literals. This is a standardized format for \gls{gls-sat} problems.},
 }
 
 \newglossaryentry{constraint}{

chapters/4_half_reif.tex

@@ -93,7 +93,7 @@ Since Boolean expressions in \minizinc{} can be used in, for example, integer ex
 
 To systematically analyse whether Boolean expressions can be \gls{half-reified}, we study the \emph{monotonicity} of \constraints{} w.r.t.\@ an expression.
 A relation \( r(\ldots{}, a, \ldots{}) \) is said to be \emph{monotone} w.r.t.\@ its argument \(a\) when given two possible values for \(a\), \(x\) and \(y\), if \(x \geq{} y\) and all other arguments to \(r\) remain the same, then \(r(\ldots{}, x, \ldots{}) \geq{} r(\ldots{}, y, \ldots{})\).
-The relation is said to be \emph{antitone} w.r.t.\@ its argument \(a\) if given two possible values for \(a\), \(x\) and \(y\), if \(x \geq{} y\) and all other arguments to \(r\) remain the same and all other arguments to \(r\) remain the same, then \(r(\ldots{}, x, \ldots{}) \leq{} r(\ldots{}, y, \ldots{}) \).
+The relation is said to be \emph{antitone} w.r.t.\@ its argument \(a\) if given two possible values for \(a\), \(x\) and \(y\), if \(x \geq{} y\) and all other arguments to \(r\) remain the same, then \(r(\ldots{}, x, \ldots{}) \leq{} r(\ldots{}, y, \ldots{}) \).
 Where, for clarification, we assume \( \false{} < \true{} \).
 
 Using these definitions, we introduce additional distinctions in the context of expressions.
@@ -1201,7 +1201,7 @@ Depending on the context, we then know whether a \constraint{} can remain non-\g
 Notably, the best context cannot always be determined without a complete \gls{parameter-assignment} and \gls{propagation}.
 We showed how this can be corrected through the definitions of the \gls{reif} predicate.
 Finally, we adapted the simplification techniques used during \gls{rewriting} to the use of \gls{half-reif}.
-We corrected \gls{cse} to take the context of an expression into account and we introduced a new simplification technique, \gls{chain-compression}, to eliminate \glspl{implication-chain} introduced by \gls{half-reif}.
+We corrected \gls{cse} to take the context of an expression into account, and we introduced a new simplification technique, \gls{chain-compression}, to eliminate \glspl{implication-chain} introduced by \gls{half-reif}.
 
 To make full use of \gls{half-reif}, we extended \gls{chuffed} with two \glspl{propagator} for \gls{half-reif} \constraints{} that were shown to be effective for certain models.
 We also extended the \minizinc{} \gls{linearization} and \gls{booleanization} libraries to make use of \gls{half-reif} in their \glspl{decomp}.

chapters/5_incremental.tex

@@ -9,9 +9,9 @@
 
 \section{An Introduction to Meta-Optimization}
 
-There are many different kinds of \gls{meta-optimization} algorithms. 
-They share neither a goal or an exact method.
-However, they can often be described through the use of incremental \constraint{} modelling.
+There are many kinds of \gls{meta-optimization} algorithms. 
+They share neither a goal nor an exact method.
+However, many of them be described through the use of incremental \constraint{} modelling.
 Each algorithm solves an \instance{}, adds new \constraints{}, the resulting \instance{} is solved again, and the \constraints{} may be removed again.
 This process is repeated until the goal of the \gls{meta-optimization} algorithm is reached.
 
@@ -522,7 +522,7 @@ In the next section, we discuss how \gls{meta-optimization} can still be efficie
 \label{sec:inc-incremental-compilation}
 
 A common approach to implementing \gls{meta-optimization} algorithms using \cmls{} is through \gls{incremental-rewriting}.
-We allow an \gls{meta-optimization} algorithm, implemented in \minisearch{} or a scripting language, to make incremental changes to an \instance{} of a \cmodel{}.
+We allow a \gls{meta-optimization} algorithm, implemented in \minisearch{} or a scripting language, to make incremental changes to an \instance{} of a \cmodel{}.
 To solve these changing \instances{}, they have to be rewritten repeatedly to \glspl{slv-mod}.
 
 In this section we extend our architecture with an incremental constraint modelling interface that accommodates \gls{incremental-rewriting}.

chapters/5_incremental_preamble.tex

@@ -1,6 +1,6 @@
 \noindent{}In previous chapters, we explored \gls{rewriting} as a definitive linear process, where an \instance{} of a \cmodel{} is translated into a \gls{slv-mod}, for which a \solver{} produces \glspl{sol}.
 However, to solve large-scale real-world problems, we often need to use \gls{meta-optimization} algorithms that solve very similar problems multiple times.
-While improvements of the \gls{rewriting} process, such as the ones discussed in previous chapters, can increase the performance of these approaches, the overhead of completely\gls{rewriting} an almost identical \instances{} time and again may still prove prohibitive.
+While improvements of the \gls{rewriting} process, such as the ones discussed in previous chapters, can increase the performance of these approaches, the overhead of completely\gls{rewriting} an almost identical \instance{} time and again may still prove prohibitive.
 \Gls{meta-optimization} warrants direct support from the \cml{} architecture.
 In this chapter, we introduce the following two methods to provide this support.
 
@@ -20,5 +20,4 @@ We first introduce examples of \gls{meta-optimization} algorithms and how they c
 In \Cref{sec:inc-solver-extension}, we introduce the method to rewrite these \gls{meta-optimization} definitions into efficient \glspl{slv-mod} and the minimal extension required from the target \gls{solver}.
 Then, \Cref{sec:inc-incremental-compilation} introduces the alternative method.
 It extends the architecture presented in the previous chapters with an incremental \constraint{} modelling interface.
-Finally, \Cref{sec:inc-experiments} reports on the experimental results of both approaches.
-
+Finally, \Cref{sec:inc-experiments} reports on the experimental results of both approaches.