Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Enable more grammar rules

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-26 09:35:20 +10:00
parent 1114894da5
commit 87c059609a
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
4 changed files with 18 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.vscode/ltex.hiddenFalsePositives.en-GB.txt vendored
View File

@ -261,3 +261,6 @@
{"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$"}
{"rule":"ACTUAL","sentence":"^\\QHowever, since functions returning Boolean Dummies are equivalent to a predicate, it is actually the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that gets used.\\E$"}
{"rule":"THREE_NN","sentence":"^\\QOur first model is based on a problem of planning cancer radiation therapy treatment using multi-leaf collimators \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"METRIC_UNITS_EN_IMPERIAL","sentence":"^\\Q=15pt =1em\\E$"}

12
.vscode/settings.json vendored
View File

@ -27,9 +27,9 @@
"\\Lrefrange{}{}": "pluralDummy",
"\\lref{}": "dummy",
"\\Lref{}": "dummy",
"\\amplfile{}": "ignore",
"\\mznfile{}": "ignore",
"\\plainfile{}": "ignore",
"\\amplfile[]{}": "ignore",
"\\mznfile[]{}": "ignore",
"\\plainfile[]{}": "ignore",
"\\cmodel{}": "dummy",
"\\cmodels{}": "pluralDummy",
"\\mzninline{}": "dummy",
@ -70,7 +70,10 @@
"\\BeforeBeginEnvironment{}{}": "ignore",
"\\AfterEndEnvironment{}{}": "ignore",
"\\syntax{}": "dummy",
"\\minisearch": "dummy"
"\\minisearch": "dummy",
"\\mznfile{}": "ignore",
"\\plainfile{}": "ignore",
"\\amplfile{}": "ignore"
},
"ltex.latex.environments": {
"mzn": "ignore",
@ -80,4 +83,5 @@
"nzn": "ignore",
"prooftree": "ignore"
},
"ltex.additionalRules.enablePickyRules": true,
}

4
chapters/0_abstract.tex
View File

@ -11,7 +11,7 @@ The \gls{rewriting} required to translate an \instance{} of a \cmodel{} into a \
However, \cmls{} have evolved to include functionality that is not directly supported by the target \solvers{}.
As such, the \gls{rewriting} process has become more important and complex.
\minizinc{}, one such language, was originally designed for constraint programming \solvers{}, whose \glspl{slv-mod} contain small number of highly complex \constraints{}.
\minizinc{}, one such language, was originally designed for constraint programming \solvers{}, whose \glspl{slv-mod} contain a small number of highly complex \constraints{}.
The same \minizinc{} models can now target mixed integer programming and Boolean satisfiability \solvers{}, resulting in numerous very simple \constraints{}.
Distinctively, the \minizinc{}'s \gls{rewriting} process is founded on its functional language.
It generates \glspl{slv-mod} through the application of increasingly complex \minizinc{} functions from \solver{}-specific libraries.
@ -20,7 +20,7 @@ For many applications, the current \minizinc{} implementation now requires a sig
This problem is exacerbated by the emerging use of \gls{meta-optimization} algorithms, which require solving a sequence of closely related \instances{}.
In this thesis we revisit the \gls{rewriting} of functional \cmls{} into \glspl{slv-mod}.
We design and evaluate an architecture for \cmls{} that can accommodate its the modern uses.
We design and evaluate an architecture for \cmls{} that can accommodate its modern uses.
At its core lies a formal execution model that allows us rewrite \cmodels{} efficiently and actively manage the \gls{slv-mod}.
We show how it can better detect and eliminate parts of the model that have become unused.
The architecture is extended using a range of well-known simplification techniques to unsure the quality of the produced \glspl{slv-mod}.

10
chapters/5_incremental.tex
View File

@ -25,7 +25,7 @@ In \minisearch{} these definitions can make use of the following function.
function int: sol(var int: x)
\end{mzn}
It returns the value that variable \mzninline{x} was assigned to in the previous \gls{sol} (similar functions are defined for Boolean, float and set variables).
It returns the value that variable \mzninline{x} was assigned to in the previous \gls{sol} (similar functions are defined for Boolean, float, and set variables).
This allows the \gls{neighbourhood} to be defined in terms of the previous \gls{sol}.
In addition, a \gls{neighbourhood} definition will typically make use of the random number generators available in \minizinc{}.
@ -52,7 +52,7 @@ It then searches for a solution (\mzninline{minimize_bab}) with a given timeout.
If the search does return a new solution, then it commits to that solution, and it becomes available to the \mzninline{sol} function in subsequent iterations.
The \mzninline{lns} function also posts the \constraint{} \mzninline{obj < sol(obj)}, ensuring the objective value in the next iteration is strictly better than that of the current solution.
Although \minisearch{} enables the modeller to express \glspl{neighbourhood} in a declarative way, the definition of the \gls{meta-optimization} algorithm is rather unintuitive and difficult to debug, leading to unwieldy code for defining even simple algorithm.
Although \minisearch{} enables the modeller to express declarative \glspl{neighbourhood}, the definition of the \gls{meta-optimization} algorithm is rather unintuitive and difficult to debug, leading to unwieldy code for defining even simple algorithm.
Furthermore, the \minisearch{} implementation requires either a close integration of the backend \solver{} into the \minisearch{} system, or it drives the solver through the regular text file based \flatzinc{} interface.
This leads to a significant communication overhead.
@ -350,7 +350,7 @@ As such, it can be used in combination with other functions, such as \mzninline{
The implementation of the \mzninline{complete} function should merely always return the same Boolean \variable{}.
However, since functions returning Boolean \variables{} are equivalent to a predicate, it is actually the \gls{reif} of \mzninline{complete} that gets used.
As such, we can define \mzninline{complete} as shown in \cref{lst:inc-complete}.
Note that the \gls{slv-mod} will actually include the \mzninline{complete_reif} \gls{native} \constraint{}.
Note that the \gls{slv-mod} will thus include the \mzninline{complete_reif} \gls{native} \constraint{}.
\begin{listing}
\mznfile{assets/listing/inc_complete.mzn}
@ -489,7 +489,7 @@ In particular, this means that until the first choice point is created \gls{rewr
constraint c;
\end{mzn}
After rewriting it results in the following \nanozinc{} program.
After \gls{rewriting}, it results in the following \nanozinc{} program.
\begin{nzn}
var true: c;
@ -738,7 +738,7 @@ It should be noted that the \gls{rbmo} method is not guaranteed to apply the exa
In this case there is an even more pronounced difference between the incremental methods and the naive method.
It is surprising to see that the application of 1000 \glspl{neighbourhood} using \gls{incremental-rewriting}, still performs very similar to \gls{rewriting} the \gls{rbmo} method.
Again, solving times are similar between all method.
Once again we do not see any real advantage of the use of the incremental \solver{} \gls{api}.
Once again, we do not see any real advantage of the use of the incremental \solver{} \gls{api}.
The advantage in solve time using \gls{rbmo} is more pronounced here, but it is hard to draw conclusions since the \glspl{neighbourhood} of this method are not exactly the same.
\subsection{Summary}