From ef4fbc658ce14ecee108be290f94bdedda47f5e4 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Wed, 28 Jul 2021 17:14:36 +1000 Subject: [PATCH] Feedback from Julie --- chapters/2_background.tex | 12 ++++++------ chapters/2_background_preamble.tex | 8 +------- chapters/3_rewriting.tex | 4 ++-- chapters/3_rewriting_preamble.tex | 2 +- chapters/4_half_reif.tex | 3 ++- chapters/4_half_reif_preamble.tex | 8 ++++---- chapters/5_incremental.tex | 7 +++---- chapters/5_incremental_preamble.tex | 6 +++--- chapters/6_conclusions.tex | 10 +++++----- 9 files changed, 27 insertions(+), 33 deletions(-) diff --git a/chapters/2_background.tex b/chapters/2_background.tex index 2d756a8..c154ca2 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -12,7 +12,7 @@ A goal shared between all programming languages is to provide a certain level of abstraction to their users. This reduces the complexity of the programming tasks by hiding unnecessary information. For example, an assembly language allows its user to abstract from the machine instructions and memory positions that are used by the hardware. -And, early imperative programming languages, like FORTRAN, were the first to offer abstraction from the processor architecture of the targeted system. +Early imperative programming languages, like FORTRAN, were the first to offer abstraction from the processor architecture of the targeted system. Consequently, in current times, writing a computer program requires little knowledge of how the targeted computer system operates. \textcite{freuder-1997-holygrail} states that the ``Holy Grail'' of programming languages would be where the user merely states the problem, and the computer solves it, and that \constraint{} modelling is one of the biggest steps towards this goal to this day. @@ -26,13 +26,12 @@ Through the variation of \prbpars{}, a \cmodel{} describes a full class of probl A specific problem is captured by an \instance{}, the combination of a \cmodel{} with a complete \gls{parameter-assignment} (i.e., a mapping from all \prbpars{} to a value). The type of problem described by a \cmodel{} is called a \gls{dec-prb}. -The goal of a \gls{dec-prb} is to find a \gls{sol}: a complete \gls{variable-assignment} that satisfies the \constraints{}. -Or, when this is not possible, prove that such an \gls{assignment} cannot exist. +The goal of a \gls{dec-prb} is to find a \gls{sol}: a complete \gls{variable-assignment} that satisfies the \constraints{}, or, when this is not possible, prove that such an \gls{assignment} cannot exist. Many \cmls{} also support the modelling of \glspl{opt-prb}, where a \gls{dec-prb} is augmented with an \gls{objective}. In this case the goal is to find a \gls{sol} that satisfies all \constraints{} while minimizing (or maximizing) the value of the \gls{objective}. Although a \cmodel{} does not contain any instructions on how to find a suitable \gls{sol}, \instances{} of \cmodels{} can generally be given to a dedicated \solver{}. -To solve these \instances{}, however, they can go through a \gls{rewriting} process to arrive at a \gls{slv-mod}, input accepted by a \solver{}. +To solve these \instances{}, however, they can go through a \gls{rewriting} process to arrive at a \gls{slv-mod}, which is the input accepted by a \solver{}. The \solver{} then uses a dedicated algorithm that finds a \gls{sol} that fits the requirements of the \instance{}. \begin{example}% @@ -1620,8 +1619,9 @@ This chapter summarized the key knowledge to understand the \gls{rewriting} \min It introduced the practice of \constraints{} modelling, and the syntax of the \minizinc{} language. We also compared \minizinc{} to other \cmls{} and found many similarities. This indicates that the research presented in this thesis could be used for these languages as well. -Using \cmls{}, a modeller can easily express a problem for a variety of \solver{} programs. +By using \cmls{}, a modeller can easily express a problem for a variety of \solver{} programs. We gave a brief overview of the main methods used by these \solvers{} and their problem formats, to which a \cmodel{} must be rewritten. Finally, we discussed the \gls{rewriting} process central to \cmls{} in more detail, focusing on the \gls{rewriting} conducted by the current implementation of \minizinc{}. -The next chapter presents a more efficient architecture to perform the \gls{rewriting} from \minizinc{} \instances{} to \glspl{slv-mod}, based on a set of formalized rewriting rules that allows better reasoning about functional \constraints{}. +The next chapter is the first of the three main empirical chapters of this thesis. +It presents a more efficient architecture to perform the \gls{rewriting} from \minizinc{} \instances{} to solver models, based on a set of formalized rewriting rules that allows better reasoning about functional \constraints{}. diff --git a/chapters/2_background_preamble.tex b/chapters/2_background_preamble.tex index 614455e..256b583 100644 --- a/chapters/2_background_preamble.tex +++ b/chapters/2_background_preamble.tex @@ -1,11 +1,5 @@ \noindent{}The research presented in this thesis investigates the process of \gls{rewriting} \cmls{}. -This chapter provides the required background information to understand \cmls{}: - -\begin{itemize} - \item How is a \cmodel{} created? - \item What process does a \solver{} employ to solve a \gls{slv-mod}? - \item How is an \instance{} of a \cmodel{} transformed into a \gls{slv-mod}? -\end{itemize} +This chapter provides the required background information to understand constraint modelling languages, including the creation of \cmodels{}, the processes employed to solve a \gls{slv-mod}, and the transformation of a \cmodel{} into a \gls{slv-mod}. In particular, it gives further information about \minizinc{} and discusses the functionality available to create \cmodels{}. It also provides some insight into \solvers{}, discussing the most important techniques used to solve \instances{} of \cmodels{}. diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex index 2fa34a6..1438971 100644 --- a/chapters/3_rewriting.tex +++ b/chapters/3_rewriting.tex @@ -852,13 +852,13 @@ We are convinced, however, that we can get closer to its performance given the r \label{sec:rew-summary} This chapter presented a new architecture for \gls{rewriting} of \minizinc{} \instances{} to \glspl{slv-mod}. -We introduced the intermediate languages \microzinc{} and \nanozinc{}, central to the \gls{rewriting} architecture. +We introduced the intermediate languages \microzinc{} and \nanozinc{}, which are central to the \gls{rewriting} architecture. \minizinc{} is transformed into a set of \microzinc{} definitions and a \nanozinc{} program. Then, a \nanozinc{} program is partially evaluated using \microzinc{} definitions. We presented formal \gls{rewriting} rules applied during this partial evaluation. Continuously applying these rules would result in a correct, but inefficient \gls{slv-mod}. -Therefore, we extended we the partial evaluation using well-known techniques to improve the \gls{slv-mod}: \gls{propagation} is used throughout the rewriting process (possibly to \gls{fixpoint}), calls can be delayed until more information is known, \gls{cse} is used both when evaluating calls and during the \minizinc{} to \microzinc{} transformation, and \constraints{} can be aggregated when beneficial for the \solver{}. +Therefore, we extended the partial evaluation using well-known techniques to improve the \gls{slv-mod}: \gls{propagation} is used throughout the rewriting process, calls can be delayed until more information is known, \gls{cse} is used both when evaluating calls and during the \minizinc{} to \microzinc{} transformation, and \constraints{} can be aggregated when beneficial for the \solver{}. Crucially, the system can correctly remove all unused and irrelevant \variables{} and \constraints{} by \nanozinc{}'s mechanism to attach \constraints{} to the \variable{} they define. The prototype of this architecture is shown to be significantly faster than the current implementation of \minizinc{}. diff --git a/chapters/3_rewriting_preamble.tex b/chapters/3_rewriting_preamble.tex index 7b0e885..b6abdf7 100644 --- a/chapters/3_rewriting_preamble.tex +++ b/chapters/3_rewriting_preamble.tex @@ -15,7 +15,7 @@ We show how this tool chain allows us to: \noindent{}In addition to providing the first formalization and systematic description of rewriting MiniZinc, we will see that the resulting architecture is also significantly more efficient and flexible than the current \minizinc{} system. This chapter is organized as follows. -\Cref{sec:rew-arch} provides a quick overview of the proposed architecture. +\Cref{sec:rew-arch} provides an overview of the proposed architecture. \Cref{sec:rew-micronano} introduces the core of our \gls{rewriting} system using the \microzinc{} and \nanozinc{} languages. These new languages provide a new intermediate representation that enables more efficient \gls{rewriting}. \Cref{sec:rew-simplification} describes how we can perform various processing and simplification steps on this representation Finally, in \cref{sec:rew-experiments} we report on the experimental results of the prototype implementation. diff --git a/chapters/4_half_reif.tex b/chapters/4_half_reif.tex index 0547964..7fd62fa 100644 --- a/chapters/4_half_reif.tex +++ b/chapters/4_half_reif.tex @@ -1200,7 +1200,8 @@ It provided a \microzinc{} analysis that associates each expression with a certa Depending on the context, we then know whether a \constraint{} can remain non-\gls{reified}, can be \gls{half-reified}, or must be \gls{reified}. 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}. +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}. 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}. diff --git a/chapters/4_half_reif_preamble.tex b/chapters/4_half_reif_preamble.tex index a6f6bbc..cc7b0fe 100644 --- a/chapters/4_half_reif_preamble.tex +++ b/chapters/4_half_reif_preamble.tex @@ -1,17 +1,17 @@ \noindent{}Determining whether a \constraint{} has to be \gls{reified} is a crucial decision made during \gls{rewriting}. \minizinc{} allows us to write complex \constraints{} that in the process of \gls{rewriting} result in multiple \constraints{} that reason about each other. However, using a \gls{reif} \(b \leftrightarrow{} c\), that determines whether a \constraint{} \(c\) holds, can slow the \solver{} down. -Even in \gls{cp} \solvers{}, not many \glspl{reif} are \gls{native} to the \solvers{}, and the \glspl{propagator}, for the ones that are, are often weak. -Generally, the \glspl{decomp} of \gls{reified} \constraint{} also result numerous \gls{native} \constraints{} and \variables{}. +Even in \gls{cp} \solvers{}, few \glspl{reif} are \gls{native} to the \solvers{}, and the \glspl{propagator}, for the ones that are, are often weak. +Generally, the \glspl{decomp} of \gls{reified} \constraint{} also result in numerous \gls{native} \constraints{} and \variables{}. It is thus important that \gls{rewriting} avoids the use of \gls{reif}, whenever it is not required. In this chapter we present an extended \gls{reif} analysis to help minimize the required \solver{} effort. Not only does it consider if a \constraint{} must be \gls{reified} or not, but it also considers whether it could instead be \gls{half-reified}. The notion of \gls{half-reif} \(b \rightarrow{} c\) for a \constraint{} \(c\) was introduced by \textcite{feydy-2011-half-reif}. -It is shown \gls{half-reif} can mitigate some problems and expenses of the use of \gls{reif}. +They show that \gls{half-reif} can mitigate some problems and expenses of the use of \gls{reif}. It is not always possible, however, to use a \gls{half-reif} instead of a \gls{reif}. -The authors identify the conditions required for its usage and provide an algorithm that rewrites a subset of the \minizinc{} language using the technique. +They also identify the conditions required for its usage and provide an algorithm that rewrites a subset of the \minizinc{} language using the technique. Crucially, because of the omission of \gls{let} and multiple occurrences of identifiers, this algorithm does not directly generalize to the full \minizinc{} language. This chapter re-evaluates \gls{half-reif} and extends the \gls{rewriting} process to fully support \gls{half-reif} in \minizinc{}. diff --git a/chapters/5_incremental.tex b/chapters/5_incremental.tex index fa6c72b..558dc11 100644 --- a/chapters/5_incremental.tex +++ b/chapters/5_incremental.tex @@ -550,7 +550,6 @@ This includes results of \gls{propagation}, \gls{cse} and other simplifications. Evaluating the second \constraint{} causes the \domain{} of \mzninline{y} to be less than nine. If we now, however, try to remove the first \constraint{}, then it is not just the direct inference on the \domain{} of \mzninline{x} that has to be undone. All consequent effects, in this case, the changes to the \domain{} of \mzninline{y}, also have to be reversed. - \end{example} The addition of \constraints{} that can later be removed is similar to making \glspl{search-decision} in a \gls{cp} \solver{} (see \cref{subsec:back-cp}). @@ -841,9 +840,9 @@ Although new \solver{} functionality is required, this method eliminates the nee We have shown that this method is very efficient, even when compared to an unrealistic ``oracle'' approach that does not require any computations. When required, however, the architecture presented in this thesis can efficiently perform \gls{incremental-rewriting}. -The architecture provides an incremental interface that allows the modeller add and later retract \variables{} and \constraints{} in chronological order. +The architecture provides an incremental interface that allows the modeller to add and later retract \variables{} and \constraints{} in chronological order. Internally, this \gls{rewriting} process is extended to maintain a \gls{trail} to be able to retract \constraints{} and minimize the portion of the \instance{} to be rewritten again. \Gls{incremental-rewriting} is shown to save a significant amount of time, compared to repeatedly \gls{rewriting} the full \instance{}. -We also discussed how incremental changing \gls{slv-mod} can be communicated to the \solver{} at different levels, but could not show a clear benefit of the incremental communication. +We also discussed how incremental changing \gls{slv-mod} can be communicated to the \solver{} at different levels, but we could not show a clear benefit of the incremental communication. -The 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 presents further avenues for research in this area. +The 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. diff --git a/chapters/5_incremental_preamble.tex b/chapters/5_incremental_preamble.tex index eb5766f..b576e15 100644 --- a/chapters/5_incremental_preamble.tex +++ b/chapters/5_incremental_preamble.tex @@ -1,7 +1,7 @@ -\noindent{}In previous chapters we explored \gls{rewriting} as a definitive linear process: an \instance{} of a \cmodel{} is translated into a \gls{slv-mod}, for which a \solver{} produces \glspl{sol}. +\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 repeatedly \gls{rewriting} almost identical \instances{} from scratch may still prove prohibitive. -It warrants direct support from the \cml{} architecture. +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. +\Gls{meta-optimization} warrants direct support from the \cml{} architecture. In this chapter, we introduce the following two methods to provide this support. \begin{itemize} diff --git a/chapters/6_conclusions.tex b/chapters/6_conclusions.tex index d61c368..fc6ab0c 100644 --- a/chapters/6_conclusions.tex +++ b/chapters/6_conclusions.tex @@ -66,7 +66,7 @@ In these \solvers{}, a functionally defined \variable{} can become unused when t 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. \section*{Reasoning about Reification} -Determining whether to a \constraint{} is \gls{reified} is a crucial decision that has to be made during \gls{rewriting}. +Determining whether a \constraint{} is \gls{reified} is a crucial decision that has to be made during \gls{rewriting}. Making the wrong decision can significantly impact \gls{solver} performance. In \cref{ch:half-reif}, we extend our architecture with our second contribution: \textbf{a formal analysis to reason about the \gls{reif} of \constraints{}}. Not only does this analysis reduce the number of required \glspl{reif}, it is the first implementation that also automatically introduces \glspl{half-reif} when possible. @@ -80,18 +80,18 @@ We noted that \gls{half-reif} interacts with some existing simplification techni 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. -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. +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}. Lastly, \glspl{half-reif} can introduce \glspl{implication-chain} that can degrade the performance of the \solver{}. We described a new simplification technique called \gls{chain-compression} that efficiently eliminates these \glspl{implication-chain} where possible. The techniques to automatically introduce \glspl{half-reif} and the simplification techniques have been implemented in both our prototype \gls{rewriting} architecture and the existing \minizinc{} \compiler{}. -These techniques were included in the official release in version 2.3.0. +These techniques were included in the official release of \minizinc{} in version 2.3.0. In support of this, we have modified the \gls{rewriting} libraries of existing \minizinc{} \solvers{} to use \gls{half-reif}. Notably, we have implemented explicit \glspl{decomp} of \gls{half-reified} \constraints{} for \gls{mip} and \gls{sat} \solvers{}. The usage of these \glspl{decomp} significantly reduces the number of \constraints{} in the \gls{slv-mod}. -Additionally, we implemented two \glspl{propagator} of \gls{half-reif} \constraints{}, \mzninline{all_different} and \mzninline{element}, in a state-of-the-art \gls{cp} \solver{}, \gls{chuffed}, to re-evaluate the claims of the original \gls{half-reif} paper. +Additionally, we implemented two \glspl{propagator} of \gls{half-reif} \constraints{}, \mzninline{all_different} and \mzninline{element}, in a state-of-the-art \gls{cp} \solver{}, \gls{chuffed}, to re-evaluate the claims of the original \gls{half-reif} paper \autocite{feydy-2011-half-reif}. In our experiments, we reaffirmed the effectiveness of the \glspl{propagator}, but we showed mixed results for the use of automatic \gls{half-reif} on a larger scale. While it was clearly beneficial for \gls{sat}, other \solvers{} did not seem to enjoy the same benefit and in some cases were even negatively impacted. @@ -119,7 +119,7 @@ Only a single \gls{slv-mod} is created. The changes to the \gls{slv-mod} are iteratively applied within the \solver{}. In our experiments, we have shown that this method is highly effective. -Even compared to an ``oracle'' approach, where the changes are merely read and not computed, this approach is only slightly slower. +When compared to an ``oracle'' approach, where the changes are merely read and not computed, this approach is only slightly slower. Meanwhile, the time required to rewrite the \gls{meta-optimization} descriptions is negligible. It is not always possible to extend a \solver{}, so for these cases we have defined a second method.