From 4ff0e5c7b58280fe1747b634899d2b0bfc0c67c8 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 20 Jul 2021 15:18:33 +1000 Subject: [PATCH] Description for complete --- assets/listing/inc_complete.mzn | 2 ++ assets/listing/inc_lex_min.mzn | 18 ++++++++++ assets/listing/inc_pareto.mzn | 19 ++++++++++ assets/listing/inc_sim_ann.mzn | 9 +++++ chapters/5_incremental.tex | 64 +++++++++++++++------------------ 5 files changed, 76 insertions(+), 36 deletions(-) create mode 100644 assets/listing/inc_complete.mzn create mode 100644 assets/listing/inc_lex_min.mzn create mode 100644 assets/listing/inc_pareto.mzn create mode 100644 assets/listing/inc_sim_ann.mzn diff --git a/assets/listing/inc_complete.mzn b/assets/listing/inc_complete.mzn new file mode 100644 index 0000000..646863b --- /dev/null +++ b/assets/listing/inc_complete.mzn @@ -0,0 +1,2 @@ +predicate complete() = complete_reif(true); +predicate complete_reif(var bool: marker); diff --git a/assets/listing/inc_lex_min.mzn b/assets/listing/inc_lex_min.mzn new file mode 100644 index 0000000..16370d4 --- /dev/null +++ b/assets/listing/inc_lex_min.mzn @@ -0,0 +1,18 @@ +predicate lex_minimize(array[int] of var int: o) = + let { + var min(index_set(o))..max(index_set(o))+1: stage; + } in if status() = START then + stage = min(index_set(o)) + elseif status() = UNSAT then + stage = lastval(stage) + 1 + else /* status() = SAT */ + stage = lastval(stage) + /\ o[stage] < sol(o[stage]) + endif + /\ _objective = o[stage]; + /\ forall(i in min(index_set(o))..stage-1) ( + o[i] = sol(o[i]) + ) + /\ if stage > max(index_set(o)) then + complete() + endif; diff --git a/assets/listing/inc_pareto.mzn b/assets/listing/inc_pareto.mzn new file mode 100644 index 0000000..00d3fb1 --- /dev/null +++ b/assets/listing/inc_pareto.mzn @@ -0,0 +1,19 @@ +predicate pareto_optimal(var int: obj1, var int: obj2) = + let { + int: ms = 1000; % max solutions + var 0..ms: nsol; % number of solutions + set of int: SOL = 1..ms; + array[SOL] of var lb(obj1)..ub(obj1): s1; + array[SOL] of var lb(obj2)..ub(obj2): s2; + } in if status() = START then + nsol = 0 + elseif status() = UNSAT then + complete() % we are finished! + elseif + nsol = sol(nsol) + 1 /\ + s1[nsol] = sol(obj1) /\ + s2[nsol] = sol(obj2) + endif + /\ for(i in 1..nsol) ( + obj1 < lastval(s1[i]) \/ obj2 < lastval(s2[i]) + ); diff --git a/assets/listing/inc_sim_ann.mzn b/assets/listing/inc_sim_ann.mzn new file mode 100644 index 0000000..0d08a17 --- /dev/null +++ b/assets/listing/inc_sim_ann.mzn @@ -0,0 +1,9 @@ +predicate simulated_annealing(float: init_temp, float: cooling_rate) = + let { + var float: temp; + } in if status() = START then + temp = init_temp + else + temp = last_val(temp) * (1 - cooling_rate) % cool down + /\ _objective < sol(_objective) - ceil(log(uniform(0.0, 1.0)) * temp) + endif; diff --git a/chapters/5_incremental.tex b/chapters/5_incremental.tex index 17b172b..65171e2 100644 --- a/chapters/5_incremental.tex +++ b/chapters/5_incremental.tex @@ -215,21 +215,23 @@ When using this strategy, the \glspl{sol} that the \solver{} finds are no longer Instead, we ask the \solver{} to find a \gls{sol} that is a significant improvement over the previous \gls{sol}. Over time, we decrease the amount by which we require the \gls{sol} needs to improve until we are just looking for any improvements. This \gls{meta-optimisation} can help improve the qualities of \gls{sol} quickly and thereby reaching the \gls{opt-sol} quicker. -This strategy is also easy to express using \gls{rbmo} as follows. +\Cref{lst:inc-sim-ann} show how this strategy is also easy to express using \gls{rbmo}. + +\begin{listing} + \mznfile{assets/listing/inc_sim_ann.mzn} + \caption{\label{lst:inc-sim-ann}A predicate implementing a simulated annealing search.} +\end{listing} + +So far, the algorithms used have been for versions of incomplete search or we have trusted the \solver{} to know when to stop searching. +However, for the following algorithms the \solver{} will (or should) not be able to determine whether the search is complete. +Instead, we introduce the following function that can be used to signal to the solver that the search is complete. \begin{mzn} - predicate simulated_annealing(float: init_temp, float: cooling_rate) = - let { - var float: temp; - } in if status() = START then - temp = init_temp - else - temp = last_val(temp) * (1 - cooling_rate) % cool down - /\ _objective < sol(_objective) - ceil(log(uniform(0.0, 1.0)) * temp) - endif; + function var bool: complete(); \end{mzn} -\todo{introduce the complete() predicate} +\noindent{}When the result of this function is said to be \mzninline{true}, then search is complete. +If any \gls{sol} was found, it is declared an \gls{opt-sol}. Using the same methods it is also possible to describe optimisation strategies with multiple \glspl{objective}. An example of such a strategy is lexicographic search. @@ -252,29 +254,12 @@ Our search is thus complete. There is not always a clear order of importance for different \glspl{objective} in a problem. We can instead look for a number of diverse \glspl{sol} and allow the user to pick the most acceptable options. -The following fragment shows a \gls{meta-optimisation} for the Pareto optimality of a pair of \glspl{objective}. +The predicate in \cref{lst:inc-pareto} shows a \gls{meta-optimisation} for the Pareto optimality of a pair of \glspl{objective}. -\begin{mzn} - predicate pareto_optimal(var int: obj1, var int: obj2) = - let { - int: ms = 1000; % max solutions - var 0..ms: nsol; % number of solutions - set of int: SOL = 1..ms; - array[SOL] of var lb(obj1)..ub(obj1): s1; - array[SOL] of var lb(obj2)..ub(obj2): s2; - } in if status() = START then - nsol = 0 - elseif status() = UNSAT then - complete() % we are finished! - elseif - nsol = sol(nsol) + 1 /\ - s1[nsol] = sol(obj1) /\ - s2[nsol] = sol(obj2) - endif - /\ for(i in 1..nsol) ( - obj1 < lastval(s1[i]) \/ obj2 < lastval(s2[i]) - ); -\end{mzn} +\begin{listing} + \mznfile{assets/listing/inc_pareto.mzn} + \caption{\label{lst:inc-pareto}A predicate implementing pareto optimality search for two \glspl{objective}.} +\end{listing} In this implementation we keep track of the number of \glspl{sol} found so far using \mzninline{nsol}. There is a maximum number we can handle, \mzninline{ms}. @@ -332,7 +317,6 @@ It simply replaces the functional form by a predicate \mzninline{status} (declar \caption{\label{lst:6-status} MiniZinc definition of the \mzninline{status} function} \end{listing} - \paragraph{\mzninline{sol} and \mzninline{last_val}} The \mzninline{sol} function is overloaded for different types. @@ -365,9 +349,17 @@ As such, it can be used in combination with other functions, such as \mzninline{ \mzninline{uniform_nbh} function for floats} \end{listing} -\paragraph{Complete} +\paragraph{\mzninline{complete}} -\todo{write something} +The implementation of the \mzninline{complete} function should merely always return the same Boolean \variable{}. +However, since functions returning Boolean \variables{} are equivalent to a predicate, it is actually the \gls{reif} of \mzninline{complete} that gets used. +As such, we can define \mzninline{complete} as shown in \cref{lst:inc-complete}. +Note that the \gls{slv-mod} will actually include the \mzninline{complete_reif} \gls{native} \constraint{}. + +\begin{listing} + \mznfile{assets/listing/inc_complete.mzn} + \caption{\label{lst:inc-complete} MiniZinc definition of the \mzninline{complete} function.} +\end{listing} \subsection{Solver Support for Restart Based Native Constraints}