Dekker1/on-restart-benchmarks
Archived
1
0
Fork 0
Code

Adjust models to use newest restart library (suing lastval)

Browse Source
This commit is contained in:
Jip J. Dekker 2021-06-16 13:36:28 +10:00
parent 12a32b4a0e
commit 15043f0d55
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
4 changed files with 21 additions and 121 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
gbac/on_restart.mzn
View File

@ -1,5 +1,5 @@
include "gbac.mzn"; include "gbac.mzn";
include "../lib.mzn"; include "restart.mzn";
predicate int_eq_imp(var int: x, var int: y, var bool: b); predicate int_eq_imp(var int: x, var int: y, var bool: b);
predicate bool_eq_imp(var bool: x, var bool: y, var bool: b); predicate bool_eq_imp(var bool: x, var bool: y, var bool: b);
@ -18,12 +18,12 @@ predicate free_period(var bool: b) = let {
array[1..2] of var bool: nbh; array[1..2] of var bool: nbh;
constraint random_allocation(nbh[1]); constraint random_allocation(nbh[1]);
constraint free_period(nbh[2]); constraint free_period(nbh[2]);
var 0..10000000: restart = restart_number(); var 1..2: select;
var 1..2: select = (restart mod 2) + 1; constraint lastval(select) mod 2 + 1 = select;
constraint bool_eq_imp(nbh[1], false, status() == UNKNOWN); constraint bool_eq_imp(nbh[1], false, status() == START);
constraint bool_eq_imp(nbh[2], false, status() == UNKNOWN); constraint bool_eq_imp(nbh[2], false, status() == START);
constraint bool_eq_imp(nbh[1], select == 1, status() != UNKNOWN); constraint bool_eq_imp(nbh[1], select == 1, status() != START);
constraint bool_eq_imp(nbh[2], select == 2, status() != UNKNOWN); constraint bool_eq_imp(nbh[2], select == 2, status() != START);
annotation main_vars(array[int] of var int: vars); annotation main_vars(array[int] of var int: vars);

100
lib.mzn
View File

@ -1,100 +0,0 @@
/***
@groupdef internal Internal Builtins
These annotations and functions provide the basic building blocks to implement
meta-heuristics and governed search with the use of solver internal values and
functionality.
*/
/*
A search annotation that supplies a function to be executed on restart
*/
ann: on_restart(string: pred);
/*
The 'status' function reports the status of the solver (before restarting).
*/
enum STATUS = {UNKNOWN, UNSAT, SAT, OPT};
function var STATUS: status();
function var int: restart_number();
/*
The 'rnd' function provides random values chosen by the solver. The arguments
to the function limit the values to a certain domain.
*/
function var int: uniform_internal(int: i, int: j) ::impure = int_uniform(i, j);
function var int: uniform_internal(set of int: S) ::impure =
if card(S) == max(S) - min(S) + 1 then
int_uniform(min(S),max(S))
else
[ i | i in S ][int_uniform(1,card(S))]
endif;
/*
'int_rnd' is the random intrinsic that needs to be implemented by the solver.
*/
function var int: int_uniform(int: a, int: b) ::impure;
/*
The 'sol' functions provides access to solution values of model variables. The
sol functions are only safe to use when the solver status is not UNKNOWN.
*/
function var bool: sol(var bool: x) =
if is_fixed(x) then
fix(x)
else
bool_sol(x)
endif;
function var float: sol(var float: x) =
if is_fixed(x) then
fix(x)
else
float_sol(x)
endif;
function var int: sol(var int: x) =
if is_fixed(x) then
fix(x)
else
int_sol(x)
endif;
function array[int] of var bool: sol(array[int] of var bool: x) =
[if is_fixed(x[i]) then fix(x[i]) else bool_sol(x[i]) endif | i in index_set(x)];
function array[int] of var float: sol(array[int] of var float: x) =
[if is_fixed(x[i]) then fix(x[i]) else float_sol(x[i]) endif | i in index_set(x)];
function array[int] of var int: sol(array[int] of var int: x) =
[if is_fixed(x[i]) then fix(x[i]) else int_sol(x[i]) endif | i in index_set(x)];
/*
'bool_rnd', 'float_sol', and 'int_sol' are the solution intrinsics that needs
to be implemented by the solver.
*/
function var bool: bool_sol(var bool: a);
function var float: float_sol(var float: a);
function var int: int_sol(var int: a);
/*
'round_robin' provides a metaheuristic for LNS where each neighbourhood is
chosen sequentially.
*/
predicate round_robin(array[int] of var bool: nbhs) =
let {
set of int: N = index_set(nbhs);
% Neighbourhood control variables
array[N] of var bool: control;
% Neighbourhood selection
var N: select;
} in forall(i in N) (control[i] -> nbhs[i]) /\
if status() == UNKNOWN then
control = [false | i in N]
/\ select = max(N)
else
select = (sol(select) + 1) mod card(N)
/\ control = [i == select | i in N]
endif;

14
rcpsp-wet/on_restart.mzn
View File

@ -1,5 +1,5 @@
include "rcpsp-wet.mzn"; include "rcpsp-wet.mzn";
include "../lib.mzn"; include "restart.mzn";
predicate int_eq_imp(var int: x, var int: y, var bool: b); predicate int_eq_imp(var int: x, var int: y, var bool: b);
predicate bool_eq_imp(var bool: x, var bool: y, var bool: b); predicate bool_eq_imp(var bool: x, var bool: y, var bool: b);
@ -21,12 +21,12 @@ predicate free_timeslot(var bool: b) =
array[1..2] of var bool: nbh; array[1..2] of var bool: nbh;
constraint randomize(nbh[1]); constraint randomize(nbh[1]);
constraint free_timeslot(nbh[2]); constraint free_timeslot(nbh[2]);
var 0..10000000: restart = restart_number(); var 1..2: select;
var 1..2: select = (restart mod 2) + 1; constraint lastval(select) mod 2 + 1 = select;
constraint bool_eq_imp(nbh[1], false, status() == UNKNOWN); constraint bool_eq_imp(nbh[1], false, status() == START);
constraint bool_eq_imp(nbh[2], false, status() == UNKNOWN); constraint bool_eq_imp(nbh[2], false, status() == START);
constraint bool_eq_imp(nbh[1], select == 1, status() != UNKNOWN); constraint bool_eq_imp(nbh[1], select == 1, status() != START);
constraint bool_eq_imp(nbh[2], select == 2, status() != UNKNOWN); constraint bool_eq_imp(nbh[2], select == 2, status() != START);
annotation main_vars(array[int] of var int: vars); annotation main_vars(array[int] of var int: vars);

14
steelmillslab/on_restart.mzn
View File

@ -1,5 +1,5 @@
include "steelmillslab.mzn"; include "steelmillslab.mzn";
include "../lib.mzn"; include "restart.mzn";
predicate int_eq_imp(var int: x, var int: y, var bool: b); predicate int_eq_imp(var int: x, var int: y, var bool: b);
predicate bool_eq_imp(var bool: x, var bool: y, var bool: b); predicate bool_eq_imp(var bool: x, var bool: y, var bool: b);
@ -18,12 +18,12 @@ predicate random_bin(var bool: b) = let {
array[1..2] of var bool: nbh; array[1..2] of var bool: nbh;
constraint random_assignment(nbh[1]); constraint random_assignment(nbh[1]);
constraint random_bin(nbh[2]); constraint random_bin(nbh[2]);
var 0..10000000: restart = restart_number(); var 1..2: select;
var 1..2: select = (restart mod 2) + 1; constraint lastval(select) mod 2 + 1 = select;
constraint bool_eq_imp(nbh[1], false, status() == UNKNOWN); constraint bool_eq_imp(nbh[1], false, status() == START);
constraint bool_eq_imp(nbh[2], false, status() == UNKNOWN); constraint bool_eq_imp(nbh[2], false, status() == START);
constraint bool_eq_imp(nbh[1], select == 1, status() != UNKNOWN); constraint bool_eq_imp(nbh[1], select == 1, status() != START);
constraint bool_eq_imp(nbh[2], select == 2, status() != UNKNOWN); constraint bool_eq_imp(nbh[2], select == 2, status() != START);
annotation main_vars(array[int] of var int: vars); annotation main_vars(array[int] of var int: vars);