Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Description for complete

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-20 15:18:33 +10:00
parent 584b9ef664
commit 4ff0e5c7b5
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
5 changed files with 76 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
assets/listing/inc_complete.mzn Normal file
View File

@ -0,0 +1,2 @@
predicate complete() = complete_reif(true);
predicate complete_reif(var bool: marker);

18
assets/listing/inc_lex_min.mzn Normal file
View File

@ -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;

19
assets/listing/inc_pareto.mzn Normal file
View File

@ -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])
);

9
assets/listing/inc_sim_ann.mzn Normal file
View File

@ -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;

64
chapters/5_incremental.tex
View File

@ -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}