More work on the incremental chapter

This commit is contained in:
Jip J. Dekker 2021-02-24 17:09:07 +11:00
parent ae8be07972
commit a04e3bee7e
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
49 changed files with 407 additions and 237 deletions

8
Pipfile.lock generated
View File

@ -26,15 +26,15 @@
}, },
"minizinc-python": { "minizinc-python": {
"git": "https://github.com/MiniZinc/minizinc-python", "git": "https://github.com/MiniZinc/minizinc-python",
"ref": "5231948b09c4fe8ed3780b3c71abed75d038a759" "ref": "0becdd6e346c1021b26901de44dc1fc7fd9ac48c"
}, },
"pygments": { "pygments": {
"hashes": [ "hashes": [
"sha256:bc9591213a8f0e0ca1a5e68a479b4887fdc3e75d0774e5c71c31920c427de435", "sha256:37a13ba168a02ac54cc5891a42b1caec333e59b66addb7fa633ea8a6d73445c0",
"sha256:df49d09b498e83c1a73128295860250b0b7edd4c723a32e9bc0d295c7c2ec337" "sha256:b21b072d0ccdf29297a82a2363359d99623597b8a265b8081760e4d0f7153c88"
], ],
"index": "pypi", "index": "pypi",
"version": "==2.7.4" "version": "==2.8.0"
} }
}, },
"develop": {} "develop": {}

View File

@ -64,7 +64,7 @@ dedicated algorithms or rewriting rules to better handle the global constraint},
\newglossaryentry{gls-lns}{ \newglossaryentry{gls-lns}{
name={large neighbourhood search}, name={large neighbourhood search},
description={Large Neighbourhood Search (LNS) is a meta-search algorithm that description={Large Neighbourhood Search (LNS) is a meta-search algorithm that
repeatedly restricts the search space, applying a \gls{neighbourhood}, to repeatedly restricts the search space, \ie applying a \gls{neighbourhood}, to
quickly find better solutions to a problem}, quickly find better solutions to a problem},
} }

View File

@ -1,4 +1,4 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{c}{\PYZpc{} Problem parameters} \PY{c}{\PYZpc{} Problem parameters}
\PY{k+kt}{enum}\PY{l+s}{ }\PY{n+nv}{TOYS}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{p}{\PYZob{}}\PY{n+nv}{football}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{tennisball}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{stuffed\PYZus{}lama}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{stuffed\PYZus{}elephant}\PY{p}{\PYZcb{}}\PY{p}{;} \PY{k+kt}{enum}\PY{l+s}{ }\PY{n+nv}{TOYS}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{p}{\PYZob{}}\PY{n+nv}{football}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{tennisball}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{stuffed\PYZus{}lama}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{stuffed\PYZus{}elephant}\PY{p}{\PYZcb{}}\PY{p}{;}
\PY{k+kt}{array}\PY{p}{[}\PY{n+nv}{TOYS}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{toy\PYZus{}joy}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{p}{[}\PY{l+m}{63}\PY{p}{,}\PY{l+s}{ }\PY{l+m}{12}\PY{p}{,}\PY{l+s}{ }\PY{l+m}{50}\PY{p}{,}\PY{l+s}{ }\PY{l+m}{100}\PY{p}{]}\PY{p}{;} \PY{k+kt}{array}\PY{p}{[}\PY{n+nv}{TOYS}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{toy\PYZus{}joy}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{p}{[}\PY{l+m}{63}\PY{p}{,}\PY{l+s}{ }\PY{l+m}{12}\PY{p}{,}\PY{l+s}{ }\PY{l+m}{50}\PY{p}{,}\PY{l+s}{ }\PY{l+m}{100}\PY{p}{]}\PY{p}{;}

View File

@ -1,4 +1,4 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{n+nv}{c}\PY{l+s}{ }\PY{esc}{$\mapsto$}\PY{l+s}{ }\PY{l}{true}\PY{l+s}{ }\PY{esc}{$\sep$}\PY{l+s}{ }\PY{p}{[}\PY{p}{]} \PY{n+nv}{c}\PY{l+s}{ }\PY{esc}{$\mapsto$}\PY{l+s}{ }\PY{l}{true}\PY{l+s}{ }\PY{esc}{$\sep$}\PY{l+s}{ }\PY{p}{[}\PY{p}{]}
\PY{n+nv}{x}\PY{l+s}{ }\PY{esc}{$\mapsto$}\PY{l+s}{ }\PY{n+nf}{mkvar}\PY{p}{(}\PY{o}{\PYZhy{}}\PY{l+m}{10}\PY{o}{..}\PY{l+m}{10}\PY{p}{)}\PY{l+s}{ }\PY{esc}{$\sep$}\PY{l+s}{ }\PY{p}{[}\PY{p}{]} \PY{n+nv}{x}\PY{l+s}{ }\PY{esc}{$\mapsto$}\PY{l+s}{ }\PY{n+nf}{mkvar}\PY{p}{(}\PY{o}{\PYZhy{}}\PY{l+m}{10}\PY{o}{..}\PY{l+m}{10}\PY{p}{)}\PY{l+s}{ }\PY{esc}{$\sep$}\PY{l+s}{ }\PY{p}{[}\PY{p}{]}
\PY{n+nv}{y}\PY{l+s}{ }\PY{esc}{$\mapsto$}\PY{l+s}{ }\PY{n+nf}{mkvar}\PY{p}{(}\PY{o}{\PYZhy{}}\PY{l+m}{10}\PY{o}{..}\PY{l+m}{10}\PY{p}{)}\PY{l+s}{ }\PY{esc}{$\sep$}\PY{l+s}{ }\PY{p}{[}\PY{p}{]} \PY{n+nv}{y}\PY{l+s}{ }\PY{esc}{$\mapsto$}\PY{l+s}{ }\PY{n+nf}{mkvar}\PY{p}{(}\PY{o}{\PYZhy{}}\PY{l+m}{10}\PY{o}{..}\PY{l+m}{10}\PY{p}{)}\PY{l+s}{ }\PY{esc}{$\sep$}\PY{l+s}{ }\PY{p}{[}\PY{p}{]}

View File

@ -1,4 +1,4 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{c}{\PYZpc{} Posted c} \PY{c}{\PYZpc{} Posted c}
\PY{l}{true}\PY{l+s}{ }\PY{esc}{$\lhd$}\PY{l+s}{ }\PY{o}{\PYZhy{}}\PY{p}{[}\PY{n+nv}{c}\PY{p}{]} \PY{l}{true}\PY{l+s}{ }\PY{esc}{$\lhd$}\PY{l+s}{ }\PY{o}{\PYZhy{}}\PY{p}{[}\PY{n+nv}{c}\PY{p}{]}
\PY{c}{\PYZpc{} Propagated c = true} \PY{c}{\PYZpc{} Propagated c = true}

View File

@ -1,8 +1,15 @@
predicate adaptiveUniform(array[int] of var int: x, float: initialDestrRate) = predicate adaptive_uniform(array[int] of var int: x, float: init_rate) =
let { var float: rate; } in let {
if status() = START then rate = initialDestrRate var float: rate;
elseif status() = UNSAT then rate = min(last_val(rate)-0.02,0.6) } in if status() = START then
else rate = max(last_val(rate)+0.02,0.95) rate = init_rate
endif /\ elseif status() = UNSAT then
forall(i in index_set(x)) rate = min(last_val(rate) - 0.02, 0.6)
(if uniform(0.0,1.0) > rate then x[i] = sol(x[i]) else true endif); else
rate = max(last_val(rate) + 0.02, 0.95)
endif
/\ forall(i in index_set(x)) (
if uniform(0.0, 1.0) > rate then
x[i] = sol(x[i])
endif
);

View File

@ -1,10 +1,17 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{adaptiveUniform}\PY{p}{(}\PY{k+kt}{array}\PY{p}{[}\PY{k+kt}{int}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{initialDestrRate}\PY{p}{)}\PY{l+s}{ }\PY{o}{=} \PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{adaptive\PYZus{}uniform}\PY{p}{(}\PY{k+kt}{array}\PY{p}{[}\PY{k+kt}{int}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{init\PYZus{}rate}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{rate}\PY{p}{;}\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in} \PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{START}\PY{l+s}{ }\PY{k}{then}\PY{l+s}{ }\PY{n+nv}{rate}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{initialDestrRate} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{rate}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{elseif}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{UNSAT}\PY{l+s}{ }\PY{k}{then}\PY{l+s}{ }\PY{n+nv}{rate}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nb}{min}\PY{p}{(}\PY{n+nf}{last\PYZus{}val}\PY{p}{(}\PY{n+nv}{rate}\PY{p}{)}\PY{o}{\PYZhy{}}\PY{l+m}{0.02}\PY{p}{,}\PY{l+m}{0.6}\PY{p}{)} \PY{l+s}{ }\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{START}\PY{l+s}{ }\PY{k}{then}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{else}\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{rate}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nb}{max}\PY{p}{(}\PY{n+nf}{last\PYZus{}val}\PY{p}{(}\PY{n+nv}{rate}\PY{p}{)}\PY{o}{+}\PY{l+m}{0.02}\PY{p}{,}\PY{l+m}{0.95}\PY{p}{)} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{rate}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{init\PYZus{}rate}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}\PY{l+s}{ }\PY{o}{/\PYZbs{}} \PY{l+s}{ }\PY{l+s}{ }\PY{k}{elseif}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{UNSAT}\PY{l+s}{ }\PY{k}{then}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{forall}\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{n+nb}{index\PYZus{}set}\PY{p}{(}\PY{n+nv}{x}\PY{p}{)}\PY{p}{)} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{rate}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nb}{min}\PY{p}{(}\PY{n+nf}{last\PYZus{}val}\PY{p}{(}\PY{n+nv}{rate}\PY{p}{)}\PY{l+s}{ }\PY{o}{\PYZhy{}}\PY{l+s}{ }\PY{l+m}{0.02}\PY{p}{,}\PY{l+s}{ }\PY{l+m}{0.6}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{p}{(}\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{uniform}\PY{p}{(}\PY{l+m}{0.0}\PY{p}{,}\PY{l+m}{1.0}\PY{p}{)}\PY{l+s}{ }\PY{o}{\PYZgt{}}\PY{l+s}{ }\PY{n+nv}{rate}\PY{l+s}{ }\PY{k}{then}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{n+nv}{x}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{p}{)}\PY{l+s}{ }\PY{k}{else}\PY{l+s}{ }\PY{l}{true}\PY{l+s}{ }\PY{k}{endif}\PY{p}{)}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{k}{else}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{rate}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nb}{max}\PY{p}{(}\PY{n+nf}{last\PYZus{}val}\PY{p}{(}\PY{n+nv}{rate}\PY{p}{)}\PY{l+s}{ }\PY{o}{+}\PY{l+s}{ }\PY{l+m}{0.02}\PY{p}{,}\PY{l+s}{ }\PY{l+m}{0.95}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}
\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{k}{forall}\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{n+nb}{index\PYZus{}set}\PY{p}{(}\PY{n+nv}{x}\PY{p}{)}\PY{p}{)}\PY{l+s}{ }\PY{p}{(}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{uniform}\PY{p}{(}\PY{l+m}{0.0}\PY{p}{,}\PY{l+s}{ }\PY{l+m}{1.0}\PY{p}{)}\PY{l+s}{ }\PY{o}{\PYZgt{}}\PY{l+s}{ }\PY{n+nv}{rate}\PY{l+s}{ }\PY{k}{then}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{n+nv}{x}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}
\PY{l+s}{ }\PY{l+s}{ }\PY{p}{)}\PY{p}{;}
\end{Verbatim} \end{Verbatim}

View File

