From e9c7b6ffcafab168f674ceab2c3ab1bd9719ed9a Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Thu, 1 Jul 2021 18:52:03 +1000 Subject: [PATCH] Some initial fixes in background --- chapters/2_background.tex | 33 +++++++++++++++++++-------------- 1 file changed, 19 insertions(+), 14 deletions(-) diff --git a/chapters/2_background.tex b/chapters/2_background.tex index dc44f93..11a9f9d 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -9,14 +9,17 @@ \section{Introduction to Constraint Modelling Languages} \label{sec:back-intro} -A goal shared between all programming languages is to provide a certain level of abstraction: an assembly language allows you to abstract from the binary instructions and memory positions; Low-level imperial languages, like FORTRAN, were the first to allow you to abstract from the processor architecture of the target machine; and nowadays writing a program requires little knowledge of the actual workings of the hardware on which the program is executed. +A goal shared between all programming languages is to provide a certain level of abstraction to its users. +Reduce the complexity by hiding unnecessary information. +For example, an assembly language allows you 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. +Consequently, in current times, writing a computer program requires little knowledge of how the targeted computer system operates. -Freuder 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 \autocite*{freuder-1997-holygrail}. -Different from imperative (and even other declarative) languages, in a \cml{} the modeller does not describe how to solve the problem, but rather provides the problem requirements. -You could say that a constraint model actually describes the solution to the problem. +Freuder 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 \autocite*{freuder-1997-holygrail}. +In \cmls{}, different from imperative (and even other declarative) languages, the modeller does not describe how to solve the problem, but rather provides the problem requirements; therefore, it could be said that a \cmodel{} actually describes the solution to the problem. -In a constraint model, instead of specifying the manner in which we can find the solution, we give a concise description of the problem. -We describe what we already know, the \parameters{}, what we wish to know, the \variables{}, and the relationships that should exist between them, the \constraints{}. +In a \cmodel{}, instead of specifying the manner in which we can find the solution, we give a concise description of the problem. +The elements of a \cmodel include \parameters{}, what we already know; \variables{}, what we wish to know; and \constraints{}, the relationships that should exist between them. This type of combinatorial problem is typically called a \gls{csp}. The goal of a \gls{csp} is to find values for the \variables{} that satisfy the \constraints{} or prove that no such assignment exists. @@ -490,14 +493,16 @@ Triggered by changes in the \glspl{domain} of its \variables{}, the \gls{propaga In the best case scenario, \gls{propagation} will eliminate all impossible values and all \variables{} have been fixed to a single value. In this case we have arrived at a solution. -Often, \gls{propagation} alone will not be enough to find a solution to the problem. -Instead, when no more \glspl{propagator} are triggered (we have reached a \gls{fixpoint}), the \solver{} has to make a search decision. +Often, \gls{propagation} alone will not be enough to find a \gls{sol} and we reach a \gls{fixpoint}, where no more \glspl{propagator} are triggered. +The \solver{} then has to make a search decision. It will fix a \variable{} to a value or add a new \constraint{}. This search decision is an assumption made by the \solver{} in the hope of finding a solution. -If no solution is found using the search decision, then it needs to try making the opposite decision: excluding the chosen value or adding the opposite constraint. +If no solution is found using the search decision, then it needs to try making the opposite decision which requires the exclusion of the chosen value or adding the opposite constraint. -Note that the important difference between values excluded by \gls{propagation} and making search decisions is that value excluded by a \gls{propagator} are guaranteed to not occur in any solution, but values excluded by a search heuristic are merely removed locally and might still be part of a solution. -A \gls{cp} \solver{} is only able to prove that the problem is unsatisfiable by exploring the full search space. +Note that there is an important difference between values excluded by \gls{propagation} and making search decisions. +Values excluded by propagation are guaranteed to not occur in any \gls{sol} +Wereas, values excluded by a search heuristic are merely removed locally and might still be part of a \gls{sol}. +A \gls{cp} \solver{} is only able to prove that the problem is \gls{unsat} by try all possible search decisions. \Gls{propagation} is not only used when starting the search, but also after making each search decision. This means that some \gls{propagation} depends on the search decision. @@ -1433,7 +1438,7 @@ The additional propagation might fix the result of the \gls{reification} of a co If this constraint is not yet rewritten, then the \solver{} will know to use a direct constraint instead of a reified version. Even more important than the Boolean \constraints{}, are equality \constraints{}. -The flattening is in the unique position to \gls{unify} \variables{} when they are found to be equal. +During the \gls{rewriting} process we are in a unique position to perform effective equality \gls{propagation}. Since they both have to take the same value, only a single \variable{} is required in the \flatzinc\ model to represent them both. -Whenever any (recognisable) equality constraint is found during the optimisation phase, it is removed and the two \variables{} are unified. -Once initialised, it is not always possible for \solvers{} to \gls{unify} \variables{} internally. +Whenever any (recognisable) equality constraint is found during the optimisation phase, it is removed and one of the \variables{} is replaced by the other. +Once initialised, it is generally not possible for \solvers{} to perform this replacement internally.