From 5699b0862121359a2b78c12e1af539abc2ecfb41 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Thu, 24 Jun 2021 19:39:44 +1000 Subject: [PATCH] Tiny reformatting --- chapters/5_incremental.tex | 32 ++++++++++++++------------------ 1 file changed, 14 insertions(+), 18 deletions(-) diff --git a/chapters/5_incremental.tex b/chapters/5_incremental.tex index 621571a..a491ba5 100644 --- a/chapters/5_incremental.tex +++ b/chapters/5_incremental.tex @@ -694,26 +694,22 @@ trailing. \subsection{Incremental Solving} -Ideally, the incremental changes made by the interpreter would also be applied -incrementally to the solver. This requires the solver to support both the -dynamic addition and removal of variables and constraints. While some solvers -can support this functionality, most solvers have limitations. The system can -therefore support solvers with different levels of an incremental interface: +Ideally, the incremental changes made by the interpreter would also be applied incrementally to the solver. +This requires the solver to support both the dynamic addition and removal of variables and constraints. +While some solvers can support this functionality, most solvers have limitations. +The system can therefore support solvers with different levels of an incremental interface: \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 - performance benefit from the improved flattening time, but not from - incremental solving. - \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. In particular for mathematical - programming solvers, this can result in dramatic performance gains compared - to ``cold-starting'' the solver every time. - \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. + + \item Using a non-incremental interface, the solver is reinitialised with the updated \nanozinc\ program every time. + In this case, we still get a performance benefit from the improved flattening time, but not from incremental solving. + + \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. + In particular for mathematical programming solvers, this can result in dramatic performance gains compared to ``cold-starting'' the solver every time. + + \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}