@ -1,8 +1,11 @@
array[1..n] of var 1..n: x; % decision variables array[1..n] of var 1..n: x; % decision variables
var int: cost; % objective function var int: cost; % objective function
% ... some constraints defining the problem
% --- some constraints defining the problem ---
% The user-defined LNS strategy % The user-defined LNS strategy
predicate my_lns() = basic_lns(uniformNeighbourhood(x,0.2)); predicate my_lns() = basic_lns(uniform_neighbourhood(x, 0.2));
% Solve using my\_lns, restart every 500 nodes, overall timeout 120 seconds % Solve using my\_lns, restart every 500 nodes, overall timeout 120 seconds
solve ::on_restart("my_lns") ::restart_constant(500) ::timeout(120) solve ::on_restart("my_lns") ::restart_constant(500) ::timeout(120)
minimize cost; minimize cost;

View File

@ -1,9 +1,12 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k+kt}{array}\PY{p}{[}\PY{l+m}{1}\PY{o}{..}\PY{n+nv}{n}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{l+m}{1}\PY{o}{..}\PY{n+nv}{n}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{;}\PY{l+s}{ }\PY{l+s}{ }\PY{c}{\PYZpc{} decision variables} \PY{k+kt}{array}\PY{p}{[}\PY{l+m}{1}\PY{o}{..}\PY{n+nv}{n}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{l+m}{1}\PY{o}{..}\PY{n+nv}{n}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{;}\PY{l+s}{ }\PY{l+s}{ }\PY{c}{\PYZpc{} decision variables}
\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{cost}\PY{p}{;}\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{c}{\PYZpc{} objective function} \PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{cost}\PY{p}{;}\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{c}{\PYZpc{} objective function}
\PY{c}{\PYZpc{} ... some constraints defining the problem}
\PY{c}{\PYZpc{} --- some constraints defining the problem ---}
\PY{c}{\PYZpc{} The user-defined LNS strategy} \PY{c}{\PYZpc{} The user-defined LNS strategy}
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{my\PYZus{}lns}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{basic\PYZus{}lns}\PY{p}{(}\PY{n+nf}{uniformNeighbourhood}\PY{p}{(}\PY{n+nv}{x}\PY{p}{,}\PY{l+m}{0.2}\PY{p}{)}\PY{p}{)}\PY{p}{;} \PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{my\PYZus{}lns}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{basic\PYZus{}lns}\PY{p}{(}\PY{n+nf}{uniform\PYZus{}neighbourhood}\PY{p}{(}\PY{n+nv}{x}\PY{p}{,}\PY{l+s}{ }\PY{l+m}{0.2}\PY{p}{)}\PY{p}{)}\PY{p}{;}
\PY{c}{\PYZpc{} Solve using my\_lns, restart every 500 nodes, overall timeout 120 seconds} \PY{c}{\PYZpc{} Solve using my\_lns, restart every 500 nodes, overall timeout 120 seconds}
\PY{k}{solve}\PY{l+s}{ }\PY{p}{:}\PY{p}{:}\PY{n+nf}{on\PYZus{}restart}\PY{p}{(}\PY{l+s}{\PYZdq{}}\PY{l+s}{my\PYZus{}lns}\PY{l+s}{\PYZdq{}}\PY{p}{)}\PY{l+s}{ }\PY{p}{:}\PY{p}{:}\PY{n+nf}{restart\PYZus{}constant}\PY{p}{(}\PY{l+m}{500}\PY{p}{)}\PY{l+s}{ }\PY{p}{:}\PY{p}{:}\PY{n+nf}{timeout}\PY{p}{(}\PY{l+m}{120}\PY{p}{)} \PY{k}{solve}\PY{l+s}{ }\PY{p}{:}\PY{p}{:}\PY{n+nf}{on\PYZus{}restart}\PY{p}{(}\PY{l+s}{\PYZdq{}}\PY{l+s}{my\PYZus{}lns}\PY{l+s}{\PYZdq{}}\PY{p}{)}\PY{l+s}{ }\PY{p}{:}\PY{p}{:}\PY{n+nf}{restart\PYZus{}constant}\PY{p}{(}\PY{l+m}{500}\PY{p}{)}\PY{l+s}{ }\PY{p}{:}\PY{p}{:}\PY{n+nf}{timeout}\PY{p}{(}\PY{l+m}{120}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{minimize}\PY{l+s}{ }\PY{n+nv}{cost}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{minimize}\PY{l+s}{ }\PY{n+nv}{cost}\PY{p}{;}

View File

@ -1,7 +1,7 @@
var 1..5: s;@ \Vlabel{line:6:status:start}@ var 1..5: s;@ \Vlabel{line:6:status:start}@
constraint status(s); constraint status(s);
var bool b1; var bool b1;
constraint int_ne_reif(s,1,b1); % b1 <-> status()!=START @\Vlabel{line:6:status:end}@ constraint int_ne_reif(s,1,b1); @\Vlabel{line:6:status:end}@ % b1 <-> status() != START
var 0.0..1.0: rnd1;@\Vlabel{line:6:x1:start}@ var 0.0..1.0: rnd1;@\Vlabel{line:6:x1:start}@
constraint float_uniform(0.0,1.0,rnd1); constraint float_uniform(0.0,1.0,rnd1);
@ -11,6 +11,6 @@ var bool: b3;
constraint bool_and(b1,b2,b3); constraint bool_and(b1,b2,b3);
var 1..3: x1; var 1..3: x1;
constraint int_sol(x[1],x1);@\Vlabel{line:6:x1}@ constraint int_sol(x[1],x1);@\Vlabel{line:6:x1}@
% (status()!=START /\ uniform(0.0,1.0)>0.2) -> x[1]=sol(x[1]) % (status() != START /\textbackslash uniform(0.0, 1.0) > 0.2) -> x[1] = sol(x[1])
constraint int_eq_imp(x[1],x1,b3); @\Vlabel{line:6:x1:end}@ constraint int_eq_imp(x[1],x1,b3); @\Vlabel{line:6:x1:end}@
@...@ @...@

View File

@ -1,8 +1,8 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k+kt}{var}\PY{l+s}{ }\PY{l+m}{1}\PY{o}{..}\PY{l+m}{5}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{s}\PY{p}{;}\PY{esc}{ \Vlabel{line:6:status:start}} \PY{k+kt}{var}\PY{l+s}{ }\PY{l+m}{1}\PY{o}{..}\PY{l+m}{5}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{s}\PY{p}{;}\PY{esc}{ \Vlabel{line:6:status:start}}
\PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{n+nv}{s}\PY{p}{)}\PY{p}{;} \PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{n+nv}{s}\PY{p}{)}\PY{p}{;}
\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{bool}\PY{l+s}{ }\PY{n+nv}{b1}\PY{p}{;} \PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{bool}\PY{l+s}{ }\PY{n+nv}{b1}\PY{p}{;}
\PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{int\PYZus{}ne\PYZus{}reif}\PY{p}{(}\PY{n+nv}{s}\PY{p}{,}\PY{l+m}{1}\PY{p}{,}\PY{n+nv}{b1}\PY{p}{)}\PY{p}{;}\PY{l+s}{ }\PY{c}{\PYZpc{} b1 <-> status()!=START @\Vlabel{line:6:status:end}@} \PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{int\PYZus{}ne\PYZus{}reif}\PY{p}{(}\PY{n+nv}{s}\PY{p}{,}\PY{l+m}{1}\PY{p}{,}\PY{n+nv}{b1}\PY{p}{)}\PY{p}{;}\PY{l+s}{ }\PY{esc}{\Vlabel{line:6:status:end}}\PY{l+s}{ }\PY{c}{\PYZpc{} b1 <-> status() != START}
\PY{k+kt}{var}\PY{l+s}{ }\PY{l+m}{0.0}\PY{o}{..}\PY{l+m}{1.0}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{rnd1}\PY{p}{;}\PY{esc}{\Vlabel{line:6:x1:start}} \PY{k+kt}{var}\PY{l+s}{ }\PY{l+m}{0.0}\PY{o}{..}\PY{l+m}{1.0}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{rnd1}\PY{p}{;}\PY{esc}{\Vlabel{line:6:x1:start}}
\PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{float\PYZus{}uniform}\PY{p}{(}\PY{l+m}{0.0}\PY{p}{,}\PY{l+m}{1.0}\PY{p}{,}\PY{n+nv}{rnd1}\PY{p}{)}\PY{p}{;} \PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{float\PYZus{}uniform}\PY{p}{(}\PY{l+m}{0.0}\PY{p}{,}\PY{l+m}{1.0}\PY{p}{,}\PY{n+nv}{rnd1}\PY{p}{)}\PY{p}{;}
@ -12,7 +12,7 @@
\PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{bool\PYZus{}and}\PY{p}{(}\PY{n+nv}{b1}\PY{p}{,}\PY{n+nv}{b2}\PY{p}{,}\PY{n+nv}{b3}\PY{p}{)}\PY{p}{;} \PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{bool\PYZus{}and}\PY{p}{(}\PY{n+nv}{b1}\PY{p}{,}\PY{n+nv}{b2}\PY{p}{,}\PY{n+nv}{b3}\PY{p}{)}\PY{p}{;}
\PY{k+kt}{var}\PY{l+s}{ }\PY{l+m}{1}\PY{o}{..}\PY{l+m}{3}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{x1}\PY{p}{;} \PY{k+kt}{var}\PY{l+s}{ }\PY{l+m}{1}\PY{o}{..}\PY{l+m}{3}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{x1}\PY{p}{;}
\PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{int\PYZus{}sol}\PY{p}{(}\PY{n+nv}{x}\PY{p}{[}\PY{l+m}{1}\PY{p}{]}\PY{p}{,}\PY{n+nv}{x1}\PY{p}{)}\PY{p}{;}\PY{esc}{\Vlabel{line:6:x1}} \PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{int\PYZus{}sol}\PY{p}{(}\PY{n+nv}{x}\PY{p}{[}\PY{l+m}{1}\PY{p}{]}\PY{p}{,}\PY{n+nv}{x1}\PY{p}{)}\PY{p}{;}\PY{esc}{\Vlabel{line:6:x1}}
\PY{c}{\PYZpc{} (status()!=START /\ uniform(0.0,1.0)>0.2) -> x[1]=sol(x[1])} \PY{c}{\PYZpc{} (status() != START /\textbackslash uniform(0.0, 1.0) > 0.2) -> x[1] = sol(x[1])}
\PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{int\PYZus{}eq\PYZus{}imp}\PY{p}{(}\PY{n+nv}{x}\PY{p}{[}\PY{l+m}{1}\PY{p}{]}\PY{p}{,}\PY{n+nv}{x1}\PY{p}{,}\PY{n+nv}{b3}\PY{p}{)}\PY{p}{;}\PY{l+s}{ }\PY{esc}{\Vlabel{line:6:x1:end}} \PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{int\PYZus{}eq\PYZus{}imp}\PY{p}{(}\PY{n+nv}{x}\PY{p}{[}\PY{l+m}{1}\PY{p}{]}\PY{p}{,}\PY{n+nv}{x1}\PY{p}{,}\PY{n+nv}{b3}\PY{p}{)}\PY{p}{;}\PY{l+s}{ }\PY{esc}{\Vlabel{line:6:x1:end}}
\PY{esc}{...} \PY{esc}{...}
\end{Verbatim} \end{Verbatim}

View File

@ -0,0 +1 @@
predicate basic_lns(var bool: nbh) = (status()!=START -> nbh);

View File

@ -0,0 +1,3 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{basic\PYZus{}lns}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{bool}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{nbh}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{p}{(}\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{o}{!=}\PY{n+nv}{START}\PY{l+s}{ }\PY{o}{\PYZhy{}\PYZgt{}}\PY{l+s}{ }\PY{n+nv}{nbh}\PY{p}{)}\PY{p}{;}
\end{Verbatim}

View File

