More work on constraint programming
This commit is contained in:
parent
771c450ea2
commit
cbec0bea7e
@ -276,6 +276,11 @@
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{propagator}{
|
||||
name={propagator},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{reification}{
|
||||
name={reification},
|
||||
description={},
|
||||
|
@ -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.
|
||||
|
Reference in New Issue
Block a user