From a04e3bee7e310fe6e5a336872de59f079b314f0f Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Wed, 24 Feb 2021 17:09:07 +1100 Subject: [PATCH] More work on the incremental chapter --- Pipfile.lock | 8 +- assets/glossary.tex | 2 +- assets/mzn/2_knapsack.mzntex | 2 +- assets/mzn/6_abs_reif_result.mzntex | 2 +- assets/mzn/6_abs_reif_trail.mzntex | 2 +- assets/mzn/6_adaptive.mzn | 23 +- assets/mzn/6_adaptive.mzntex | 25 +- assets/mzn/6_basic_complete.mzn | 7 +- assets/mzn/6_basic_complete.mzntex | 9 +- assets/mzn/6_basic_complete_transformed.mzn | 4 +- .../mzn/6_basic_complete_transformed.mzntex | 6 +- assets/mzn/6_basic_lns.mzn | 1 + assets/mzn/6_basic_lns.mzntex | 3 + assets/mzn/6_gbac_neighbourhood.mzntex | 2 +- assets/mzn/6_hill_climbing.mzn | 4 +- assets/mzn/6_hill_climbing.mzntex | 6 +- assets/mzn/6_incremental.mzntex | 2 +- assets/mzn/6_lex_minimize.mzn | 25 ++ assets/mzn/6_lex_minimize.mzntex | 27 +++ assets/mzn/6_lns_minisearch.mzn | 17 +- assets/mzn/6_lns_minisearch.mzntex | 19 +- assets/mzn/6_lns_minisearch_pred.mzn | 9 +- assets/mzn/6_lns_minisearch_pred.mzntex | 11 +- assets/mzn/6_pareto_optimal.mzn | 19 ++ assets/mzn/6_pareto_optimal.mzntex | 21 ++ assets/mzn/6_rcpsp_neighbourhood.mzntex | 2 +- assets/mzn/6_restart_ann.mzntex | 2 +- assets/mzn/6_round_robin.mzn | 21 +- assets/mzn/6_round_robin.mzntex | 23 +- assets/mzn/6_simulated_annealing.mzn | 12 +- assets/mzn/6_simulated_annealing.mzntex | 14 +- assets/mzn/6_sol_function.mzn | 12 +- assets/mzn/6_sol_function.mzntex | 14 +- assets/mzn/6_state_access.mzn | 1 + assets/mzn/6_state_access.mzntex | 3 +- assets/mzn/6_status.mzn | 7 +- assets/mzn/6_status.mzntex | 9 +- .../mzn/6_steelmillslab_neighbourhood.mzntex | 2 +- assets/mzn/6_transformed_half_reif.mzn | 1 + assets/mzn/6_transformed_half_reif.mzntex | 3 + assets/mzn/6_transformed_partial.mzn | 1 + assets/mzn/6_transformed_partial.mzntex | 3 + assets/mzn/6_uniform_neighbourhood.mzn | 6 - assets/mzn/6_uniform_neighbourhood.mzntex | 8 - assets/mzn/6_uniform_slv.mzn | 6 + assets/mzn/6_uniform_slv.mzntex | 8 + assets/py/2_dyn_knapsack.pytex | 2 +- chapters/6_incremental.tex | 218 ++++++++++-------- dekker_thesis.tex | 10 +- 49 files changed, 407 insertions(+), 237 deletions(-) create mode 100644 assets/mzn/6_basic_lns.mzn create mode 100644 assets/mzn/6_basic_lns.mzntex create mode 100644 assets/mzn/6_lex_minimize.mzn create mode 100644 assets/mzn/6_lex_minimize.mzntex create mode 100644 assets/mzn/6_pareto_optimal.mzn create mode 100644 assets/mzn/6_pareto_optimal.mzntex create mode 100644 assets/mzn/6_transformed_half_reif.mzn create mode 100644 assets/mzn/6_transformed_half_reif.mzntex create mode 100644 assets/mzn/6_transformed_partial.mzn create mode 100644 assets/mzn/6_transformed_partial.mzntex delete mode 100644 assets/mzn/6_uniform_neighbourhood.mzn delete mode 100644 assets/mzn/6_uniform_neighbourhood.mzntex create mode 100644 assets/mzn/6_uniform_slv.mzn create mode 100644 assets/mzn/6_uniform_slv.mzntex diff --git a/Pipfile.lock b/Pipfile.lock index 31d0ad6..4215dbf 100644 --- a/Pipfile.lock +++ b/Pipfile.lock @@ -26,15 +26,15 @@ }, "minizinc-python": { "git": "https://github.com/MiniZinc/minizinc-python", - "ref": "5231948b09c4fe8ed3780b3c71abed75d038a759" + "ref": "0becdd6e346c1021b26901de44dc1fc7fd9ac48c" }, "pygments": { "hashes": [ - "sha256:bc9591213a8f0e0ca1a5e68a479b4887fdc3e75d0774e5c71c31920c427de435", - "sha256:df49d09b498e83c1a73128295860250b0b7edd4c723a32e9bc0d295c7c2ec337" + "sha256:37a13ba168a02ac54cc5891a42b1caec333e59b66addb7fa633ea8a6d73445c0", + "sha256:b21b072d0ccdf29297a82a2363359d99623597b8a265b8081760e4d0f7153c88" ], "index": "pypi", - "version": "==2.7.4" + "version": "==2.8.0" } }, "develop": {} diff --git a/assets/glossary.tex b/assets/glossary.tex index 2d66f59..e3b682c 100644 --- a/assets/glossary.tex +++ b/assets/glossary.tex @@ -64,7 +64,7 @@ dedicated algorithms or rewriting rules to better handle the global constraint}, \newglossaryentry{gls-lns}{ name={large neighbourhood search}, 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}, } diff --git a/assets/mzn/2_knapsack.mzntex b/assets/mzn/2_knapsack.mzntex index 13159d1..19f14f7 100644 --- a/assets/mzn/2_knapsack.mzntex +++ b/assets/mzn/2_knapsack.mzntex @@ -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{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}{;} diff --git a/assets/mzn/6_abs_reif_result.mzntex b/assets/mzn/6_abs_reif_result.mzntex index 9dbca26..c7b9a86 100644 --- a/assets/mzn/6_abs_reif_result.mzntex +++ b/assets/mzn/6_abs_reif_result.mzntex @@ -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}{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}{]} diff --git a/assets/mzn/6_abs_reif_trail.mzntex b/assets/mzn/6_abs_reif_trail.mzntex index c3576ac..70ee3ca 100644 --- a/assets/mzn/6_abs_reif_trail.mzntex +++ b/assets/mzn/6_abs_reif_trail.mzntex @@ -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{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} diff --git a/assets/mzn/6_adaptive.mzn b/assets/mzn/6_adaptive.mzn index 454ab97..1c3570f 100644 --- a/assets/mzn/6_adaptive.mzn +++ b/assets/mzn/6_adaptive.mzn @@ -1,8 +1,15 @@ -predicate adaptiveUniform(array[int] of var int: x, float: initialDestrRate) = - let { var float: rate; } in - if status() = START then rate = initialDestrRate - elseif status() = UNSAT then rate = min(last_val(rate)-0.02,0.6) - 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]) else true endif); +predicate adaptive_uniform(array[int] of var int: x, float: init_rate) = + let { + var float: rate; + } in if status() = START then + rate = init_rate + elseif status() = UNSAT then + rate = min(last_val(rate) - 0.02, 0.6) + 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 + ); diff --git a/assets/mzn/6_adaptive.mzntex b/assets/mzn/6_adaptive.mzntex index 0dda622..2c9c9bd 100644 --- a/assets/mzn/6_adaptive.mzntex +++ b/assets/mzn/6_adaptive.mzntex @@ -1,10 +1,17 @@ -\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}{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{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}{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{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{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{k}{endif}\PY{l+s}{ }\PY{o}{/\PYZbs{}} -\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{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}{;} +\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}{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{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{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}{rate}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{init\PYZus{}rate} +\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+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{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} diff --git a/assets/mzn/6_basic_complete.mzn b/assets/mzn/6_basic_complete.mzn index 64f4348..08a26db 100644 --- a/assets/mzn/6_basic_complete.mzn +++ b/assets/mzn/6_basic_complete.mzn @@ -1,8 +1,11 @@ array[1..n] of var 1..n: x; % decision variables var int: cost; % objective function -% ... some constraints defining the problem + +% --- some constraints defining the problem --- + % 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 ::on_restart("my_lns") ::restart_constant(500) ::timeout(120) minimize cost; diff --git a/assets/mzn/6_basic_complete.mzntex b/assets/mzn/6_basic_complete.mzntex index 841b81a..d4d906e 100644 --- a/assets/mzn/6_basic_complete.mzntex +++ b/assets/mzn/6_basic_complete.mzntex @@ -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}{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{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{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}{;} diff --git a/assets/mzn/6_basic_complete_transformed.mzn b/assets/mzn/6_basic_complete_transformed.mzn index e4a4986..7fda0ef 100644 --- a/assets/mzn/6_basic_complete_transformed.mzn +++ b/assets/mzn/6_basic_complete_transformed.mzn @@ -1,7 +1,7 @@ var 1..5: s;@ \Vlabel{line:6:status:start}@ constraint status(s); 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}@ constraint float_uniform(0.0,1.0,rnd1); @@ -11,6 +11,6 @@ var bool: b3; constraint bool_and(b1,b2,b3); var 1..3: 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}@ @...@ diff --git a/assets/mzn/6_basic_complete_transformed.mzntex b/assets/mzn/6_basic_complete_transformed.mzntex index bea0ac7..79eb808 100644 --- a/assets/mzn/6_basic_complete_transformed.mzntex +++ b/assets/mzn/6_basic_complete_transformed.mzntex @@ -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}{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}{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}{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+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{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{esc}{...} \end{Verbatim} diff --git a/assets/mzn/6_basic_lns.mzn b/assets/mzn/6_basic_lns.mzn new file mode 100644 index 0000000..79bcc87 --- /dev/null +++ b/assets/mzn/6_basic_lns.mzn @@ -0,0 +1 @@ +predicate basic_lns(var bool: nbh) = (status()!=START -> nbh); diff --git a/assets/mzn/6_basic_lns.mzntex b/assets/mzn/6_basic_lns.mzntex new file mode 100644 index 0000000..ef92a21 --- /dev/null +++ b/assets/mzn/6_basic_lns.mzntex @@ -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} diff --git a/assets/mzn/6_gbac_neighbourhood.mzntex b/assets/mzn/6_gbac_neighbourhood.mzntex index 0a97611..732e1ab 100644 --- a/assets/mzn/6_gbac_neighbourhood.mzntex +++ b/assets/mzn/6_gbac_neighbourhood.mzntex @@ -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{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}{(} diff --git a/assets/mzn/6_hill_climbing.mzn b/assets/mzn/6_hill_climbing.mzn index 9f2cb53..c79f793 100644 --- a/assets/mzn/6_hill_climbing.mzn +++ b/assets/mzn/6_hill_climbing.mzn @@ -1,3 +1 @@ -predicate hill_climbing() = - if status()=START then true - else _objective < sol(_objective) endif; +predicate hill_climbing() = status() != START -> _objective < sol(_objective); diff --git a/assets/mzn/6_hill_climbing.mzntex b/assets/mzn/6_hill_climbing.mzntex index f9a314f..5f7b579 100644 --- a/assets/mzn/6_hill_climbing.mzntex +++ b/assets/mzn/6_hill_climbing.mzntex @@ -1,5 +1,3 @@ -\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}{hill\PYZus{}climbing}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=} -\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}{;} +\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{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}{;} \end{Verbatim} diff --git a/assets/mzn/6_incremental.mzntex b/assets/mzn/6_incremental.mzntex index d17c9d5..2e1142a 100644 --- a/assets/mzn/6_incremental.mzntex +++ b/assets/mzn/6_incremental.mzntex @@ -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}{y}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nv}{x}\PY{p}{;} \end{Verbatim} diff --git a/assets/mzn/6_lex_minimize.mzn b/assets/mzn/6_lex_minimize.mzn new file mode 100644 index 0000000..91b835b --- /dev/null +++ b/assets/mzn/6_lex_minimize.mzn @@ -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; diff --git a/assets/mzn/6_lex_minimize.mzntex b/assets/mzn/6_lex_minimize.mzntex new file mode 100644 index 0000000..f2fe5ef --- /dev/null +++ b/assets/mzn/6_lex_minimize.mzntex @@ -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} diff --git a/assets/mzn/6_lns_minisearch.mzn b/assets/mzn/6_lns_minisearch.mzn index 333a36a..60e8be9 100644 --- a/assets/mzn/6_lns_minisearch.mzn +++ b/assets/mzn/6_lns_minisearch.mzn @@ -1,8 +1,13 @@ function ann: lns(var int: obj, array[int] of var int: vars, int: iterations, float: destr_rate, int: explore_time) = - repeat (i in 1..iterations) ( scope( - if has_sol() then post(uniform_neighbourhood(vars, destr_rate)) - else true endif /\ - time_limit(explore_time, minimize_bab(obj)) /\ - commit() /\ print() - ) /\ post(obj < sol(obj)) ); + repeat (i in 1..iterations) ( + scope( + if has_sol() then + post(uniform_neighbourhood(vars, destr_rate)) + endif + /\ time_limit(explore_time, minimize_bab(obj)) + /\ commit() + /\ print() + ) + /\ post(obj < sol(obj)) + ); diff --git a/assets/mzn/6_lns_minisearch.mzntex b/assets/mzn/6_lns_minisearch.mzntex index 9a7504d..58dca4f 100644 --- a/assets/mzn/6_lns_minisearch.mzntex +++ b/assets/mzn/6_lns_minisearch.mzntex @@ -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{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{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{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{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{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{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{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{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}{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{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{k}{endif} +\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} diff --git a/assets/mzn/6_lns_minisearch_pred.mzn b/assets/mzn/6_lns_minisearch_pred.mzn index 953d563..3fc1379 100644 --- a/assets/mzn/6_lns_minisearch_pred.mzn +++ b/assets/mzn/6_lns_minisearch_pred.mzn @@ -1,3 +1,6 @@ -predicate uniform_neighbourhood(array[int] of var int: x, float: destrRate) = - forall(i in index_set(x)) - (if uniform(0.0,1.0) > destrRate then x[i] = sol(x[i]) else true endif); +predicate uniform_neighbourhood(array[int] of var int: x, float: destr_rate) = + forall(i in index_set(x)) ( + if uniform(0.0, 1.0) > destr_rate then + x[i] = sol(x[i]) + endif + ); diff --git a/assets/mzn/6_lns_minisearch_pred.mzntex b/assets/mzn/6_lns_minisearch_pred.mzntex index 2ae231b..6567b23 100644 --- a/assets/mzn/6_lns_minisearch_pred.mzntex +++ b/assets/mzn/6_lns_minisearch_pred.mzntex @@ -1,5 +1,8 @@ -\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}{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{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{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}{;} +\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}{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{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} diff --git a/assets/mzn/6_pareto_optimal.mzn b/assets/mzn/6_pareto_optimal.mzn new file mode 100644 index 0000000..74e587b --- /dev/null +++ b/assets/mzn/6_pareto_optimal.mzn @@ -0,0 +1,19 @@ +predicate pareto_optimal(var int: obj1, var int: obj2) = + let { + int: ms = 1000; % max solutions + var 0..ms: nsol; % number of solutions + set of int: SOL = 1..ms; + array[SOL] of var lb(obj1)..ub(obj1): s1; + array[SOL] of var lb(obj2)..ub(obj2): s2; + } in if status() = START then + nsol = 0 + elseif status() = UNSAT then + complete() % we are finished! + elseif + nsol = sol(nsol) + 1 /\ + s1[nsol] = sol(obj1) /\ + s2[nsol] = sol(obj2) + endif + /\ for(i in 1..nsol) ( + obj1 < lastval(s1[i]) \/ obj2 < lastval(s2[i]) + ); diff --git a/assets/mzn/6_pareto_optimal.mzntex b/assets/mzn/6_pareto_optimal.mzntex new file mode 100644 index 0000000..e310530 --- /dev/null +++ b/assets/mzn/6_pareto_optimal.mzntex @@ -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} diff --git a/assets/mzn/6_rcpsp_neighbourhood.mzntex b/assets/mzn/6_rcpsp_neighbourhood.mzntex index a1d3ba5..6a0f016 100644 --- a/assets/mzn/6_rcpsp_neighbourhood.mzntex +++ b/assets/mzn/6_rcpsp_neighbourhood.mzntex @@ -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{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} diff --git a/assets/mzn/6_restart_ann.mzntex b/assets/mzn/6_restart_ann.mzntex index db613a5..9fd2ea1 100644 --- a/assets/mzn/6_restart_ann.mzntex +++ b/assets/mzn/6_restart_ann.mzntex @@ -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{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} diff --git a/assets/mzn/6_round_robin.mzn b/assets/mzn/6_round_robin.mzn index 989332d..f7c626b 100644 --- a/assets/mzn/6_round_robin.mzn +++ b/assets/mzn/6_round_robin.mzn @@ -1,11 +1,12 @@ predicate round_robin(array[int] of var bool: nbhs) = - let { - int: N = length(nbhs); - var -1..N-1: select; % Neighbourhood selection - } in if status()=START then - select= -1 - else - select= (last_val(select) + 1) mod N - endif /\ forall(i in 1..N) ( - select=i-1 -> nbhs[i] @\Vlabel{line:6:roundrobin:post}@ - ); + let { + int: N = length(nbhs); + var -1..N-1: select; % Neighbourhood selection + } in if status()=START then + select = -1 + else + select = (last_val(select) + 1) mod N + endif + /\ forall(i in 1..N) ( + select = i-1 -> nbhs[i] @\Vlabel{line:6:roundrobin:post}@ + ); diff --git a/assets/mzn/6_round_robin.mzntex b/assets/mzn/6_round_robin.mzntex index 64ffaa4..d38c7e0 100644 --- a/assets/mzn/6_round_robin.mzntex +++ b/assets/mzn/6_round_robin.mzntex @@ -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{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}{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{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{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{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{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{l+s}{ }\PY{l+s}{ }\PY{p}{)}\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{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}{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{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{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{k}{else} +\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{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{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{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} diff --git a/assets/mzn/6_simulated_annealing.mzn b/assets/mzn/6_simulated_annealing.mzn index 9f1c6cf..d8a16b3 100644 --- a/assets/mzn/6_simulated_annealing.mzn +++ b/assets/mzn/6_simulated_annealing.mzn @@ -1,7 +1,9 @@ -predicate simulated_annealing(float: initTemp, float: coolingRate) = - let { var float: temp; } in - if status()=START then temp = initTemp +predicate simulated_annealing(float: init_temp, float: cooling_rate) = + let { + var float: temp; + } in if status() = START then + temp = init_temp else - temp = last_val(temp)*(1-coolingRate) /\ % cool down - _objective < sol(_objective) - ceil(log(uniform(0.0,1.0)) * temp) + temp = last_val(temp) * (1 - cooling_rate) % cool down + /\ _objective < sol(_objective) - ceil(log(uniform(0.0, 1.0)) * temp) endif; diff --git a/assets/mzn/6_simulated_annealing.mzntex b/assets/mzn/6_simulated_annealing.mzntex index 06724c6..47b3276 100644 --- a/assets/mzn/6_simulated_annealing.mzntex +++ b/assets/mzn/6_simulated_annealing.mzntex @@ -1,9 +1,11 @@ -\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}{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{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}{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} +\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}{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{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{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{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{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{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}{;} \end{Verbatim} diff --git a/assets/mzn/6_sol_function.mzn b/assets/mzn/6_sol_function.mzn index 9086230..ea9725a 100644 --- a/assets/mzn/6_sol_function.mzn +++ b/assets/mzn/6_sol_function.mzn @@ -1,8 +1,10 @@ predicate int_sol(var int: x, var int: xi); function int: sol(var int: x) = - if is_fixed(x) then fix(x) - else let { - var lb(x)..ub(x): xi; - constraint int_sol(x,xi); + if is_fixed(x) then + fix(x) + else + let { + var lb(x)..ub(x): xi; + constraint int_sol(x,xi); } in xi; - endif; + endif; diff --git a/assets/mzn/6_sol_function.mzntex b/assets/mzn/6_sol_function.mzntex index e2dff85..80e808f 100644 --- a/assets/mzn/6_sol_function.mzntex +++ b/assets/mzn/6_sol_function.mzntex @@ -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}{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{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{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{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{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{n+nb}{fix}\PY{p}{(}\PY{n+nv}{x}\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}{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{k}{endif}\PY{p}{;} +\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}\PY{p}{;} \end{Verbatim} diff --git a/assets/mzn/6_state_access.mzn b/assets/mzn/6_state_access.mzn index 0e20cc9..a2f2686 100644 --- a/assets/mzn/6_state_access.mzn +++ b/assets/mzn/6_state_access.mzn @@ -1,5 +1,6 @@ % Report the status of the solver (before restarting). enum STATUS = {START, UNKNOWN, UNSAT, SAT, OPT} @\label{ann:enum_status}@ function STATUS: status(); @\label{ann:status}@ + % Provide access to the last assigned value of variable x. function int: last_val(var int: x); diff --git a/assets/mzn/6_state_access.mzntex b/assets/mzn/6_state_access.mzntex index 2743aaf..a63a3a7 100644 --- a/assets/mzn/6_state_access.mzntex +++ b/assets/mzn/6_state_access.mzntex @@ -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{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{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}{;} \end{Verbatim} diff --git a/assets/mzn/6_status.mzn b/assets/mzn/6_status.mzn index d90c637..bd4ace5 100644 --- a/assets/mzn/6_status.mzn +++ b/assets/mzn/6_status.mzn @@ -1,5 +1,6 @@ predicate status(var int: stat); @\Vlabel{line:6:status}@ function var STATUS: status() = - let { var STATUS: stat; - constraint status(stat); - } in stat; + let { + var STATUS: stat; + constraint status(stat); + } in stat; diff --git a/assets/mzn/6_status.mzntex b/assets/mzn/6_status.mzntex index 8d25a18..a7a0803 100644 --- a/assets/mzn/6_status.mzntex +++ b/assets/mzn/6_status.mzntex @@ -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}{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{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{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}\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{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{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} diff --git a/assets/mzn/6_steelmillslab_neighbourhood.mzntex b/assets/mzn/6_steelmillslab_neighbourhood.mzntex index 3498fe5..e82aa45 100644 --- a/assets/mzn/6_steelmillslab_neighbourhood.mzntex +++ b/assets/mzn/6_steelmillslab_neighbourhood.mzntex @@ -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{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}{)} diff --git a/assets/mzn/6_transformed_half_reif.mzn b/assets/mzn/6_transformed_half_reif.mzn new file mode 100644 index 0000000..4d2c228 --- /dev/null +++ b/assets/mzn/6_transformed_half_reif.mzn @@ -0,0 +1 @@ +b3 -> x[1] = sol(x[1]) diff --git a/assets/mzn/6_transformed_half_reif.mzntex b/assets/mzn/6_transformed_half_reif.mzntex new file mode 100644 index 0000000..01c02e8 --- /dev/null +++ b/assets/mzn/6_transformed_half_reif.mzntex @@ -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} diff --git a/assets/mzn/6_transformed_partial.mzn b/assets/mzn/6_transformed_partial.mzn new file mode 100644 index 0000000..5a51d90 --- /dev/null +++ b/assets/mzn/6_transformed_partial.mzn @@ -0,0 +1 @@ +(status() != START /\ uniform(0.0,1.0) > 0.2) -> x[1] = sol(x[1]) diff --git a/assets/mzn/6_transformed_partial.mzntex b/assets/mzn/6_transformed_partial.mzntex new file mode 100644 index 0000000..f17f311 --- /dev/null +++ b/assets/mzn/6_transformed_partial.mzntex @@ -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} diff --git a/assets/mzn/6_uniform_neighbourhood.mzn b/assets/mzn/6_uniform_neighbourhood.mzn deleted file mode 100644 index 650360a..0000000 --- a/assets/mzn/6_uniform_neighbourhood.mzn +++ /dev/null @@ -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; diff --git a/assets/mzn/6_uniform_neighbourhood.mzntex b/assets/mzn/6_uniform_neighbourhood.mzntex deleted file mode 100644 index ea5d157..0000000 --- a/assets/mzn/6_uniform_neighbourhood.mzntex +++ /dev/null @@ -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} diff --git a/assets/mzn/6_uniform_slv.mzn b/assets/mzn/6_uniform_slv.mzn new file mode 100644 index 0000000..f174b62 --- /dev/null +++ b/assets/mzn/6_uniform_slv.mzn @@ -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; diff --git a/assets/mzn/6_uniform_slv.mzntex b/assets/mzn/6_uniform_slv.mzntex new file mode 100644 index 0000000..ea5aa9b --- /dev/null +++ b/assets/mzn/6_uniform_slv.mzntex @@ -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} diff --git a/assets/py/2_dyn_knapsack.pytex b/assets/py/2_dyn_knapsack.pytex index 776e3ee..8d9c1a6 100644 --- a/assets/py/2_dyn_knapsack.pytex +++ b/assets/py/2_dyn_knapsack.pytex @@ -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{}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} diff --git a/chapters/6_incremental.tex b/chapters/6_incremental.tex index 00aa38c..16b60ba 100644 --- a/chapters/6_incremental.tex +++ b/chapters/6_incremental.tex @@ -55,22 +55,22 @@ still prove prohibitive, warranting direct support from the methods to provide this support: \begin{itemize} - \item Using a minimal extension of existing solvers, we can compile - \gls{meta-search} algorithms into efficient solver-level specifications - based on solver restart, avoiding re-compilation all-together. - \item We can add an interface for adding and removing constraints in the - \gls{constraint-modelling} infrastructure and avoid re-compilation where - possible. + \item We introduce the notion of restart-based \gls{meta-search} algorithms. + Using a minimal extension to a \cml\ and its target solver, we can model + some \gls{meta-search} algorithms and compile \gls{meta-search} + algorithms into efficient solver-level specifications based on solver + restarts, avoiding re-compilation all-together. + \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} -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} -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 \gls{meta-search} specifications into efficient solver-level specifications that 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. -\section{Modelling of Meta-Search} +\section{Modelling of Restart-Based Meta-Search} \label{sec:6-modelling} 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} annotation in \cref{lst:6-restart-ann}). -The second component of our \gls{lns} definition is the \emph{restarting strategy}, -defining how much effort the solver should put into each neighbourhood (\ie\ -restart), and when to stop the overall search. +The second component of our \gls{lns} definition is the \emph{restarting + strategy}, defining how much effort the solver should put into each +neighbourhood (\ie\ restart), and when to stop the overall search. We propose adding new search annotations to \minizinc\ to control this behaviour (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 search after a fixed number of restarts. -\begin{listing}[t] +\begin{listing} \highlightfile{assets/mzn/6_restart_ann.mzn} \caption{\label{lst:6-restart-ann} New annotations to control the restarting 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 basic \gls{lns} algorithm, more advanced \gls{meta-search} algorithms will -require more then just reapplying the same \gls{neighbourhood} time after time. -It is, for example, often beneficial to use several \gls{neighbourhood} -definitions for a problem. Different \glspl{neighbourhood} may be able to -improve different aspects of a solution, at different phases of the search. -Adaptive \gls{lns} \autocite{ropke-2006-adaptive, pisinger-2007-heuristic}, -which keeps track of the \glspl{neighbourhood} that led to improvements and -favours them for future iterations, is the prime example for this approach. A -simpler scheme may apply several \glspl{neighbourhood} in a round-robin fashion. +require more then reapplying the same \gls{neighbourhood} time after time. It +is, for example, often beneficial to use several \gls{neighbourhood} definitions +for a problem. Different \glspl{neighbourhood} may be able to improve different +aspects of a solution, at different phases of the search. Adaptive \gls{lns} +\autocite{ropke-2006-adaptive, pisinger-2007-heuristic}, which keeps track of +the \glspl{neighbourhood} that led to improvements and favours them for future +iterations, is the prime example for this approach. A simpler scheme may apply +several \glspl{neighbourhood} in a round-robin fashion. In \minisearch\, these adaptive or round-robin approaches can be implemented 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 undefined if \mzninline{status()=START}). -\begin{listing}[t] +\begin{listing} \highlightfile{assets/mzn/6_state_access.mzn} \caption{\label{lst:6-state-access} Functions for accessing previous solver 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 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 -cannot simply pass \mzninline{basic_lns(uniformNeighbourhood(x,0.2))}. First of -all, calling \mzninline{uniformNeighbourhood} like that would result in a +cannot simply pass \mzninline{basic_lns(uniform_neighbourhood(x, 0.2))}. First +of all, calling \mzninline{uniform_neighbourhood} like that would result in a \emph{single} evaluation of the predicate, since \minizinc\ employs a call-by-value evaluation strategy. Furthermore, the \mzninline{on_restart} 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} shows a complete example of a basic \gls{lns} model. -\begin{listing}[t] +\begin{listing} \highlightfile{assets/mzn/6_basic_complete.mzn} \caption{\label{lst:6-basic-complete} Complete \gls{lns} example} \end{listing} 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 cycles -through a list of \mzninline{N} neighbourhoods \mzninline{nbhs}. To do this, it -uses the decision variable \mzninline{select}. In the initialisation phase -(\mzninline{status()=START}), \mzninline{select} is set to \mzninline{-1}, which -means none of the neighbourhoods is activated. In any following restart, +\Cref{lst:6-round-robin} defines a round-robin \gls{lns} meta-heuristic, which +cycles through a list of \mzninline{N} neighbourhoods \mzninline{nbhs}. To do +this, it uses the decision variable \mzninline{select}. In the initialisation +phase (\mzninline{status()=START}), \mzninline{select} is set to \mzninline{-1}, +which means none of the neighbourhoods is activated. In any following restart, \mzninline{select} is incremented modulo \mzninline{N}, by accessing the last value assigned in a previous restart (\mzninline{last_val(select)}). This will activate a different neighbourhood for each restart (\lref{line:6:roundrobin:post}). -\begin{listing}[t] +\begin{listing} \highlightfile{assets/mzn/6_round_robin.mzn} \caption{\label{lst:6-round-robin} A predicate providing the round robin meta-heuristic} \end{listing} %\paragraph{Adaptive \gls{lns}} -For adaptive \gls{lns}, a simple strategy is to change the size of the neighbourhood -depending on whether the previous size was successful or not. +For adaptive \gls{lns}, a simple strategy is to change the size of the +neighbourhood depending on whether the previous size was successful or not. \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 bounds $[0.6,0.95]$. -\begin{listing}[t] +\begin{listing} \highlightfile{assets/mzn/6_adaptive.mzn} \caption{\label{lst:6-adaptive} A simple adaptive neighbourhood} \end{listing} -\subsection{Meta-heuristics} +\subsection{Optimisation strategies} 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 -is found, the solver adds a constraint to the remainder of the search to only -accept better solutions, as defined by the objective function in the +\minizinc\ solvers to use a branch-and-bound method for optimisation: when a new +solution is found, the solver adds a constraint to the remainder of the search +to only accept better solutions, as defined by the objective function in the \mzninline{minimize} or \mzninline{maximize} clause of the \mzninline{solve} item. When combined with restarts and \gls{lns}, this is equivalent to a simple 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 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). -% + With \mzninline{restart_without_objective}, the restart predicate is now responsible for constraining the objective function. Note that a simple hill-climbing (for minimisation) can still be defined easily in this context as: -{ - \scriptsize - \highlightfile{assets/mzn/6_hill_climbing.mzn} -} +\highlightfile{assets/mzn/6_hill_climbing.mzn} It takes advantage of the fact that the declared objective function is available -through the built-in variable \mzninline{_objective}. -% -A simulated annealing strategy is also easy to -express: +through the built-in variable \mzninline{_objective}. A more interesting example +is a simulated annealing strategy. When using this strategy, the solutions that +the solver finds are no longer required to steadily improve in quality. Instead, +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} -\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} 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 \minisearch\ way, the \minisearch\ runtime implements those built-in functions, computing the correct value whenever a predicate is evaluated. -% + Instead, the compilation scheme presented below uses a limited form of \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 @@ -403,7 +419,7 @@ performs four simple steps: \mzninline{sol}, \mzninline{status}, and \mzninline{last_val} as returning a \mzninline{var} instead of a \mzninline{par} value; and 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. \item Convert any expression containing a call from step 2 to \mzninline{var} 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 definitions, since the built-in functions are often used in positions that accept both parameters and variables. For example, the -\mzninline{uniformNeighbourhood} predicate from \cref{lst:6-lns-minisearch-pred} -uses \mzninline{uniform(0.0,1.0)} in an \mzninline{if} expression, and -\mzninline{sol(x[i])} in an equality constraint. Both expressions can be -translated to \flatzinc\ when the functions return a \mzninline{var}. +\mzninline{uniform_neighbourhood} predicate from +\cref{lst:6-lns-minisearch-pred} uses \mzninline{uniform(0.0, 1.0)} in an +\mzninline{if} expression, and \mzninline{sol(x[i])} in an equality constraint. +Both expressions can be translated to \flatzinc\ when the functions return a +\mzninline{var}. \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 \mzninline{stat} to take the status value. -\begin{listing}[t] +\begin{listing} \highlightfile{assets/mzn/6_status.mzn} \caption{\label{lst:6-status} MiniZinc definition of the \mzninline{status} function} \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, which is the constraint that will be executed by the solver. % -\begin{listing}[t] +\begin{listing} \highlightfile{assets/mzn/6_sol_function.mzn} \caption{\label{lst:6-int-sol} MiniZinc definition of the \mzninline{sol} function for integer variables} @@ -467,7 +484,7 @@ able to generate the most efficient \flatzinc\ code for expressions involving \paragraph{Random number functions} 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 \mzninline{sol}, \mzninline{status}, and \mzninline{last_val}. The MiniZinc 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 as \mzninline{sol}. -\begin{listing}[t] - \highlightfile{assets/mzn/6_uniform_neighbourhood.mzn} +\begin{listing} + \highlightfile{assets/mzn/6_uniform_slv.mzn} \caption{\label{lst:6-int-rnd} MiniZinc definition of the \mzninline{uniform_nbh} function for floats} \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 new \flatzinc\ constraints and, consequently, to execute \gls{lns} definitions @@ -500,10 +517,10 @@ new constraints the solver needs to: \begin{itemize} \item \mzninline{status(s)}: record the status of the previous restart, and 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 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 ever assigned, it has no effect. Note that many solvers (in particular 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. \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}. \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 -block of code (\lrefrange{line:6:x1:start}{line:6:x1:end}) represents the -decomposition of the expression +\mzninline{b1} that is true if-and-only-if the status is not \mzninline{START}. +The second block of code (\lrefrange{line:6:x1:start}{line:6:x1:end}) represents +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} predicate with the \mzninline{if} expression from \mzninline{uniformNeighbourhood}. The code first introduces and constrains a 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 -\mzninline{b3} is constrained to be the conjunction \mzninline{status()!=START - /\ uniform(0.0,1.0)>0.2}. \lref{line:6:x1} constrains \mzninline{x1} to be the -value of \mzninline{x[1]} in the previous solution. Finally, the half-reified -constraint in \lref{line:6:x1:end} implements \mzninline{b3 -> x[1]=sol(x[1])}. +is constrained to be true if-and-only-if the random number is greater than +\(0.2\); while \mzninline{b3} is constrained to be the conjunction of the two. +\lref{line:6:x1} constrains \mzninline{x1} to be the value of \mzninline{x[1]} +in the previous solution. Finally, the half-reified constraint in +\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 \mzninline{x[n]}. Note that the \flatzinc\ shown here has been simplified for presentation. -\begin{listing}[t] +\begin{listing} \highlightfile{assets/mzn/6_basic_complete_transformed.mzn} \caption{\label{lst:6-flat-pred} \flatzinc\ that results from compiling \\ \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. The neighbourhood constraints are effectively switched off. -When the solver restarts, all of the special propagators are re-executed. -Now \mzninline{s} is not 1, and \mzninline{b1} will be set to -\mzninline{true}. The \mzninline{float_random} propagator assigns -\mzninline{rnd1} a new random value and, depending on whether it is greater -than \mzninline{0.2}, the Boolean variables \mzninline{b2}, and consequently -\mzninline{b3} will be assigned. If it is \mzninline{true}, the constraint -in line \lref{line:6:x1:end} will become active and assign \mzninline{x[1]} -to its value in the previous solution. +When the solver restarts, all of the special propagators are re-executed. Now +\mzninline{s} is not 1, and \mzninline{b1} will be set to \mzninline{true}. The +\mzninline{float_random} propagator assigns \mzninline{rnd1} a new random value +and, depending on whether it is greater than \mzninline{0.2}, the Boolean +variables \mzninline{b2}, and consequently \mzninline{b3} will be assigned. If +it is \mzninline{true}, the constraint in line \lref{line:6:x1:end} will become +active and assign \mzninline{x[1]} to its value in the previous solution. 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 -solution has been recorded yet, but we use this simple example to illustrate -how these Boolean conditions are compiled and evaluated. +solution has been recorded yet, but we use this simple example to illustrate how +these Boolean conditions are compiled and evaluated. \section{An Incremental Interface for Constraint Modelling Languages} \label{sec:6-incremental-compilation} In order to support incremental flattening, the \nanozinc\ interpreter must be 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 -calls is straightforward, since \nanozinc\ is already processed call-by-call. +as well as to \emph{remove} calls from an existing \nanozinc\ program. Adding +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 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 period and frees all courses that are assigned to it. -\begin{table}[t] +\begin{table} \centering \input{assets/table/6_gbac} \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}} -\begin{listing}[t] +\begin{listing} \highlightfile{assets/mzn/6_steelmillslab_neighbourhood.mzn} \caption{\label{lst:6-free-bin}\texttt{steelmillslab}: Neighbourhood that frees 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 slab. -\begin{table}[t] +\begin{table} \centering \input{assets/table/6_steelmillslab} \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 \subsubsection{\texttt{rcpsp-wet}} -\begin{listing}[t] +\begin{listing} \highlightfile{assets/mzn/6_rcpsp_neighbourhood.mzn} \caption{\label{lst:6-free-timeslot}\texttt{rcpsp-wet}: Neighbourhood freeing all tasks starting in the drawn interval.} diff --git a/dekker_thesis.tex b/dekker_thesis.tex index fa8ecc0..0eca795 100644 --- a/dekker_thesis.tex +++ b/dekker_thesis.tex @@ -39,11 +39,11 @@ following publication: \end{refsection} \mainmatter{} -\include{chapters/1_introduction} -\include{chapters/2_background} -\include{chapters/3_paradigms} -\include{chapters/4_rewriting} -\include{chapters/5_half_reif} +% \include{chapters/1_introduction} +% \include{chapters/2_background} +% \include{chapters/3_paradigms} +% \include{chapters/4_rewriting} +% \include{chapters/5_half_reif} \include{chapters/6_incremental} \backmatter{}