@ -1,4 +1,4 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{c}{\PYZpc{} TODO: We probably need to unify these (at least for the thesis)} \PY{c}{\PYZpc{} TODO: We probably need to unify these (at least for the thesis)}
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{random\PYZus{}allocation}\PY{p}{(}\PY{k+kt}{array}\PY{p}{[}\PY{k+kt}{int}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{sol}\PY{p}{)}\PY{l+s}{ }\PY{o}{=} \PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{random\PYZus{}allocation}\PY{p}{(}\PY{k+kt}{array}\PY{p}{[}\PY{k+kt}{int}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{sol}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{forall}\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{n+nv}{courses}\PY{p}{)}\PY{l+s}{ }\PY{p}{(} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{forall}\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{n+nv}{courses}\PY{p}{)}\PY{l+s}{ }\PY{p}{(}

View File

@ -1,3 +1 @@
predicate hill_climbing() = predicate hill_climbing() = status() != START -> _objective < sol(_objective);
if status()=START then true
else _objective < sol(_objective) endif;

View File

@ -1,5 +1,3 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{hill\PYZus{}climbing}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=} \PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{hill\PYZus{}climbing}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{!=}\PY{l+s}{ }\PY{n+nv}{START}\PY{l+s}{ }\PY{o}{\PYZhy{}\PYZgt{}}\PY{l+s}{ }\PY{l+s}{\PYZus{}}\PY{l+s}{o}\PY{l+s}{b}\PY{l+s}{j}\PY{l+s}{e}\PY{l+s}{c}\PY{l+s}{t}\PY{l+s}{i}\PY{l+s}{v}\PY{l+s}{e}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{l+s}{\PYZus{}}\PY{l+s}{o}\PY{l+s}{b}\PY{l+s}{j}\PY{l+s}{e}\PY{l+s}{c}\PY{l+s}{t}\PY{l+s}{i}\PY{l+s}{v}\PY{l+s}{e}\PY{p}{)}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{o}{=}\PY{n+nv}{START}\PY{l+s}{ }\PY{k}{then}\PY{l+s}{ }\PY{l}{true}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{else}\PY{l+s}{ }\PY{l+s}{\PYZus{}}\PY{l+s}{o}\PY{l+s}{b}\PY{l+s}{j}\PY{l+s}{e}\PY{l+s}{c}\PY{l+s}{t}\PY{l+s}{i}\PY{l+s}{v}\PY{l+s}{e}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{l+s}{\PYZus{}}\PY{l+s}{o}\PY{l+s}{b}\PY{l+s}{j}\PY{l+s}{e}\PY{l+s}{c}\PY{l+s}{t}\PY{l+s}{i}\PY{l+s}{v}\PY{l+s}{e}\PY{p}{)}\PY{l+s}{ }\PY{k}{endif}\PY{p}{;}
\end{Verbatim} \end{Verbatim}

View File

@ -1,4 +1,4 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{constraint}\PY{l+s}{ }\PY{n+nv}{x}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{l+m}{10}\PY{p}{;} \PY{k}{constraint}\PY{l+s}{ }\PY{n+nv}{x}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{l+m}{10}\PY{p}{;}
\PY{k}{constraint}\PY{l+s}{ }\PY{n+nv}{y}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{;} \PY{k}{constraint}\PY{l+s}{ }\PY{n+nv}{y}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{;}
\end{Verbatim} \end{Verbatim}

View File

@ -0,0 +1,25 @@
predicate lex_minimize(array[int] of var int: o) =
let {
var index_set(o): stage
array[index_set(o)] of var int: best;
} in if status() = START then
stage = min(index_set(o))
else
if status() = UNSAT then
if lastval(stage) < l then
stage = lastval(stage) + 1
else
complete() % we are finished
endif
else
stage = lastval(stage)
/\ best[stage] = sol(_objective)
endif
/\ for(i in min(index_set(o))..stage-1) (
o[i] = lastval(best[i])
)
/\ if status() = SAT then
o[stage] < sol(_objective)
endif
/\ _objective = o[stage]
endif;

View File

@ -0,0 +1,27 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{lex\PYZus{}minimize}\PY{p}{(}\PY{k+kt}{array}\PY{p}{[}\PY{k+kt}{int}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{o}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{n+nb}{index\PYZus{}set}\PY{p}{(}\PY{n+nv}{o}\PY{p}{)}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{stage}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{array}\PY{p}{[}\PY{n+nb}{index\PYZus{}set}\PY{p}{(}\PY{n+nv}{o}\PY{p}{)}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{best}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{START}\PY{l+s}{ }\PY{k}{then}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{stage}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nb}{min}\PY{p}{(}\PY{n+nb}{index\PYZus{}set}\PY{p}{(}\PY{n+nv}{o}\PY{p}{)}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{else}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{UNSAT}\PY{l+s}{ }\PY{k}{then}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{lastval}\PY{p}{(}\PY{n+nv}{stage}\PY{p}{)}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nv}{l}\PY{l+s}{ }\PY{k}{then}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{stage}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{lastval}\PY{p}{(}\PY{n+nv}{stage}\PY{p}{)}\PY{l+s}{ }\PY{o}{+}\PY{l+s}{ }\PY{l+m}{1}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{else}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nf}{complete}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{l+s}{ }\PY{c}{\PYZpc{} we are finished}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{else}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{stage}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{lastval}\PY{p}{(}\PY{n+nv}{stage}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{n+nv}{best}\PY{p}{[}\PY{n+nv}{stage}\PY{p}{]}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{l+s}{\PYZus{}}\PY{l+s}{o}\PY{l+s}{b}\PY{l+s}{j}\PY{l+s}{e}\PY{l+s}{c}\PY{l+s}{t}\PY{l+s}{i}\PY{l+s}{v}\PY{l+s}{e}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{k}{for}\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{n+nb}{min}\PY{p}{(}\PY{n+nb}{index\PYZus{}set}\PY{p}{(}\PY{n+nv}{o}\PY{p}{)}\PY{p}{)}\PY{l+s}{.}\PY{l+s}{.}\PY{n+nv}{stage}\PY{o}{\PYZhy{}}\PY{l+m}{1}\PY{p}{)}\PY{l+s}{ }\PY{p}{(}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{o}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{lastval}\PY{p}{(}\PY{n+nv}{best}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{SAT}\PY{l+s}{ }\PY{k}{then}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{o}\PY{p}{[}\PY{n+nv}{stage}\PY{p}{]}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{l+s}{\PYZus{}}\PY{l+s}{o}\PY{l+s}{b}\PY{l+s}{j}\PY{l+s}{e}\PY{l+s}{c}\PY{l+s}{t}\PY{l+s}{i}\PY{l+s}{v}\PY{l+s}{e}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{l+s}{\PYZus{}}\PY{l+s}{o}\PY{l+s}{b}\PY{l+s}{j}\PY{l+s}{e}\PY{l+s}{c}\PY{l+s}{t}\PY{l+s}{i}\PY{l+s}{v}\PY{l+s}{e}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{o}\PY{p}{[}\PY{n+nv}{stage}\PY{p}{]}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}\PY{p}{;}
\end{Verbatim}

View File

@ -1,8 +1,13 @@
function ann: lns(var int: obj, array[int] of var int: vars, function ann: lns(var int: obj, array[int] of var int: vars,
int: iterations, float: destr_rate, int: explore_time) = int: iterations, float: destr_rate, int: explore_time) =
repeat (i in 1..iterations) ( scope( repeat (i in 1..iterations) (
if has_sol() then post(uniform_neighbourhood(vars, destr_rate)) scope(
else true endif /\ if has_sol() then
time_limit(explore_time, minimize_bab(obj)) /\ post(uniform_neighbourhood(vars, destr_rate))
commit() /\ print() endif
) /\ post(obj < sol(obj)) ); /\ time_limit(explore_time, minimize_bab(obj))
/\ commit()
/\ print()
)
/\ post(obj < sol(obj))
);

View File

@ -1,10 +1,15 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{function}\PY{l+s}{ }\PY{k+kt}{ann}\PY{p}{:}\PY{l+s}{ }\PY{n+nf}{lns}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{obj}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{array}\PY{p}{[}\PY{k+kt}{int}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{vars}\PY{p}{,} \PY{k}{function}\PY{l+s}{ }\PY{k+kt}{ann}\PY{p}{:}\PY{l+s}{ }\PY{n+nf}{lns}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{obj}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{array}\PY{p}{[}\PY{k+kt}{int}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{vars}\PY{p}{,}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{iterations}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{destr\PYZus{}rate}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{explore\PYZus{}time}\PY{g+gr}{)}\PY{l+s}{ }\PY{o}{=} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{iterations}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{destr\PYZus{}rate}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{explore\PYZus{}time}\PY{g+gr}{)}\PY{l+s}{ }\PY{o}{=}
\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{repeat}\PY{l+s}{ }\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{l+m}{1}\PY{o}{..}\PY{n+nv}{iterations}\PY{p}{)}\PY{l+s}{ }\PY{p}{(}\PY{l+s}{ }\PY{n+nf}{scope}\PY{p}{(} \PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{repeat}\PY{l+s}{ }\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{l+m}{1}\PY{o}{..}\PY{n+nv}{iterations}\PY{p}{)}\PY{l+s}{ }\PY{p}{(}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{has\PYZus{}sol}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{k}{then}\PY{l+s}{ }\PY{n+nf}{post}\PY{p}{(}\PY{n+nf}{uniform\PYZus{}neighbourhood}\PY{p}{(}\PY{n+nv}{vars}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{destr\PYZus{}rate}\PY{p}{)}\PY{p}{)} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nf}{scope}\PY{p}{(}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{else}\PY{l+s}{ }\PY{l}{true}\PY{l+s}{ }\PY{k}{endif}\PY{l+s}{ }\PY{o}{/\PYZbs{}} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{has\PYZus{}sol}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{k}{then}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nf}{time\PYZus{}limit}\PY{p}{(}\PY{n+nv}{explore\PYZus{}time}\PY{p}{,}\PY{l+s}{ }\PY{n+nf}{minimize\PYZus{}bab}\PY{p}{(}\PY{n+nv}{obj}\PY{p}{)}\PY{p}{)}\PY{l+s}{ }\PY{o}{/\PYZbs{}} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nf}{post}\PY{p}{(}\PY{n+nf}{uniform\PYZus{}neighbourhood}\PY{p}{(}\PY{n+nv}{vars}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{destr\PYZus{}rate}\PY{p}{)}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nf}{commit}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{n+nf}{print}\PY{p}{(}\PY{p}{)} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{g+gr}{)}\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{n+nf}{post}\PY{p}{(}\PY{n+nv}{obj}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{n+nv}{obj}\PY{p}{)}\PY{p}{)}\PY{l+s}{ }\PY{g+gr}{)}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{n+nf}{time\PYZus{}limit}\PY{p}{(}\PY{n+nv}{explore\PYZus{}time}\PY{p}{,}\PY{l+s}{ }\PY{n+nf}{minimize\PYZus{}bab}\PY{p}{(}\PY{n+nv}{obj}\PY{p}{)}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{n+nf}{commit}\PY{p}{(}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{n+nf}{print}\PY{p}{(}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{g+gr}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{n+nf}{post}\PY{p}{(}\PY{n+nv}{obj}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{n+nv}{obj}\PY{p}{)}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{g+gr}{)}\PY{p}{;}
\end{Verbatim} \end{Verbatim}

View File

@ -1,3 +1,6 @@
predicate uniform_neighbourhood(array[int] of var int: x, float: destrRate) = predicate uniform_neighbourhood(array[int] of var int: x, float: destr_rate) =
forall(i in index_set(x)) forall(i in index_set(x)) (
(if uniform(0.0,1.0) > destrRate then x[i] = sol(x[i]) else true endif); if uniform(0.0, 1.0) > destr_rate then
x[i] = sol(x[i])
endif
);

View File

@ -1,5 +1,8 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{uniform\PYZus{}neighbourhood}\PY{p}{(}\PY{k+kt}{array}\PY{p}{[}\PY{k+kt}{int}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{destrRate}\PY{p}{)}\PY{l+s}{ }\PY{o}{=} \PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{uniform\PYZus{}neighbourhood}\PY{p}{(}\PY{k+kt}{array}\PY{p}{[}\PY{k+kt}{int}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{destr\PYZus{}rate}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{forall}\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{n+nb}{index\PYZus{}set}\PY{p}{(}\PY{n+nv}{x}\PY{p}{)}\PY{p}{)} \PY{l+s}{ }\PY{l+s}{ }\PY{k}{forall}\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{n+nb}{index\PYZus{}set}\PY{p}{(}\PY{n+nv}{x}\PY{p}{)}\PY{p}{)}\PY{l+s}{ }\PY{p}{(}
\PY{l+s}{ }\PY{l+s}{ }\PY{p}{(}\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{uniform}\PY{p}{(}\PY{l+m}{0.0}\PY{p}{,}\PY{l+m}{1.0}\PY{p}{)}\PY{l+s}{ }\PY{o}{\PYZgt{}}\PY{l+s}{ }\PY{n+nv}{destrRate}\PY{l+s}{ }\PY{k}{then}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{n+nv}{x}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{p}{)}\PY{l+s}{ }\PY{k}{else}\PY{l+s}{ }\PY{l}{true}\PY{l+s}{ }\PY{k}{endif}\PY{p}{)}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{uniform}\PY{p}{(}\PY{l+m}{0.0}\PY{p}{,}\PY{l+s}{ }\PY{l+m}{1.0}\PY{p}{)}\PY{l+s}{ }\PY{o}{\PYZgt{}}\PY{l+s}{ }\PY{n+nv}{destr\PYZus{}rate}\PY{l+s}{ }\PY{k}{then}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{n+nv}{x}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}
\PY{l+s}{ }\PY{l+s}{ }\PY{p}{)}\PY{p}{;}
\end{Verbatim} \end{Verbatim}

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

View File

@ -0,0 +1,21 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{pareto\PYZus{}optimal}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{obj1}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{obj2}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{ms}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{l+m}{1000}\PY{p}{;}\PY{l+s}{ }\PY{c}{\PYZpc{} max solutions}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{l+m}{0}\PY{o}{..}\PY{n+nv}{ms}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{nsol}\PY{p}{;}\PY{l+s}{ }\PY{l+s}{ }\PY{c}{\PYZpc{} number of solutions}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{set}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{SOL}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{l+m}{1}\PY{o}{..}\PY{n+nv}{ms}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{array}\PY{p}{[}\PY{n+nv}{SOL}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{n+nb}{lb}\PY{p}{(}\PY{n+nv}{obj1}\PY{p}{)}\PY{l+s}{.}\PY{l+s}{.}\PY{n+nb}{ub}\PY{p}{(}\PY{n+nv}{obj1}\PY{p}{)}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{s1}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{array}\PY{p}{[}\PY{n+nv}{SOL}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{n+nb}{lb}\PY{p}{(}\PY{n+nv}{obj2}\PY{p}{)}\PY{l+s}{.}\PY{l+s}{.}\PY{n+nb}{ub}\PY{p}{(}\PY{n+nv}{obj2}\PY{p}{)}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{s2}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{START}\PY{l+s}{ }\PY{k}{then}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{nsol}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{l+m}{0}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{elseif}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{UNSAT}\PY{l+s}{ }\PY{k}{then}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nf}{complete}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{c}{\PYZpc{} we are finished!}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{elseif}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{nsol}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{n+nv}{nsol}\PY{p}{)}\PY{l+s}{ }\PY{o}{+}\PY{l+s}{ }\PY{l+m}{1}\PY{l+s}{ }\PY{o}{/\PYZbs{}}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{s1}\PY{p}{[}\PY{n+nv}{nsol}\PY{p}{]}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{n+nv}{obj1}\PY{p}{)}\PY{l+s}{ }\PY{o}{/\PYZbs{}}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{s2}\PY{p}{[}\PY{n+nv}{nsol}\PY{p}{]}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{n+nv}{obj2}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}
\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{k}{for}\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{l+m}{1}\PY{o}{..}\PY{n+nv}{nsol}\PY{p}{)}\PY{l+s}{ }\PY{p}{(}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{obj1}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nf}{lastval}\PY{p}{(}\PY{n+nv}{s1}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{p}{)}\PY{l+s}{ }\PY{o}{\PYZbs{}/}\PY{l+s}{ }\PY{n+nv}{obj2}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nf}{lastval}\PY{p}{(}\PY{n+nv}{s2}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{p}{)}\PY{p}{;}
\end{Verbatim}

