From a0b83a5934d93faf88c113bed2b07c73a9f4818f Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Thu, 29 Jul 2021 09:34:18 +1000 Subject: [PATCH] Notes from Andreas --- assets/listing/intro_open_shop.mod | 4 ++-- chapters/1_introduction.tex | 8 ++++---- chapters/3_rewriting.tex | 2 +- chapters/3_rewriting_preamble.tex | 4 ++-- chapters/6_conclusions.tex | 4 ++-- 5 files changed, 11 insertions(+), 11 deletions(-) diff --git a/assets/listing/intro_open_shop.mod b/assets/listing/intro_open_shop.mod index f0e379a..05183a1 100644 --- a/assets/listing/intro_open_shop.mod +++ b/assets/listing/intro_open_shop.mod @@ -8,9 +8,9 @@ var end_time integer >= 0;@\Vlabel{line:intro:var:end}@ minimize goal: end_time;@\Vlabel{line:intro:goal}@ subject to job_excl {m in 1..Machines, j1 in 1..Jobs, j2 in j1+1..Jobs}:@\Vlabel{line:intro:con:start}@ start[m,j1] + Duration[m,j1] <= start[m,j2] - or start[m,j2] + Duration[m,j2] <= start[m,j1]; + or start[m,j2] + Duration[m,j2] <= start[m,j1];@\Vlabel{line:intro:or:first}@ subject to machine_excl {j in 1..Jobs, m1 in 1..Machines, m2 in m1+1..Machines}: start[m1,j] + Duration[m1,j] <= start[m2,j] - or start[m2,j] + Duration[m2,j] <= start[m1,j]; + or start[m2,j] + Duration[m2,j] <= start[m1,j];@\Vlabel{line:intro:or:second}@ subject to push_end_time {m in 1..Machines, j in 1..Jobs}: start[m,j] + Duration[m,j] <= end_time;@\Vlabel{line:intro:con:end}@ diff --git a/chapters/1_introduction.tex b/chapters/1_introduction.tex index 6fc7b88..05c0167 100644 --- a/chapters/1_introduction.tex +++ b/chapters/1_introduction.tex @@ -104,7 +104,7 @@ The \glsxtrshort{ampl} model provides a clear definition of the problem class, b Moreover, the process to encode an \instance{} into a \gls{slv-mod} all happens ``behind the scenes''. The \solver{} cannot specify how, for example, an operator is best rewritten. As such, \glsxtrshort{ampl} cannot rewrite all models for all its \solvers{}. -For example, since the model in \cref{lst:intro-open-shop} uses the \mzninline{or} operator, it can only be encoded for \solvers{} that support \glsxtrshort{ampl}'s \gls{cp} interface. +For example, since the model in \cref{lst:intro-open-shop} uses the \mzninline{or} operator (see lines \ref{line:intro:or:first} and \ref{line:intro:or:second}), it can only be encoded for \solvers{} that support \glsxtrshort{ampl}'s \gls{cp} interface. Although they do support the \gls{rewriting} of models between different problem classes, other traditional \cmls{}, such as \gls{essence} and \glsxtrshort{opl}, exhibit the same problems. They do not provide any way to capture common concepts. @@ -132,7 +132,7 @@ For example, the concepts of one task preceding another and non-overlapping of t The definition of \texttt{non\_overlap} requires that either task A precedes task B, or vice versa. However, unlike the \glsxtrshort{ampl} model, Prolog would not provide this choice to the \solver{}. -Instead, it enforces one, tests if this works, and it otherwise enforces the other. +Instead, it enforces one, tests if this works, and otherwise it enforces the other. This is a powerful mechanism where choices are made in the \gls{rewriting} process, and not in the \solver{}. The problem with the mechanism is that it requires a highly incremental interface with the \solver{} that can incrementally post and retract \constraints{}. @@ -186,7 +186,7 @@ Now, the language is also used to target low-level \solvers{}, such as \gls{sat} For them, the encoding of the same \minizinc{} \instance{} results in a much larger \gls{slv-mod}. Additionally, \minizinc{} is used in progressively more \gls{meta-optimization} toolchains. To a great extent, this is testament to the effectiveness of the language. -However, as they have become more common, these extended uses have revealed weaknesses of the existing \minizinc{} tool chain. +However, as they have become more common, these extended uses have revealed weaknesses of the existing \minizinc{} toolchain. In particular: \begin{itemize} @@ -209,7 +209,7 @@ In particular: \item Monolithic \gls{rewriting} is wasteful. When \minizinc{} is used as part of a \gls{meta-optimization} toolchain, there is typically a large base model, common to all sub-problems, and a small set of \constraints{}, which are added or removed in each iteration. - In the current tool chain, the whole model must be fully rewritten to a \gls{slv-mod} each time. + In the current toolchain, the whole model must be fully rewritten to a \gls{slv-mod} each time. Not only does this repeat all the work done to rewrite the base model, this means a large (sometimes dominant) portion of runtime is simply spent \gls{rewriting} the core model over and over again. This also prevents the \solver{} from carrying over anything it learnt from one problem to the next. diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex index dc208a2..b39207a 100644 --- a/chapters/3_rewriting.tex +++ b/chapters/3_rewriting.tex @@ -44,7 +44,7 @@ The \cmodel{} in the \interpreter{} is internally represented as a \nanozinc{} p \nanozinc{} is a slight extension of the \flatzinc{} format. The \interpreter{} finishes when it reaches a \gls{slv-mod}. -We have developed a prototype of this tool chain, and present experimental validation that the new tool chain can perform \gls{rewriting} much faster, and produce better models, than the current \minizinc{} \compiler{}. +We have developed a prototype of this toolchain, and present experimental validation that the new tool chain can perform \gls{rewriting} much faster, and produce better models, than the current \minizinc{} \compiler{}. \section{\glsentrytext{microzinc} and \glsentrytext{nanozinc}}\label{sec:rew-micronano} diff --git a/chapters/3_rewriting_preamble.tex b/chapters/3_rewriting_preamble.tex index b6abdf7..59f2ea2 100644 --- a/chapters/3_rewriting_preamble.tex +++ b/chapters/3_rewriting_preamble.tex @@ -1,6 +1,6 @@ \noindent{}In this chapter, we develop a new architecture for \gls{rewriting} \minizinc{} into \glspl{slv-mod}. -We describe a new \textbf{systematic view of the execution of \minizinc{}} and build on this to propose a new tool chain. -We show how this tool chain allows us to: +We describe a new \textbf{systematic view of the execution of \minizinc{}} and build on this to propose a new toolchain. +We show how this toolchain allows us to: \begin{itemize} diff --git a/chapters/6_conclusions.tex b/chapters/6_conclusions.tex index fc6ab0c..c7970b9 100644 --- a/chapters/6_conclusions.tex +++ b/chapters/6_conclusions.tex @@ -60,7 +60,7 @@ This could potentially lead to the ability to prove certain properties of the \g Additionally, the architecture introduces reasoning about the transition from \minizinc{} \instances{} to \gls{slv-mod} as two different levels: the transition from \minizinc{} to \microzinc{} and the evaluation of the \nanozinc{} program to create a \gls{slv-mod}. In our prototype we have presented techniques to help improve the quality of the \gls{slv-mod}, but many improvements to these techniques and other techniques may be possible. Finally, we use \nanozinc{} to track \constraints{} that are introduced to define a \variable{}. -Although we have showed how this helps when a \variable{} becomes unused, we not yet investigated if the same information might help improve \solver{} performance. +Although we have showed how this helps when a \variable{} becomes unused, we not yet investigated if the same information can help improve \solver{} performance. A possible example of where this information can be useful is found in \gls{cp} \solvers{}. In these \solvers{}, a functionally defined \variable{} can become unused when the \constraints{} that use \variable{} have already been \gls{satisfied}, independent of its \gls{fixed} value. Like we can remove the defining \constraint{} during \gls{rewriting}, in a \gls{cp} \solver{} we could stop further \gls{propagation} of this \constraint{} and possibly speed up the solving. @@ -79,7 +79,7 @@ Depending on the context of a \constraint{}, we can decide if a \gls{reif} can b We noted that \gls{half-reif} interacts with some existing simplification techniques in the architecture and propose alterations to accommodate them. Foremost, \gls{cse} cannot always reuse the same results for identical \constraints{} any more. It must now also consider the context of the \constraint{}. -For \constraints{} were \gls{cse} is triggered in multiple contexts, we propose rules to either use the result that is acceptable in both contexts, or create such a result. +For \constraints{} where \gls{cse} is triggered in multiple contexts, we propose rules to either use the result that is acceptable in both contexts, or create such a result. Using this adjustment, we ensure that identical \constraints{} are not duplicated and re-use the same \gls{cvar}, even when they occurred in different contexts. The usage of \gls{propagation} can change the context of a \constraint{} during the \gls{rewriting} process. We described how we can communicate this change through the \glspl{cvar} of (half-)\glspl{reif}.