Warm starts from MiniZinc

[glebbelov]

Hi,

warm start annotations are being added in MiniZinc. I wonder if your flatzinc CP solver can support them and if you wish to extend the annotations. To be used, e.g., in the sunny-cp framework or in iterative approaches. For details, see README_MIP.txt on the develop branch, currently supported only for Gurobi and CPLEX backends.

Example:

array[1..3] of var 0..10: x;
array[1..3] of var 0.0..10.5: xf;
var bool: b;
array[1..3] of var set of 5..9: xs;
constraint b+sum(x)==1;
constraint b+sum(xf)==2.4;
constraint 5==sum( [ card(xs[i]) | i in index_set(xs) ] );
solve
  :: warm_start( [b], [<>] )                         %%% Use <> for missing values
  :: warm_start_array( [
       warm_start( x, [<>,8,4] ),
       warm_start( xf, array1d(-5..-3, [5.6,<>,4.7] ) ),
       warm_start( xs, array1d( -3..-2, [ 6..8, 5..7 ] ) )
     ] )
  :: seq_search( [ int_search(x, first_fail, indomain_min, complete)  ] )
  minimize x[1] + b + xf[2] + card( xs[1] intersect xs[3] );

[lperron]

The Flatzinc CP is under deep maintenance :-) We may look at it for the SAT backend. Thanks Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00 2017-12-06 5:33 GMT+01:00 glebbelov <notifications@github.com>:

…

Hi, warm start annotations are being added in MiniZinc. I wonder if your flatzinc CP solver can support them and if you wish to extend the annotations. To be used, e.g., in the sunny-cp framework or in iterative approaches. For details, see README_MIP.txt on the develop branch, currently supported only for Gurobi and CPLEX backends. Example: array[1..3] of var 0..10: x; array[1..3] of var 0.0..10.5: xf; var bool: b; array[1..3] of var set of 5..9: xs; constraint b+sum(x)==1; constraint b+sum(xf)==2.4; constraint 5==sum( [ card(xs[i]) | i in index_set(xs) ] ); solve :: warm_start( [b], [<>] ) %%% Use <> for missing values :: warm_start_array( [ warm_start( x, [<>,8,4] ), warm_start( xf, array1d(-5..-3, [5.6,<>,4.7] ) ), warm_start( xs, array1d( -3..-2, [ 6..8, 5..7 ] ) ) ] ) :: seq_search( [ int_search(x, first_fail, indomain_min, complete) ] ) minimize x[1] + b + xf[2] + card( xs[1] intersect xs[3] ); — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#539>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AKj17YcbdPPq7fiRCHo7yVrnkwm2lS76ks5s9hkcgaJpZM4Q3W-k> .

[lperron]

I tried to compile the example.
It crashes with minizinc 2.2.1 :-(

[glebbelov]

Cannot reproduce the issue. (This is not to bother you on weekend!) The example flattens well on KUbuntu 16.04, for std, linear, and or-tools-sat libraries (current, 2b1d70a). However fzn-or-tools has two things: the float array xf needs to be removed, but then it fails to parse fzn because :: warm_start( [b], [<>] ) %%% Use <> for missing values has been flattened to empty annotation: :: warm_start([],[])

…

On Fri, 7 Sep 2018 at 18:50, Laurent Perron ***@***.***> wrote: I tried to compile the example. It crashes with minizinc 2.2.1 :-( — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#539 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AQgXZpIEQMFqv8Umb-UvxVj4ms-jFYEMks5uYjNQgaJpZM4Q3W-k> .

-- Dr Gleb Belov Monash University +61 3 9903 1622

[lalithsuresh]

Any plans to support warm_start annotations for the CP-SAT backend? I'd be happy to test this out if there's any early code available for this.

[lperron]

I just need the spec of the flatzinc format, and some tests :-) plus some time. Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00 Le jeu. 21 févr. 2019 à 04:55, Lalith Suresh <notifications@github.com> a écrit :

…

Any plans to support warm_start annotations for the CP-SAT backend? I'd be happy to test this out if there's any early code available for this. — You are receiving this because you were assigned. Reply to this email directly, view it on GitHub <#539 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AKj17Rs2T76JDNm4znmlLwAzvELIcbZ4ks5vPhjOgaJpZM4Q3W-k> .

[glebbelov]

Hi, Flatzinc format is whatever you redefine (or not, then you get what is declared in stdlib.mzn). For example, std/nosets.mzn already redefines warm_start for set variables into something using booleans: annotation warm_start( array[int] of var set of int: x, array[int] of set of int: v ) = warm_start_array( [ let { array[int] of var bool: xb = set2bools(x[i]), set of int: is_var = ub(x[i]) diff lb(x[i]), int: iV = i - min(index_set(x)) + if 0<length(v) then min(index_set(v)) else 0 endif, } in warm_start( [ xb[k] | k in is_var ], if iV in index_set(v) then [ k in v[iV] | k in is_var ] else [] endif ) | i in index_set(x) ] ); %% ignoring v[i] diff ub(x[i]) and lb(x[i]) diff v[i] All you need to do then, similarly as you process search annotations, process the warm_starts. The original declarations for the warm_start annotations are in stdlib.mzn, as well as redefinitions for optional variables, so anything you don't redefine can be passed to FZN. stdlib.mzn also contains the remark that the order of warm_starts, relative to other search annotations, can be important, so they all might need to be put into a seq_search as below. The example I used for testing (currently in README_MIP.txt but to be moved to documentation): array[1..3] of var 0..10: x; array[1..3] of var 0.0..10.5: xf; var bool: b; array[1..3] of var set of 5..9: xs; constraint b+sum(x)==1; constraint b+sum(xf)==2.4; constraint 5==sum( [ card(xs[i]) | i in index_set(xs) ] ); solve :: warm_start_array( [ %%% Can be on the upper level warm_start( x, [<>,8,4] ), %%% Use <> for missing values warm_start( xf, array1d(-5..-3, [5.6,<>,4.7] ) ), warm_start( xs, array1d( -3..-2, [ 6..8, 5..7 ] ) ) ] ) :: seq_search( [ warm_start_array( [ %%% Now included in seq_search to keep order warm_start( x, [<>,5,2] ), %%% Repeated warm_starts allowed but not specified warm_start( xf, array1d(-5..-3, [5.6,<>,4.7] ) ), warm_start( xs, array1d( -3..-2, [ 6..8, 5..7 ] ) ) ] ), warm_start( [b], [true] ), int_search(x, first_fail, indomain_min, complete) ] ) minimize x[1] + b + xf[2] + card( xs[1] intersect xs[3] ); Best regards,

…

On Thu, 21 Feb 2019 at 18:14, Laurent Perron ***@***.***> wrote: I just need the spec of the flatzinc format, and some tests :-) plus some time. Laurent Perron | Operations Research | ***@***.*** | (33) 1 42 68 53 00 Le jeu. 21 févr. 2019 à 04:55, Lalith Suresh ***@***.***> a écrit : > Any plans to support warm_start annotations for the CP-SAT backend? I'd be > happy to test this out if there's any early code available for this. > > — > You are receiving this because you were assigned. > Reply to this email directly, view it on GitHub > <#539 (comment)>, > or mute the thread > < https://github.com/notifications/unsubscribe-auth/AKj17Rs2T76JDNm4znmlLwAzvELIcbZ4ks5vPhjOgaJpZM4Q3W-k > > . > — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#539 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AQgXZn7SGrrxt7yQpG9KHNQw9-nz_mGtks5vPkdOgaJpZM4Q3W-k> .

-- Dr Gleb Belov Monash University +61 3 9903 1622