View File

@ -1,4 +1,4 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{free\PYZus{}timeslot}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{l+s}{ }\PY{o}{=} \PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{free\PYZus{}timeslot}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{l+s}{ }\PY{o}{=}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{slot}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nb}{max}\PY{p}{(}\PY{n+nv}{Times}\PY{p}{)}\PY{l+s}{ }\PY{o}{div}\PY{l+s}{ }\PY{l+m}{10}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{slot}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nb}{max}\PY{p}{(}\PY{n+nv}{Times}\PY{p}{)}\PY{l+s}{ }\PY{o}{div}\PY{l+s}{ }\PY{l+m}{10}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{time}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{uniform}\PY{p}{(}\PY{n+nb}{min}\PY{p}{(}\PY{n+nv}{Times}\PY{p}{)}\PY{p}{,}\PY{l+s}{ }\PY{n+nb}{max}\PY{p}{(}\PY{n+nv}{Times}\PY{p}{)}\PY{l+s}{ }\PY{o}{\PYZhy{}}\PY{l+s}{ }\PY{n+nv}{slot}\PY{p}{)}\PY{p}{;}\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{time}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{uniform}\PY{p}{(}\PY{n+nb}{min}\PY{p}{(}\PY{n+nv}{Times}\PY{p}{)}\PY{p}{,}\PY{l+s}{ }\PY{n+nb}{max}\PY{p}{(}\PY{n+nv}{Times}\PY{p}{)}\PY{l+s}{ }\PY{o}{\PYZhy{}}\PY{l+s}{ }\PY{n+nv}{slot}\PY{p}{)}\PY{p}{;}\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}

View File

@ -1,4 +1,4 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{c}{\PYZpc{} post predicate "pred" whenever the solver restarts} \PY{c}{\PYZpc{} post predicate "pred" whenever the solver restarts}
\PY{k}{annotation}\PY{l+s}{ }\PY{n+nf}{on\PYZus{}restart}\PY{p}{(}\PY{k+kt}{string}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{pred}\PY{p}{)}\PY{p}{;} \PY{k}{annotation}\PY{l+s}{ }\PY{n+nf}{on\PYZus{}restart}\PY{p}{(}\PY{k+kt}{string}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{pred}\PY{p}{)}\PY{p}{;}
\PY{c}{\PYZpc{} restart after fixed number of nodes} \PY{c}{\PYZpc{} restart after fixed number of nodes}

View File

@ -1,11 +1,12 @@
predicate round_robin(array[int] of var bool: nbhs) = predicate round_robin(array[int] of var bool: nbhs) =
let { let {
int: N = length(nbhs); int: N = length(nbhs);
var -1..N-1: select; % Neighbourhood selection var -1..N-1: select; % Neighbourhood selection
} in if status()=START then } in if status()=START then
select= -1 select = -1
else else
select= (last_val(select) + 1) mod N select = (last_val(select) + 1) mod N
endif /\ forall(i in 1..N) ( endif
select=i-1 -> nbhs[i] @\Vlabel{line:6:roundrobin:post}@ /\ forall(i in 1..N) (
); select = i-1 -> nbhs[i] @\Vlabel{line:6:roundrobin:post}@
);

View File

@ -1,13 +1,14 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{round\PYZus{}robin}\PY{p}{(}\PY{k+kt}{array}\PY{p}{[}\PY{k+kt}{int}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{bool}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{nbhs}\PY{p}{)}\PY{l+s}{ }\PY{o}{=} \PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{round\PYZus{}robin}\PY{p}{(}\PY{k+kt}{array}\PY{p}{[}\PY{k+kt}{int}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{bool}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{nbhs}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}} \PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{N}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nb}{length}\PY{p}{(}\PY{n+nv}{nbhs}\PY{p}{)}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{N}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nb}{length}\PY{p}{(}\PY{n+nv}{nbhs}\PY{p}{)}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{o}{\PYZhy{}}\PY{l+m}{1}\PY{o}{..}\PY{n+nv}{N}\PY{o}{\PYZhy{}}\PY{l+m}{1}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{select}\PY{p}{;}\PY{l+s}{ }\PY{c}{\PYZpc{} Neighbourhood selection} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{o}{\PYZhy{}}\PY{l+m}{1}\PY{o}{..}\PY{n+nv}{N}\PY{o}{\PYZhy{}}\PY{l+m}{1}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{select}\PY{p}{;}\PY{l+s}{ }\PY{c}{\PYZpc{} Neighbourhood selection}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{o}{=}\PY{n+nv}{START}\PY{l+s}{ }\PY{k}{then} \PY{l+s}{ }\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{o}{=}\PY{n+nv}{START}\PY{l+s}{ }\PY{k}{then}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{select}\PY{o}{=}\PY{l+s}{ }\PY{o}{\PYZhy{}}\PY{l+m}{1} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{select}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{o}{\PYZhy{}}\PY{l+m}{1}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{else} \PY{l+s}{ }\PY{l+s}{ }\PY{k}{else}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{select}\PY{o}{=}\PY{l+s}{ }\PY{p}{(}\PY{n+nf}{last\PYZus{}val}\PY{p}{(}\PY{n+nv}{select}\PY{p}{)}\PY{l+s}{ }\PY{o}{+}\PY{l+s}{ }\PY{l+m}{1}\PY{p}{)}\PY{l+s}{ }\PY{o}{mod}\PY{l+s}{ }\PY{n+nv}{N} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{select}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{p}{(}\PY{n+nf}{last\PYZus{}val}\PY{p}{(}\PY{n+nv}{select}\PY{p}{)}\PY{l+s}{ }\PY{o}{+}\PY{l+s}{ }\PY{l+m}{1}\PY{p}{)}\PY{l+s}{ }\PY{o}{mod}\PY{l+s}{ }\PY{n+nv}{N}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{k}{forall}\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{l+m}{1}\PY{o}{..}\PY{n+nv}{N}\PY{p}{)}\PY{l+s}{ }\PY{p}{(} \PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{select}\PY{o}{=}\PY{n+nv}{i}\PY{o}{\PYZhy{}}\PY{l+m}{1}\PY{l+s}{ }\PY{o}{\PYZhy{}\PYZgt{}}\PY{l+s}{ }\PY{n+nv}{nbhs}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{l+s}{ }\PY{esc}{\Vlabel{line:6:roundrobin:post}} \PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{k}{forall}\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{l+m}{1}\PY{o}{..}\PY{n+nv}{N}\PY{p}{)}\PY{l+s}{ }\PY{p}{(}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{p}{)}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{select}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{i}\PY{o}{\PYZhy{}}\PY{l+m}{1}\PY{l+s}{ }\PY{o}{\PYZhy{}\PYZgt{}}\PY{l+s}{ }\PY{n+nv}{nbhs}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{l+s}{ }\PY{esc}{\Vlabel{line:6:roundrobin:post}}
\PY{l+s}{ }\PY{l+s}{ }\PY{p}{)}\PY{p}{;}
\end{Verbatim} \end{Verbatim}

View File

@ -1,7 +1,9 @@
predicate simulated_annealing(float: initTemp, float: coolingRate) = predicate simulated_annealing(float: init_temp, float: cooling_rate) =
let { var float: temp; } in let {
if status()=START then temp = initTemp var float: temp;
} in if status() = START then
temp = init_temp
else else
temp = last_val(temp)*(1-coolingRate) /\ % cool down temp = last_val(temp) * (1 - cooling_rate) % cool down
_objective < sol(_objective) - ceil(log(uniform(0.0,1.0)) * temp) /\ _objective < sol(_objective) - ceil(log(uniform(0.0, 1.0)) * temp)
endif; endif;

View File

