Tiny reformatting

This commit is contained in:
Jip J. Dekker 2021-06-24 19:39:44 +10:00
parent 574a40ea43
commit 5699b08621
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3

View File

@ -694,26 +694,22 @@ trailing.
\subsection{Incremental Solving} \subsection{Incremental Solving}
Ideally, the incremental changes made by the interpreter would also be applied Ideally, the incremental changes made by the interpreter would also be applied incrementally to the solver.
incrementally to the solver. This requires the solver to support both the This requires the solver to support both the dynamic addition and removal of variables and constraints.
dynamic addition and removal of variables and constraints. While some solvers While some solvers can support this functionality, most solvers have limitations.
can support this functionality, most solvers have limitations. The system can The system can therefore support solvers with different levels of an incremental interface:
therefore support solvers with different levels of an incremental interface:
\begin{itemize} \begin{itemize}
\item Using a non-incremental interface, the solver is reinitialised with the
updated \nanozinc\ program every time. In this case, we still get a \item Using a non-incremental interface, the solver is reinitialised with the updated \nanozinc\ program every time.
performance benefit from the improved flattening time, but not from In this case, we still get a performance benefit from the improved flattening time, but not from incremental solving.
incremental solving.
\item Using a \textit{warm-starting} interface, the solver is reinitialised \item Using a \textit{warm-starting} interface, the solver is reinitialised with the updated program as above, but it is also given a previous solution to initialise some internal data structures.
with the updated program as above, but it is also given a previous solution In particular for mathematical programming solvers, this can result in dramatic performance gains compared to ``cold-starting'' the solver every time.
to initialise some internal data structures. In particular for mathematical
programming solvers, this can result in dramatic performance gains compared \item Using a fully incremental interface, the solver is instructed to apply the changes made by the interpreter.
to ``cold-starting'' the solver every time. In this case, the trail data structure is used to compute the set of \nanozinc\ changes since the last choice point.
\item Using a fully incremental interface, the solver is instructed to apply
the changes made by the interpreter. In this case, the trail data structure
is used to compute the set of \nanozinc\ changes since the last choice
point.
\end{itemize} \end{itemize}