diff --git a/assets/glossary.tex b/assets/glossary.tex index 4c9274e..62114a7 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -276,6 +276,11 @@ description={}, } +\newglossaryentry{propagator}{ + name={propagator}, + description={}, +} + \newglossaryentry{reification}{ name={reification}, description={}, diff --git a/chapters/2_background.tex b/chapters/2_background.tex index c23630b..0efdd29 100644 --- a/chapters/2_background.tex +++ b/chapters/2_background.tex @@ -633,9 +633,26 @@ It is clear that when the value \mzninline{a} is known, then the value of performing an intelligent search by inferring which which values are still feasible for each \gls{variable} \autocite{rossi-2006-cp}. +To find a solution to a given \gls{csp}, a \gls{cp} \gls{solver} will perform a +depth first search. At each node, the \gls{solver} will try and eliminate any +impossible value using a process called \gls{propagation}. For each +\gls{constraint} the \gls{solver} has a chosen algorithm called a +\gls{propagator}. Triggered by changes in the \glspl{domain} of its +\glspl{variable}, the \gls{propagator} will analyse and prune the any values +that are proven to be inconsistent. + +When there are no more triggered \glspl{propagator} and not all \glspl{variable} +have been assigned a value, the \gls{solver} has to make a search decision. It +will bind a \gls{variable} to a value or add a new \gls{constraint}. \begin{example}% \label{ex:back-nqueens} +Consider as an example the N-Queens problem. Given a chess board of size +\(n \times n\), find a placement for \(n\) queen chess pieces such that no queen +can attack another. Meaning only one queen per row, one queen per column, and +one queen per diagonal. + +The problem can be modelled as a \gls{csp} as follows. \begin{mzn} int: n; @@ -646,9 +663,31 @@ feasible for each \gls{variable} \autocite{rossi-2006-cp}. constraint all_different([q[i] - i | i in 1..n]); \end{mzn} +Since we know that there can only be one queen per column, the decision in the +model left to make is, for every queen, where in the column the piece is placed. +The \glspl{constraint} in the model model the remaining rules of the problem: no +two queen can be placed in the same row, no two queen can be place in the same +upward diagonal, and no two queens can be place in the same downward diagonal. +This model can be directly used in most \gls{cp} \glspl{solver}, since integer +\glspl{variable} and a \gls{propagator} are common. + +When solving the problem, initially no values can be eliminated from the +\glspl{domain} of the \glspl{variable}. The first propagation will happen when +the first queen is placed on the board. The search space will then look like +this: + +\jip{insert image of nqueens board with one queen assigned.} + +Now that one queen is placed on the board the propagators for the +\mzninline{all_different} constraints can start propagating. They can eliminate +all values that are on the same row or diagonal as the queen placed on the +board. + +\jip{insert previous image with all impossible moves marked red.} + \end{example} -\paragraph{Constraint Propagation} + \subsection{Mathematical Programming}% \label{subsec:back-mip} @@ -737,7 +776,7 @@ can then be rewritten as linear \glspl{constraint} using the \glspl{variable} integer \glspl{variable} \(q\) are used to represent where the queen is located in each column. To encode the \mzninline{all_different} constraints, the \glspl{indicator-var} \(y\) are inserted to reason about the value of - \(q\). The \cref{line:mip-channel} is used to connect the \(q\) and \(y\) + \(q\). The \cref{line:back-mip-channel} is used to connect the \(q\) and \(y\) \glspl{variable} and make sure that their values correspond. \Cref{line:back-mip-row} ensures that only one queen is placed in the same row.