@ -1,9 +1,11 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{simulated\PYZus{}annealing}\PY{p}{(}\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{initTemp}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{coolingRate}\PY{p}{)}\PY{l+s}{ }\PY{o}{=} \PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{simulated\PYZus{}annealing}\PY{p}{(}\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{init\PYZus{}temp}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{cooling\PYZus{}rate}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{temp}\PY{p}{;}\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in} \PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{o}{=}\PY{n+nv}{START}\PY{l+s}{ }\PY{k}{then}\PY{l+s}{ }\PY{n+nv}{temp}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{initTemp} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{temp}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{START}\PY{l+s}{ }\PY{k}{then}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{temp}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{init\PYZus{}temp}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{else} \PY{l+s}{ }\PY{l+s}{ }\PY{k}{else}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{temp}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{last\PYZus{}val}\PY{p}{(}\PY{n+nv}{temp}\PY{p}{)}\PY{o}{*}\PY{p}{(}\PY{l+m}{1}\PY{o}{\PYZhy{}}\PY{n+nv}{coolingRate}\PY{p}{)}\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{c}{\PYZpc{} cool down} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{temp}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{last\PYZus{}val}\PY{p}{(}\PY{n+nv}{temp}\PY{p}{)}\PY{l+s}{ }\PY{o}{*}\PY{l+s}{ }\PY{p}{(}\PY{l+m}{1}\PY{l+s}{ }\PY{o}{\PYZhy{}}\PY{l+s}{ }\PY{n+nv}{cooling\PYZus{}rate}\PY{p}{)}\PY{l+s}{ }\PY{c}{\PYZpc{} cool down}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{\PYZus{}}\PY{l+s}{o}\PY{l+s}{b}\PY{l+s}{j}\PY{l+s}{e}\PY{l+s}{c}\PY{l+s}{t}\PY{l+s}{i}\PY{l+s}{v}\PY{l+s}{e}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{l+s}{\PYZus{}}\PY{l+s}{o}\PY{l+s}{b}\PY{l+s}{j}\PY{l+s}{e}\PY{l+s}{c}\PY{l+s}{t}\PY{l+s}{i}\PY{l+s}{v}\PY{l+s}{e}\PY{p}{)}\PY{l+s}{ }\PY{o}{\PYZhy{}}\PY{l+s}{ }\PY{n+nb}{ceil}\PY{p}{(}\PY{n+nb}{log}\PY{p}{(}\PY{n+nf}{uniform}\PY{p}{(}\PY{l+m}{0.0}\PY{p}{,}\PY{l+m}{1.0}\PY{p}{)}\PY{p}{)}\PY{l+s}{ }\PY{o}{*}\PY{l+s}{ }\PY{n+nv}{temp}\PY{p}{)} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{l+s}{\PYZus{}}\PY{l+s}{o}\PY{l+s}{b}\PY{l+s}{j}\PY{l+s}{e}\PY{l+s}{c}\PY{l+s}{t}\PY{l+s}{i}\PY{l+s}{v}\PY{l+s}{e}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{l+s}{\PYZus{}}\PY{l+s}{o}\PY{l+s}{b}\PY{l+s}{j}\PY{l+s}{e}\PY{l+s}{c}\PY{l+s}{t}\PY{l+s}{i}\PY{l+s}{v}\PY{l+s}{e}\PY{p}{)}\PY{l+s}{ }\PY{o}{\PYZhy{}}\PY{l+s}{ }\PY{n+nb}{ceil}\PY{p}{(}\PY{n+nb}{log}\PY{p}{(}\PY{n+nf}{uniform}\PY{p}{(}\PY{l+m}{0.0}\PY{p}{,}\PY{l+s}{ }\PY{l+m}{1.0}\PY{p}{)}\PY{p}{)}\PY{l+s}{ }\PY{o}{*}\PY{l+s}{ }\PY{n+nv}{temp}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}\PY{p}{;}
\end{Verbatim} \end{Verbatim}

View File

@ -1,8 +1,10 @@
predicate int_sol(var int: x, var int: xi); predicate int_sol(var int: x, var int: xi);
function int: sol(var int: x) = function int: sol(var int: x) =
if is_fixed(x) then fix(x) if is_fixed(x) then
else let { fix(x)
var lb(x)..ub(x): xi; else
constraint int_sol(x,xi); let {
var lb(x)..ub(x): xi;
constraint int_sol(x,xi);
} in xi; } in xi;
endif; endif;

View File

@ -1,10 +1,12 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{int\PYZus{}sol}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{xi}\PY{p}{)}\PY{p}{;} \PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{int\PYZus{}sol}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{xi}\PY{p}{)}\PY{p}{;}
\PY{k}{function}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{)}\PY{l+s}{ }\PY{o}{=} \PY{k}{function}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nb}{is\PYZus{}fixed}\PY{p}{(}\PY{n+nv}{x}\PY{p}{)}\PY{l+s}{ }\PY{k}{then}\PY{l+s}{ }\PY{n+nb}{fix}\PY{p}{(}\PY{n+nv}{x}\PY{p}{)} \PY{l+s}{ }\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nb}{is\PYZus{}fixed}\PY{p}{(}\PY{n+nv}{x}\PY{p}{)}\PY{l+s}{ }\PY{k}{then}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{else}\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nb}{fix}\PY{p}{(}\PY{n+nv}{x}\PY{p}{)}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{n+nb}{lb}\PY{p}{(}\PY{n+nv}{x}\PY{p}{)}\PY{l+s}{.}\PY{l+s}{.}\PY{n+nb}{ub}\PY{p}{(}\PY{n+nv}{x}\PY{p}{)}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{xi}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{k}{else}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{int\PYZus{}sol}\PY{p}{(}\PY{n+nv}{x}\PY{p}{,}\PY{n+nv}{xi}\PY{p}{)}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{n+nb}{lb}\PY{p}{(}\PY{n+nv}{x}\PY{p}{)}\PY{l+s}{.}\PY{l+s}{.}\PY{n+nb}{ub}\PY{p}{(}\PY{n+nv}{x}\PY{p}{)}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{xi}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{int\PYZus{}sol}\PY{p}{(}\PY{n+nv}{x}\PY{p}{,}\PY{n+nv}{xi}\PY{p}{)}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{n+nv}{xi}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{n+nv}{xi}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}\PY{p}{;}
\end{Verbatim} \end{Verbatim}

View File

@ -1,5 +1,6 @@
% Report the status of the solver (before restarting). % Report the status of the solver (before restarting).
enum STATUS = {START, UNKNOWN, UNSAT, SAT, OPT} @\label{ann:enum_status}@ enum STATUS = {START, UNKNOWN, UNSAT, SAT, OPT} @\label{ann:enum_status}@
function STATUS: status(); @\label{ann:status}@ function STATUS: status(); @\label{ann:status}@
% Provide access to the last assigned value of variable x. % Provide access to the last assigned value of variable x.
function int: last_val(var int: x); function int: last_val(var int: x);

View File

@ -1,7 +1,8 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{c}{\PYZpc{} Report the status of the solver (before restarting).} \PY{c}{\PYZpc{} Report the status of the solver (before restarting).}
\PY{k+kt}{enum}\PY{l+s}{ }\PY{n+nv}{STATUS}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{p}{\PYZob{}}\PY{n+nv}{START}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{UNKNOWN}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{UNSAT}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{SAT}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{OPT}\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{esc}{\label{ann:enum_status}} \PY{k+kt}{enum}\PY{l+s}{ }\PY{n+nv}{STATUS}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{p}{\PYZob{}}\PY{n+nv}{START}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{UNKNOWN}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{UNSAT}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{SAT}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{OPT}\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{esc}{\label{ann:enum_status}}
\PY{k}{function}\PY{l+s}{ }\PY{n+nv}{STATUS}\PY{p}{:}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{p}{;}\PY{l+s}{ }\PY{esc}{\label{ann:status}} \PY{k}{function}\PY{l+s}{ }\PY{n+nv}{STATUS}\PY{p}{:}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{p}{;}\PY{l+s}{ }\PY{esc}{\label{ann:status}}
\PY{c}{\PYZpc{} Provide access to the last assigned value of variable x.} \PY{c}{\PYZpc{} Provide access to the last assigned value of variable x.}
\PY{k}{function}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nf}{last\PYZus{}val}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{)}\PY{p}{;} \PY{k}{function}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nf}{last\PYZus{}val}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{)}\PY{p}{;}
\end{Verbatim} \end{Verbatim}

View File

@ -1,5 +1,6 @@
predicate status(var int: stat); @\Vlabel{line:6:status}@ predicate status(var int: stat); @\Vlabel{line:6:status}@
function var STATUS: status() = function var STATUS: status() =
let { var STATUS: stat; let {
constraint status(stat); var STATUS: stat;
} in stat; constraint status(stat);
} in stat;

View File

@ -1,7 +1,8 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{stat}\PY{p}{)}\PY{p}{;}\PY{l+s}{ }\PY{esc}{\Vlabel{line:6:status}} \PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{stat}\PY{p}{)}\PY{p}{;}\PY{l+s}{ }\PY{esc}{\Vlabel{line:6:status}}
\PY{k}{function}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{n+nv}{STATUS}\PY{p}{:}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=} \PY{k}{function}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{n+nv}{STATUS}\PY{p}{:}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{n+nv}{STATUS}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{stat}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{n+nv}{stat}\PY{p}{)}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{n+nv}{STATUS}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{stat}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{n+nv}{stat}\PY{p}{;} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{n+nv}{stat}\PY{p}{)}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{n+nv}{stat}\PY{p}{;}
\end{Verbatim} \end{Verbatim}

View File

@ -1,4 +1,4 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{free\PYZus{}slab}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=} \PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{free\PYZus{}slab}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{slab}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{uniform}\PY{p}{(}\PY{l+m}{1}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{nbSlabs}\PY{p}{)}\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{slab}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{uniform}\PY{p}{(}\PY{l+m}{1}\PY{p}{,}\PY{l+s}{ }\PY{n+nv}{nbSlabs}\PY{p}{)}\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{forall}\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{l+m}{1}\PY{o}{..}\PY{n+nv}{nbSlabs}\PY{l+s}{ }\PY{k}{where}\PY{l+s}{ }\PY{n+nv}{slab}\PY{l+s}{ }\PY{o}{!=}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{n+nv}{assign}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{p}{)}\PY{p}{)} \PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{forall}\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{l+m}{1}\PY{o}{..}\PY{n+nv}{nbSlabs}\PY{l+s}{ }\PY{k}{where}\PY{l+s}{ }\PY{n+nv}{slab}\PY{l+s}{ }\PY{o}{!=}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{n+nv}{assign}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{p}{)}\PY{p}{)}

View File

@ -0,0 +1 @@
b3 -> x[1] = sol(x[1])

View File

@ -0,0 +1,3 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{n+nv}{b3}\PY{l+s}{ }\PY{o}{\PYZhy{}\PYZgt{}}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{[}\PY{l+m}{1}\PY{p}{]}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{n+nv}{x}\PY{p}{[}\PY{l+m}{1}\PY{p}{]}\PY{p}{)}
\end{Verbatim}

View File

@ -0,0 +1 @@
(status() != START /\ uniform(0.0,1.0) > 0.2) -> x[1] = sol(x[1])

View File

@ -0,0 +1,3 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{p}{(}\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{!=}\PY{l+s}{ }\PY{n+nv}{START}\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{n+nf}{uniform}\PY{p}{(}\PY{l+m}{0.0}\PY{p}{,}\PY{l+m}{1.0}\PY{p}{)}\PY{l+s}{ }\PY{o}{\PYZgt{}}\PY{l+s}{ }\PY{l+m}{0.2}\PY{p}{)}\PY{l+s}{ }\PY{o}{\PYZhy{}\PYZgt{}}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{[}\PY{l+m}{1}\PY{p}{]}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{n+nv}{x}\PY{p}{[}\PY{l+m}{1}\PY{p}{]}\PY{p}{)}
\end{Verbatim}

View File

@ -1,6 +0,0 @@
predicate float_uniform(var float:l, var float: u, var float: r);
function var float: uniform_nbh(var float: l, var float: u) :: impure =
let {
var lb(l)..ub(u): rnd;
constraint float_uniform(l,u,rnd):
} in rnd;

View File

@ -1,8 +0,0 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm]
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{float\PYZus{}uniform}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{n+nv}{l}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{u}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{r}\PY{p}{)}\PY{p}{;}
\PY{k}{function}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nf}{uniform\PYZus{}nbh}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{l}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{u}\PY{p}{)}\PY{l+s}{ }\PY{p}{:}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{impure}\PY{l+s}{ }\PY{o}{=}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{n+nb}{lb}\PY{p}{(}\PY{n+nv}{l}\PY{p}{)}\PY{l+s}{.}\PY{l+s}{.}\PY{n+nb}{ub}\PY{p}{(}\PY{n+nv}{u}\PY{p}{)}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{rnd}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{float\PYZus{}uniform}\PY{p}{(}\PY{n+nv}{l}\PY{p}{,}\PY{n+nv}{u}\PY{p}{,}\PY{n+nv}{rnd}\PY{p}{)}\PY{p}{:}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{n+nv}{rnd}\PY{p}{;}
\end{Verbatim}

View File

@ -0,0 +1,6 @@
predicate float_uniform(var float:l, var float: u, var float: r);
function var float: uniform_slv(var float: l, var float: u) :: impure =
let {
var lb(l)..ub(u): rnd;
constraint float_uniform(l,u,rnd):
} in rnd;

View File

@ -0,0 +1,8 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{float\PYZus{}uniform}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{n+nv}{l}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{u}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{r}\PY{p}{)}\PY{p}{;}
\PY{k}{function}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nf}{uniform\PYZus{}slv}\PY{p}{(}\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{l}\PY{p}{,}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{float}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{u}\PY{p}{)}\PY{l+s}{ }\PY{p}{:}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{impure}\PY{l+s}{ }\PY{o}{=}
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{n+nb}{lb}\PY{p}{(}\PY{n+nv}{l}\PY{p}{)}\PY{l+s}{.}\PY{l+s}{.}\PY{n+nb}{ub}\PY{p}{(}\PY{n+nv}{u}\PY{p}{)}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{rnd}\PY{p}{;}
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{constraint}\PY{l+s}{ }\PY{n+nf}{float\PYZus{}uniform}\PY{p}{(}\PY{n+nv}{l}\PY{p}{,}\PY{n+nv}{u}\PY{p}{,}\PY{n+nv}{rnd}\PY{p}{)}\PY{p}{:}
\PY{l+s}{ }\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{n+nv}{rnd}\PY{p}{;}
\end{Verbatim}

View File

@ -1,4 +1,4 @@
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8},xleftmargin=5mm] \begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
\PY{n}{toys\PYZus{}joy} \PY{o}{=} \PY{p}{[}\PY{l+m+mi}{63}\PY{p}{,} \PY{l+m+mi}{12}\PY{p}{,} \PY{l+m+mi}{50}\PY{p}{,} \PY{l+m+mi}{100}\PY{p}{]} \PY{n}{toys\PYZus{}joy} \PY{o}{=} \PY{p}{[}\PY{l+m+mi}{63}\PY{p}{,} \PY{l+m+mi}{12}\PY{p}{,} \PY{l+m+mi}{50}\PY{p}{,} \PY{l+m+mi}{100}\PY{p}{]}
\PY{n}{toys\PYZus{}space} \PY{o}{=} \PY{p}{[}\PY{l+m+mi}{32}\PY{p}{,} \PY{l+m+mi}{8}\PY{p}{,} \PY{l+m+mi}{16}\PY{p}{,} \PY{l+m+mi}{40}\PY{p}{]} \PY{n}{toys\PYZus{}space} \PY{o}{=} \PY{p}{[}\PY{l+m+mi}{32}\PY{p}{,} \PY{l+m+mi}{8}\PY{p}{,} \PY{l+m+mi}{16}\PY{p}{,} \PY{l+m+mi}{40}\PY{p}{]}
\PY{n}{space\PYZus{}left} \PY{o}{=} \PY{l+m+mi}{64} \PY{n}{space\PYZus{}left} \PY{o}{=} \PY{l+m+mi}{64}

View File

@ -55,22 +55,22 @@ still prove prohibitive, warranting direct support from the
methods to provide this support: methods to provide this support:
\begin{itemize} \begin{itemize}
\item Using a minimal extension of existing solvers, we can compile \item We introduce the notion of restart-based \gls{meta-search} algorithms.
\gls{meta-search} algorithms into efficient solver-level specifications Using a minimal extension to a \cml\ and its target solver, we can model
based on solver restart, avoiding re-compilation all-together. some \gls{meta-search} algorithms and compile \gls{meta-search}
\item We can add an interface for adding and removing constraints in the algorithms into efficient solver-level specifications based on solver
\gls{constraint-modelling} infrastructure and avoid re-compilation where restarts, avoiding re-compilation all-together.
possible. \item Alternatively, we can add an incremental interface for adding and
removing constraints to the infrastructure of the \cml. Although this
does not avoid the need for re-compilation, it can reduce the work to
only the part of the constraint model that has changed. This approach
can be used when an algorithm cannot be described using restart-based
\gls{meta-search} or required extension is not available for the solver.
\end{itemize} \end{itemize}
Although it might sound like the first option is always the best one, it should
be noted that this option cannot always be used. It might not be possible to
extend the target \gls{solver} (or it might not be allowed in case of some
proprietary \glspl{solver}). Furthermore, the modelling of \gls{meta-search}
algorithms using solver restarts is limited \textbf{TODO: in some way}.
The rest of the chapter is organised as follows. \Cref{sec:6-modelling} The rest of the chapter is organised as follows. \Cref{sec:6-modelling}
discusses the declarative modelling of \gls{meta-search} algorithms using \cmls. discusses the declarative modelling of restart-based \gls{meta-search}
algorithms that can be modelled directly in a \cml.
\Cref{sec:6-solver-extension} introduces the method to compile these \Cref{sec:6-solver-extension} introduces the method to compile these
\gls{meta-search} specifications into efficient solver-level specifications that \gls{meta-search} specifications into efficient solver-level specifications that
only require a small extension of existing \glspl{solver}. only require a small extension of existing \glspl{solver}.
@ -81,7 +81,7 @@ and remove constraints from an existing model while avoiding recompilation.
Finally, \Cref{sec:6-conclusion} presents the conclusions. Finally, \Cref{sec:6-conclusion} presents the conclusions.
\section{Modelling of Meta-Search} \section{Modelling of Restart-Based Meta-Search}
\label{sec:6-modelling} \label{sec:6-modelling}
This section introduces a \minizinc\ extension that enables modellers to define This section introduces a \minizinc\ extension that enables modellers to define
@ -198,9 +198,9 @@ workaround, we currently pass the name of the predicate to be called for each
restart as a string (see the definition of the new \mzninline{on_restart} restart as a string (see the definition of the new \mzninline{on_restart}
annotation in \cref{lst:6-restart-ann}). annotation in \cref{lst:6-restart-ann}).
The second component of our \gls{lns} definition is the \emph{restarting strategy}, The second component of our \gls{lns} definition is the \emph{restarting
defining how much effort the solver should put into each neighbourhood (\ie\ strategy}, defining how much effort the solver should put into each
restart), and when to stop the overall search. neighbourhood (\ie\ restart), and when to stop the overall search.
We propose adding new search annotations to \minizinc\ to control this behaviour We propose adding new search annotations to \minizinc\ to control this behaviour
(see \cref{lst:6-restart-ann}). The \mzninline{restart_on_solution} annotation (see \cref{lst:6-restart-ann}). The \mzninline{restart_on_solution} annotation
@ -212,7 +212,7 @@ search when no solution is found. The \mzninline{timeout} annotation gives an
overall time limit for the search, whereas \mzninline{restart_limit} stops the overall time limit for the search, whereas \mzninline{restart_limit} stops the
search after a fixed number of restarts. search after a fixed number of restarts.
\begin{listing}[t] \begin{listing}
\highlightfile{assets/mzn/6_restart_ann.mzn} \highlightfile{assets/mzn/6_restart_ann.mzn}
\caption{\label{lst:6-restart-ann} New annotations to control the restarting \caption{\label{lst:6-restart-ann} New annotations to control the restarting
behaviour} behaviour}
@ -222,14 +222,14 @@ search after a fixed number of restarts.
Although using just a restart annotations by themselves allows us to run the Although using just a restart annotations by themselves allows us to run the
basic \gls{lns} algorithm, more advanced \gls{meta-search} algorithms will basic \gls{lns} algorithm, more advanced \gls{meta-search} algorithms will
require more then just reapplying the same \gls{neighbourhood} time after time. require more then reapplying the same \gls{neighbourhood} time after time. It
It is, for example, often beneficial to use several \gls{neighbourhood} is, for example, often beneficial to use several \gls{neighbourhood} definitions
definitions for a problem. Different \glspl{neighbourhood} may be able to for a problem. Different \glspl{neighbourhood} may be able to improve different
improve different aspects of a solution, at different phases of the search. aspects of a solution, at different phases of the search. Adaptive \gls{lns}
Adaptive \gls{lns} \autocite{ropke-2006-adaptive, pisinger-2007-heuristic}, \autocite{ropke-2006-adaptive, pisinger-2007-heuristic}, which keeps track of
which keeps track of the \glspl{neighbourhood} that led to improvements and the \glspl{neighbourhood} that led to improvements and favours them for future
favours them for future iterations, is the prime example for this approach. A iterations, is the prime example for this approach. A simpler scheme may apply
simpler scheme may apply several \glspl{neighbourhood} in a round-robin fashion. several \glspl{neighbourhood} in a round-robin fashion.
In \minisearch\, these adaptive or round-robin approaches can be implemented In \minisearch\, these adaptive or round-robin approaches can be implemented
using \emph{state variables}, which support destructive update (overwriting the using \emph{state variables}, which support destructive update (overwriting the
@ -252,7 +252,7 @@ like \mzninline{sol}, has versions for all basic variable types) allows
modellers to access the last value assigned to a variable (the value is modellers to access the last value assigned to a variable (the value is
undefined if \mzninline{status()=START}). undefined if \mzninline{status()=START}).
\begin{listing}[t] \begin{listing}
\highlightfile{assets/mzn/6_state_access.mzn} \highlightfile{assets/mzn/6_state_access.mzn}
\caption{\label{lst:6-state-access} Functions for accessing previous solver \caption{\label{lst:6-state-access} Functions for accessing previous solver
states} states}
@ -272,59 +272,58 @@ parametric over the neighbourhoods they should apply. For example, since
strategy \mzninline{basic_lns} that applies a neighbourhood only if the current strategy \mzninline{basic_lns} that applies a neighbourhood only if the current
status is not \mzninline{START}: status is not \mzninline{START}:
\mzninline{predicate basic_lns(var bool: nbh) = (status()!=START -> nbh);} \highlightfile{assets/mzn/6_basic_lns.mzn}
In order to use this predicate with the \mzninline{on_restart} annotation, we In order to use this predicate with the \mzninline{on_restart} annotation, we
cannot simply pass \mzninline{basic_lns(uniformNeighbourhood(x,0.2))}. First of cannot simply pass \mzninline{basic_lns(uniform_neighbourhood(x, 0.2))}. First
all, calling \mzninline{uniformNeighbourhood} like that would result in a of all, calling \mzninline{uniform_neighbourhood} like that would result in a
\emph{single} evaluation of the predicate, since \minizinc\ employs a \emph{single} evaluation of the predicate, since \minizinc\ employs a
call-by-value evaluation strategy. Furthermore, the \mzninline{on_restart} call-by-value evaluation strategy. Furthermore, the \mzninline{on_restart}
annotation only accepts the name of a nullary predicate. Therefore, users have annotation only accepts the name of a nullary predicate. Therefore, users have
to define their overall strategy in a new predicate. \Cref{lst:6-basic-complete} to define their overall strategy in a new predicate. \Cref{lst:6-basic-complete}
shows a complete example of a basic \gls{lns} model. shows a complete example of a basic \gls{lns} model.
\begin{listing}[t] \begin{listing}
\highlightfile{assets/mzn/6_basic_complete.mzn} \highlightfile{assets/mzn/6_basic_complete.mzn}
\caption{\label{lst:6-basic-complete} Complete \gls{lns} example} \caption{\label{lst:6-basic-complete} Complete \gls{lns} example}
\end{listing} \end{listing}
We can also define round-robin and adaptive strategies using these primitives. We can also define round-robin and adaptive strategies using these primitives.
%\paragraph{Round-robin \gls{lns}} \Cref{lst:6-round-robin} defines a round-robin \gls{lns} meta-heuristic, which
\Cref{lst:6-round-robin} defines a round-robin \gls{lns} meta-heuristic, which cycles cycles through a list of \mzninline{N} neighbourhoods \mzninline{nbhs}. To do
through a list of \mzninline{N} neighbourhoods \mzninline{nbhs}. To do this, it this, it uses the decision variable \mzninline{select}. In the initialisation
uses the decision variable \mzninline{select}. In the initialisation phase phase (\mzninline{status()=START}), \mzninline{select} is set to \mzninline{-1},
(\mzninline{status()=START}), \mzninline{select} is set to \mzninline{-1}, which which means none of the neighbourhoods is activated. In any following restart,
means none of the neighbourhoods is activated. In any following restart,
\mzninline{select} is incremented modulo \mzninline{N}, by accessing the last \mzninline{select} is incremented modulo \mzninline{N}, by accessing the last
value assigned in a previous restart (\mzninline{last_val(select)}). This will value assigned in a previous restart (\mzninline{last_val(select)}). This will
activate a different neighbourhood for each restart activate a different neighbourhood for each restart
(\lref{line:6:roundrobin:post}). (\lref{line:6:roundrobin:post}).
\begin{listing}[t] \begin{listing}
\highlightfile{assets/mzn/6_round_robin.mzn} \highlightfile{assets/mzn/6_round_robin.mzn}
\caption{\label{lst:6-round-robin} A predicate providing the round robin \caption{\label{lst:6-round-robin} A predicate providing the round robin
meta-heuristic} meta-heuristic}
\end{listing} \end{listing}
%\paragraph{Adaptive \gls{lns}} %\paragraph{Adaptive \gls{lns}}
For adaptive \gls{lns}, a simple strategy is to change the size of the neighbourhood For adaptive \gls{lns}, a simple strategy is to change the size of the
depending on whether the previous size was successful or not. neighbourhood depending on whether the previous size was successful or not.
\Cref{lst:6-adaptive} shows an adaptive version of the \Cref{lst:6-adaptive} shows an adaptive version of the
\mzninline{uniformNeighbourhood} that increases the number of free variables \mzninline{uniform_neighbourhood} that increases the number of free variables
when the previous restart failed, and decreases it when it succeeded, within the when the previous restart failed, and decreases it when it succeeded, within the
bounds $[0.6,0.95]$. bounds $[0.6,0.95]$.
\begin{listing}[t] \begin{listing}
\highlightfile{assets/mzn/6_adaptive.mzn} \highlightfile{assets/mzn/6_adaptive.mzn}
\caption{\label{lst:6-adaptive} A simple adaptive neighbourhood} \caption{\label{lst:6-adaptive} A simple adaptive neighbourhood}
\end{listing} \end{listing}
\subsection{Meta-heuristics} \subsection{Optimisation strategies}
The \gls{lns} strategies we have seen so far rely on the default behaviour of The \gls{lns} strategies we have seen so far rely on the default behaviour of
\minizinc\ solvers to use branch-and-bound for optimisation: when a new solution \minizinc\ solvers to use a branch-and-bound method for optimisation: when a new
is found, the solver adds a constraint to the remainder of the search to only solution is found, the solver adds a constraint to the remainder of the search
accept better solutions, as defined by the objective function in the to only accept better solutions, as defined by the objective function in the
\mzninline{minimize} or \mzninline{maximize} clause of the \mzninline{solve} \mzninline{minimize} or \mzninline{maximize} clause of the \mzninline{solve}
item. When combined with restarts and \gls{lns}, this is equivalent to a simple item. When combined with restarts and \gls{lns}, this is equivalent to a simple
hill-climbing meta-heuristic. hill-climbing meta-heuristic.
@ -336,25 +335,42 @@ branch-and-bound constraint on restart. It will still use the declared objective
to decide whether a new solution is the globally best one seen so far, and only to decide whether a new solution is the globally best one seen so far, and only
output those (to maintain the convention of \minizinc\ solvers that the last output those (to maintain the convention of \minizinc\ solvers that the last
solution printed at any point in time is the currently best known one). solution printed at any point in time is the currently best known one).
%
With \mzninline{restart_without_objective}, the restart predicate is now With \mzninline{restart_without_objective}, the restart predicate is now
responsible for constraining the objective function. Note that a simple responsible for constraining the objective function. Note that a simple
hill-climbing (for minimisation) can still be defined easily in this context as: hill-climbing (for minimisation) can still be defined easily in this context as:
{ \highlightfile{assets/mzn/6_hill_climbing.mzn}
\scriptsize
\highlightfile{assets/mzn/6_hill_climbing.mzn}
}
It takes advantage of the fact that the declared objective function is available It takes advantage of the fact that the declared objective function is available
through the built-in variable \mzninline{_objective}. through the built-in variable \mzninline{_objective}. A more interesting example
% is a simulated annealing strategy. When using this strategy, the solutions that
A simulated annealing strategy is also easy to the solver finds are no longer required to steadily improve in quality. Instead,
express: we ask the solver to find a solution that is a significant improvement over the
previous solution. Over time we decrease the amount by which we require the
solution needs to improve until we are just looking for any improvements. This
\gls{meta-search} can help improving the qualities of solutions quickly and
thereby reaching the optimal solution quicker. This strategy is also easy to
express using our restart-based modelling:
\highlightfile{assets/mzn/6_simulated_annealing.mzn} \highlightfile{assets/mzn/6_simulated_annealing.mzn}
\section{Compilation of Meta-Search} Using the same methods it is also possible to describe optimisation strategies
with multiple objectives. An example of such a strategy is lexicographic search.
Lexicographic search can be employed when there is a strict order between the
importance of different variables. It required that, once a solution is found,
each subsequent solution must either improve the first objective, or have the
same value for the first objective and improve the second objective, or have the
same value for the first two objectives and improve the third objective, and so
on. We can model this strategy restarts as such:
\highlightfile{assets/mzn/6_lex_minimize.mzn}
Another optimisation
\highlightfile{assets/mzn/6_pareto_optimal.mzn}
\section{Compilation of Meta-Search Specifications}
\label{sec:6-solver-extension} \label{sec:6-solver-extension}
The neighbourhoods defined in the previous section can be executed with The neighbourhoods defined in the previous section can be executed with
@ -380,7 +396,7 @@ in terms of standard \minizinc\ expressions, with the exception of a few new
built-in functions. When the neighbourhood predicates are evaluated in the built-in functions. When the neighbourhood predicates are evaluated in the
\minisearch\ way, the \minisearch\ runtime implements those built-in functions, \minisearch\ way, the \minisearch\ runtime implements those built-in functions,
computing the correct value whenever a predicate is evaluated. computing the correct value whenever a predicate is evaluated.
%
Instead, the compilation scheme presented below uses a limited form of Instead, the compilation scheme presented below uses a limited form of
\emph{partial evaluation}: parameters known at compile time will be fully \emph{partial evaluation}: parameters known at compile time will be fully
evaluated; those only known during the solving, such as the result of a call to evaluated; those only known during the solving, such as the result of a call to
@ -403,7 +419,7 @@ performs four simple steps:
\mzninline{sol}, \mzninline{status}, and \mzninline{last_val} as \mzninline{sol}, \mzninline{status}, and \mzninline{last_val} as
returning a \mzninline{var} instead of a \mzninline{par} value; and returning a \mzninline{var} instead of a \mzninline{par} value; and
rename calls to random functions, e.g., \mzninline{uniform} to rename calls to random functions, e.g., \mzninline{uniform} to
\mzninline{uniform_nbh}, in order to distinguish them from their \mzninline{uniform_slv}, in order to distinguish them from their
standard library versions. standard library versions.
\item Convert any expression containing a call from step 2 to \mzninline{var} \item Convert any expression containing a call from step 2 to \mzninline{var}
to ensure the functions are compiled as constraints, rather than to ensure the functions are compiled as constraints, rather than
@ -416,10 +432,11 @@ performs four simple steps:
These transformations will not change the code of many neighbourhood These transformations will not change the code of many neighbourhood
definitions, since the built-in functions are often used in positions that definitions, since the built-in functions are often used in positions that
accept both parameters and variables. For example, the accept both parameters and variables. For example, the
\mzninline{uniformNeighbourhood} predicate from \cref{lst:6-lns-minisearch-pred} \mzninline{uniform_neighbourhood} predicate from
uses \mzninline{uniform(0.0,1.0)} in an \mzninline{if} expression, and \cref{lst:6-lns-minisearch-pred} uses \mzninline{uniform(0.0, 1.0)} in an
\mzninline{sol(x[i])} in an equality constraint. Both expressions can be \mzninline{if} expression, and \mzninline{sol(x[i])} in an equality constraint.
translated to \flatzinc\ when the functions return a \mzninline{var}. Both expressions can be translated to \flatzinc\ when the functions return a
\mzninline{var}.
\subsection{Compiling the new built-ins} \subsection{Compiling the new built-ins}
@ -433,7 +450,7 @@ simply replaces the functional form by a predicate \mzninline{status} (declared
in \lref{line:6:status}), which constrains its local variable argument in \lref{line:6:status}), which constrains its local variable argument
\mzninline{stat} to take the status value. \mzninline{stat} to take the status value.
\begin{listing}[t] \begin{listing}
\highlightfile{assets/mzn/6_status.mzn} \highlightfile{assets/mzn/6_status.mzn}
\caption{\label{lst:6-status} MiniZinc definition of the \mzninline{status} function} \caption{\label{lst:6-status} MiniZinc definition of the \mzninline{status} function}
\end{listing} \end{listing}
@ -451,7 +468,7 @@ question becomes known at compile time, we use that value instead. Otherwise, we
replace the function call with a type specific \mzninline{int_sol} predicate, replace the function call with a type specific \mzninline{int_sol} predicate,
which is the constraint that will be executed by the solver. which is the constraint that will be executed by the solver.
% %
\begin{listing}[t] \begin{listing}
\highlightfile{assets/mzn/6_sol_function.mzn} \highlightfile{assets/mzn/6_sol_function.mzn}
\caption{\label{lst:6-int-sol} MiniZinc definition of the \mzninline{sol} \caption{\label{lst:6-int-sol} MiniZinc definition of the \mzninline{sol}
function for integer variables} function for integer variables}
@ -467,7 +484,7 @@ able to generate the most efficient \flatzinc\ code for expressions involving
\paragraph{Random number functions} \paragraph{Random number functions}
Calls to the random number functions have been renamed by appending Calls to the random number functions have been renamed by appending
\texttt{\_nbh}, so that the compiler does not simply evaluate them statically. \texttt{\_slv}, so that the compiler does not simply evaluate them statically.
The definition of these new functions follows the same pattern as for The definition of these new functions follows the same pattern as for
\mzninline{sol}, \mzninline{status}, and \mzninline{last_val}. The MiniZinc \mzninline{sol}, \mzninline{status}, and \mzninline{last_val}. The MiniZinc
definition of the \mzninline{uniform_nbh} function is shown in definition of the \mzninline{uniform_nbh} function is shown in
@ -479,13 +496,13 @@ Note that the function accepts variable arguments \mzninline{l} and
\mzninline{u}, so that it can be used in combination with other functions, such \mzninline{u}, so that it can be used in combination with other functions, such
as \mzninline{sol}. as \mzninline{sol}.
\begin{listing}[t] \begin{listing}
\highlightfile{assets/mzn/6_uniform_neighbourhood.mzn} \highlightfile{assets/mzn/6_uniform_slv.mzn}
\caption{\label{lst:6-int-rnd} MiniZinc definition of the \caption{\label{lst:6-int-rnd} MiniZinc definition of the
\mzninline{uniform_nbh} function for floats} \mzninline{uniform_nbh} function for floats}
\end{listing} \end{listing}
\subsection{Solver support for \gls{lns} \glsentrytext{flatzinc}} \subsection{Solver support for restart-based built-ins}
We will now show the minimal extensions required from a solver to interpret the We will now show the minimal extensions required from a solver to interpret the
new \flatzinc\ constraints and, consequently, to execute \gls{lns} definitions new \flatzinc\ constraints and, consequently, to execute \gls{lns} definitions
@ -500,10 +517,10 @@ new constraints the solver needs to:
\begin{itemize} \begin{itemize}
\item \mzninline{status(s)}: record the status of the previous restart, and \item \mzninline{status(s)}: record the status of the previous restart, and
fix \mzninline{s} to the recorded status. fix \mzninline{s} to the recorded status.
\item \mzninline{sol(x,sx)} (variants): constrain \mzninline{sx} to be equal \item \mzninline{sol(x, sx)} (variants): constrain \mzninline{sx} to be equal
to the value of \mzninline{x} in the incumbent solution. If there is no to the value of \mzninline{x} in the incumbent solution. If there is no
incumbent solution, it has no effect. incumbent solution, it has no effect.
\item \mzninline{last_val(x,lx)} (variants): constrain \mzninline{lx} to take \item \mzninline{last_val(x, lx)} (variants): constrain \mzninline{lx} to take
the last value assigned to \mzninline{x} during search. If no value was the last value assigned to \mzninline{x} during search. If no value was
ever assigned, it has no effect. Note that many solvers (in particular ever assigned, it has no effect. Note that many solvers (in particular
SAT and LCG solvers) already track \mzninline{last_val} for their SAT and LCG solvers) already track \mzninline{last_val} for their
@ -527,30 +544,33 @@ implemented these extensions for both Gecode (110 new lines of code) and Chuffed
For example, consider the model from \cref{lst:6-basic-complete} again. For example, consider the model from \cref{lst:6-basic-complete} again.
\Cref{lst:6-flat-pred} shows a part of the \flatzinc\ that arises from compiling \Cref{lst:6-flat-pred} shows a part of the \flatzinc\ that arises from compiling
\mzninline{basic_lns(uniformNeighbourhood(x, 0.2))}, assuming that \mzninline{basic_lns(uniform_neighbourhood(x, 0.2))}, assuming that
\mzninline{index_set(x) = 1..n}. \mzninline{index_set(x) = 1..n}.
\Lrefrange{line:6:status:start}{line:6:status:end} define a Boolean variable \Lrefrange{line:6:status:start}{line:6:status:end} define a Boolean variable
\mzninline{b1} that is true iff the status is not \mzninline{START}. The second \mzninline{b1} that is true if-and-only-if the status is not \mzninline{START}.
block of code (\lrefrange{line:6:x1:start}{line:6:x1:end}) represents the The second block of code (\lrefrange{line:6:x1:start}{line:6:x1:end}) represents
decomposition of the expression the decomposition of the expression
\highlightfile{assets/mzn/6_transformed_partial.mzn}
\mzninline{(status() != START /\ uniform(0.0,1.0) > 0.2) -> x[1] = sol(x[1])}
%
which is the result of merging the implication from the \mzninline{basic_lns} which is the result of merging the implication from the \mzninline{basic_lns}
predicate with the \mzninline{if} expression from predicate with the \mzninline{if} expression from
\mzninline{uniformNeighbourhood}. The code first introduces and constrains a \mzninline{uniformNeighbourhood}. The code first introduces and constrains a
variable for the random number, then adds two Boolean variables: \mzninline{b2} variable for the random number, then adds two Boolean variables: \mzninline{b2}
is constrained to be true iff the random number is greater than 0.2; while is constrained to be true if-and-only-if the random number is greater than
\mzninline{b3} is constrained to be the conjunction \mzninline{status()!=START \(0.2\); while \mzninline{b3} is constrained to be the conjunction of the two.
/\ uniform(0.0,1.0)>0.2}. \lref{line:6:x1} constrains \mzninline{x1} to be the \lref{line:6:x1} constrains \mzninline{x1} to be the value of \mzninline{x[1]}
value of \mzninline{x[1]} in the previous solution. Finally, the half-reified in the previous solution. Finally, the half-reified constraint in
constraint in \lref{line:6:x1:end} implements \mzninline{b3 -> x[1]=sol(x[1])}. \lref{line:6:x1:end} implements
\highlightfile{assets/mzn/6_transformed_half_reif.mzn}
We have omitted the similar code generated for \mzninline{x[2]} to We have omitted the similar code generated for \mzninline{x[2]} to
\mzninline{x[n]}. Note that the \flatzinc\ shown here has been simplified for \mzninline{x[n]}. Note that the \flatzinc\ shown here has been simplified for
presentation. presentation.
\begin{listing}[t] \begin{listing}
\highlightfile{assets/mzn/6_basic_complete_transformed.mzn} \highlightfile{assets/mzn/6_basic_complete_transformed.mzn}
\caption{\label{lst:6-flat-pred} \flatzinc\ that results from compiling \\ \caption{\label{lst:6-flat-pred} \flatzinc\ that results from compiling \\
\mzninline{basic_lns(uniformNeighbourhood(x,0.2))}.} \mzninline{basic_lns(uniformNeighbourhood(x,0.2))}.}
@ -562,28 +582,28 @@ and \mzninline{b3} to \mzninline{false}. Therefore, the implication in
\lref{line:6:x1:end} is not activated, leaving \mzninline{x[1]} unconstrained. \lref{line:6:x1:end} is not activated, leaving \mzninline{x[1]} unconstrained.
The neighbourhood constraints are effectively switched off. The neighbourhood constraints are effectively switched off.
When the solver restarts, all of the special propagators are re-executed. When the solver restarts, all of the special propagators are re-executed. Now
Now \mzninline{s} is not 1, and \mzninline{b1} will be set to \mzninline{s} is not 1, and \mzninline{b1} will be set to \mzninline{true}. The
\mzninline{true}. The \mzninline{float_random} propagator assigns \mzninline{float_random} propagator assigns \mzninline{rnd1} a new random value
\mzninline{rnd1} a new random value and, depending on whether it is greater and, depending on whether it is greater than \mzninline{0.2}, the Boolean
than \mzninline{0.2}, the Boolean variables \mzninline{b2}, and consequently variables \mzninline{b2}, and consequently \mzninline{b3} will be assigned. If
\mzninline{b3} will be assigned. If it is \mzninline{true}, the constraint it is \mzninline{true}, the constraint in line \lref{line:6:x1:end} will become
in line \lref{line:6:x1:end} will become active and assign \mzninline{x[1]} active and assign \mzninline{x[1]} to its value in the previous solution.
to its value in the previous solution.
Furthermore, it is not strictly necessary to guard \mzninline{int_uniform} Furthermore, it is not strictly necessary to guard \mzninline{int_uniform}
against being invoked before \mzninline{status()!=START}, since the against being invoked before the first solution is found, since the
\mzninline{sol} constraints will simply not propagate anything in case no \mzninline{sol} constraints will simply not propagate anything in case no
solution has been recorded yet, but we use this simple example to illustrate solution has been recorded yet, but we use this simple example to illustrate how
how these Boolean conditions are compiled and evaluated. these Boolean conditions are compiled and evaluated.
\section{An Incremental Interface for Constraint Modelling Languages} \section{An Incremental Interface for Constraint Modelling Languages}
\label{sec:6-incremental-compilation} \label{sec:6-incremental-compilation}
In order to support incremental flattening, the \nanozinc\ interpreter must be In order to support incremental flattening, the \nanozinc\ interpreter must be
able to process \nanozinc\ calls \emph{added} to an existing \nanozinc\ program, able to process \nanozinc\ calls \emph{added} to an existing \nanozinc\ program,
as well as to \emph{remove} calls from an existing \nanozinc\ program. Adding new as well as to \emph{remove} calls from an existing \nanozinc\ program. Adding
calls is straightforward, since \nanozinc\ is already processed call-by-call. new calls is straightforward, since \nanozinc\ is already processed
call-by-call.
Removing a call, however, is not so simple. When we remove a call, all effects Removing a call, however, is not so simple. When we remove a call, all effects
the call had on the \nanozinc\ program have to be undone, including results of the call had on the \nanozinc\ program have to be undone, including results of
@ -854,7 +874,7 @@ periods, which is done via the variables \mzninline{period_of} in the model.
\cref{lst:6-free-period} shows the neighbourhood chosen, which randomly picks one \cref{lst:6-free-period} shows the neighbourhood chosen, which randomly picks one
period and frees all courses that are assigned to it. period and frees all courses that are assigned to it.
\begin{table}[t] \begin{table}
\centering \centering
\input{assets/table/6_gbac} \input{assets/table/6_gbac}
\caption{\label{tab:6-gbac}\texttt{gbac} benchmarks} \caption{\label{tab:6-gbac}\texttt{gbac} benchmarks}
@ -868,7 +888,7 @@ Gecode. However, \gls{lns} again significantly improves over standard Chuffed.
\subsubsection{\texttt{steelmillslab}} \subsubsection{\texttt{steelmillslab}}
\begin{listing}[t] \begin{listing}
\highlightfile{assets/mzn/6_steelmillslab_neighbourhood.mzn} \highlightfile{assets/mzn/6_steelmillslab_neighbourhood.mzn}
\caption{\label{lst:6-free-bin}\texttt{steelmillslab}: Neighbourhood that frees \caption{\label{lst:6-free-bin}\texttt{steelmillslab}: Neighbourhood that frees
all orders assigned to a selected slab.} all orders assigned to a selected slab.}
@ -884,7 +904,7 @@ that randomly selects a slab and frees the orders assigned to it in the
incumbent solution. These orders can then be freely reassigned to any other incumbent solution. These orders can then be freely reassigned to any other
slab. slab.
\begin{table}[t] \begin{table}
\centering \centering
\input{assets/table/6_steelmillslab} \input{assets/table/6_steelmillslab}
\caption{\label{tab:6-steelmillslab}\texttt{steelmillslab} benchmarks} \caption{\label{tab:6-steelmillslab}\texttt{steelmillslab} benchmarks}
@ -901,7 +921,7 @@ outperforms \gecodeStd on this problem, once we use \gls{lns}, the learning in
% RCPSP/wet % RCPSP/wet
\subsubsection{\texttt{rcpsp-wet}} \subsubsection{\texttt{rcpsp-wet}}
\begin{listing}[t] \begin{listing}
\highlightfile{assets/mzn/6_rcpsp_neighbourhood.mzn} \highlightfile{assets/mzn/6_rcpsp_neighbourhood.mzn}
\caption{\label{lst:6-free-timeslot}\texttt{rcpsp-wet}: Neighbourhood freeing \caption{\label{lst:6-free-timeslot}\texttt{rcpsp-wet}: Neighbourhood freeing
all tasks starting in the drawn interval.} all tasks starting in the drawn interval.}

View File

@ -39,11 +39,11 @@ following publication:
\end{refsection} \end{refsection}
\mainmatter{} \mainmatter{}
\include{chapters/1_introduction} % \include{chapters/1_introduction}
\include{chapters/2_background} % \include{chapters/2_background}
\include{chapters/3_paradigms} % \include{chapters/3_paradigms}
\include{chapters/4_rewriting} % \include{chapters/4_rewriting}
\include{chapters/5_half_reif} % \include{chapters/5_half_reif}
\include{chapters/6_incremental} \include{chapters/6_incremental}
\backmatter{} \backmatter{}