FlatZinc feature request

[glebbelov]

Please add wall time limit -t ms, i.e., in milliseconds, as it is a standard option. Also, -s should ideally output some statistics in standard format (%%%mzn-stat: name=value) about each solution and maybe more often (i.e., at least with every solution when using -a). Especially important are objective, objectiveBound, and nodes/failures.

See the updated docs on develop for these: https://gitlab.com/minizinc/minizinc-doc/blob/develop/en/fzn-spec.rst, in particular the statistics format.

[lperron]

I cannot read the specs for the output

[glebbelov]

The statistics format is here: https://github.com/MiniZinc/minizinc-doc/blob/develop/en/fzn-spec.rst#statistics-output, copying below:

Statistics output FlatZinc solvers can output statistics in a standard format so that it can be read by scripts, for example, in order to run experiments and automatically aggregate the results. Statistics should be printed to the standard output stream in the form of FlatZinc comments that follow a specific format. Statistics can be output at any time during the solving, i.e., before the first solution, between solutions, and after the search has finished.

Each value should be output on a line of its own in the following format:

%%%mzn-stat: = Each block of statistics is terminated by a line of its own with the following format:

%%%mzn-stat-end The :mzndef:<name> describes the kind of statistics gathered, and the :mzndef:<value> can be any value of a MiniZinc type. The following names are considered standard statistics:

Name Type Explanation nodes int Number of search nodes openNodes int Number of open search nodes objective float Current objective value objectiveBound float Dual bound on the objective value failures int Number of leaf nodes that were failed restarts int Number of times the solver restarted the search variables int Number of variables intVariables int Number of integer variables created boolVariables int Number of bool variables created floatVariables int Number of float variables created setVariables int Number of set variables created propagators int Number of propagators created propagations int Number of propagator invocations peakDepth int Peak depth of search tree nogoods int Number of nogoods created backjumps int Number of backjumps peakMem float Peak memory (in Mbytes) initTime float Initialisation time (in seconds) solveTime float Solving time (in seconds)

[lperron]

I like how this specs does not give an actual example of the format :-)

Where do you put the info ? after the solution, before the solution? After the '======' line, before it for the final part ? Do you need a prefix ?

%%%mzn-stat: = objective = 3.5 objectiveBounds = 2.1 %%%mzn-stat-end

Can I give the initTime after the solve ?

Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00

Le ven. 21 juin 2019 à 02:59, glebbelov notifications@github.com a écrit :

The statistics format is here: https://github.com/MiniZinc/minizinc-doc/blob/develop/en/fzn-spec.rst#statistics-output, copying below:

Statistics output FlatZinc solvers can output statistics in a standard format so that it can be read by scripts, for example, in order to run experiments and automatically aggregate the results. Statistics should be printed to the standard output stream in the form of FlatZinc comments that follow a specific format. Statistics can be output at any time during the solving, i.e., before the first solution, between solutions, and after the search has finished.

Each value should be output on a line of its own in the following format:

%%%mzn-stat: = Each block of statistics is terminated by a line of its own with the following format:

%%%mzn-stat-end The :mzndef: describes the kind of statistics gathered, and the :mzndef: can be any value of a MiniZinc type. The following names are considered standard statistics:

Name Type Explanation nodes int Number of search nodes openNodes int Number of open search nodes objective float Current objective value objectiveBound float Dual bound on the objective value failures int Number of leaf nodes that were failed restarts int Number of times the solver restarted the search variables int Number of variables intVariables int Number of integer variables created boolVariables int Number of bool variables created floatVariables int Number of float variables created setVariables int Number of set variables created propagators int Number of propagators created propagations int Number of propagator invocations peakDepth int Peak depth of search tree nogoods int Number of nogoods created backjumps int Number of backjumps peakMem float Peak memory (in Mbytes) initTime float Initialisation time (in seconds) solveTime float Solving time (in seconds)

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/google/or-tools/issues/1367?email_source=notifications&email_token=ACUPL3JLHTDLMHRU4L5CXCLP3QRW7A5CNFSM4HZPR2AKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODYHD6PI#issuecomment-504250173, or mute the thread https://github.com/notifications/unsubscribe-auth/ACUPL3IRUG6FHEGJ4JACTYLP3QRW7ANCNFSM4HZPR2AA .

[glebbelov]

Thank you for the questions.

The info can be before of after every printed solution, but before its '----------' separator. For the final '==========' marker, assuming you run with -a, the last solution's info is printed simultaneously, but after '==========', the final output is needed in any case, see example as added on the docs.

No prefix, the fields can be in any order.

---

Statistics can be output at any time during the solving, i.e., before the first solution, between solutions, and after the search has finished. Statistics output corresponding to a solution should be the last one before its '----------' separator.

...........

Example

%%%mzn-stat objective=1e+308
%%%mzn-stat objectiveBound=0
%%%mzn-stat nodes=0
%%%mzn-stat solveTime=2.3567
%%%mzn-stat-end

(no feasible solution found yet but something can be printed...)

%%%mzn-stat objective=12345
%%%mzn-stat objectiveBound=122
%%%mzn-stat nodes=35
%%%mzn-stat solveTime=78.5799
%%%mzn-stat-end

(the corresponding feasible solution with value 12345 goes here
   or before its statistics but above the separator)
----------               (<- the solution separator)

%%%mzn-stat objective=379
%%%mzn-stat objectiveBound=379
%%%mzn-stat nodes=4725
%%%mzn-stat solveTime=178.5799
%%%mzn-stat-end

(the corr. optimal solution with value 379 goes here)
----------
==========               (<- the 'search complete' marker)

%%%mzn-stat objective=379      (<- this is the concluding output)
%%%mzn-stat objectiveBound=379
%%%mzn-stat nodes=13456
%%%mzn-stat solveTime=2378.5799
%%%mzn-stat-end

[lperron]

Is this correct?

./bin/fz -l -s examples/flatzinc/golomb.fzn

%% File examples/flatzinc/golomb.fzn parsed in 0 ms

%% Presolve model

%% - presolve looped 3 times over the model

%% - rule PresolveInequalities was applied 1 time

%% - rule PresolveIntEq was applied 4 times

%% - rule PresolveLinear was applied 3 times

%% - rule SimplifyBinaryLinear was applied 3 times

%% - done in 0 ms

%% Model golomb

%% - all_different_int: 1

%% - int_lin_eq: 3

%% - int_lt: 3

%% - Minimization problem

%% *** Starting translation to CP-SAT

%% Optimization model 'golomb':

%% Search strategy: on 4 variables, CHOOSE_FIRST, SELECT_MIN_VALUE

%% #Variables: 7 (1 in objective)

%% - 2 in [0,16]

%% - 1 in [1,14]

%% - 1 in [2,15]

%% - 1 in [2,16]

%% - 1 in [3,16]

%% - 1 constants in {0}

%% #kAllDiff: 1

%% #kLinear2: 3

%% #kLinear3: 3

mark = array1d(1..4, [0, 1, 4, 6]);

---

==========

%%%mzn-stat objective=6

%%%mzn-stat objectiveBound=6

%%%mzn-stat boolVariables=3

%%%mzn-stat failures=1

%%%mzn-stat propagations=62

%%%mzn-stat solveTime=0.001892

and with -a

./bin/fz -l -s examples/flatzinc/golomb.fzn -a

%% File examples/flatzinc/golomb.fzn parsed in 1 ms

%% Presolve model

%% - presolve looped 3 times over the model

%% - rule PresolveInequalities was applied 1 time

%% - rule PresolveIntEq was applied 4 times

%% - rule PresolveLinear was applied 3 times

%% - rule SimplifyBinaryLinear was applied 3 times

%% - done in 0 ms

%% Model golomb

%% - all_different_int: 1

%% - int_lin_eq: 3

%% - int_lt: 3

%% - Minimization problem

%% *** Starting translation to CP-SAT

%% Optimization model 'golomb':

%% Search strategy: on 4 variables, CHOOSE_FIRST, SELECT_MIN_VALUE

%% #Variables: 7 (1 in objective)

%% - 2 in [0,16]

%% - 1 in [1,14]

%% - 1 in [2,15]

%% - 1 in [2,16]

%% - 1 in [3,16]

%% - 1 constants in {0}

%% #kAllDiff: 1

%% #kLinear2: 3

%% #kLinear3: 3

mark = array1d(1..4, [0, 1, 3, 7]);

%%%mzn-stat objective=7

%%%mzn-stat objectiveBound=4

%%%mzn-stat boolVariables=3

%%%mzn-stat failures=0

%%%mzn-stat propagations=21

%%%mzn-stat solveTime=0.00168

---

mark = array1d(1..4, [0, 1, 4, 6]);

%%%mzn-stat objective=6

%%%mzn-stat objectiveBound=4

%%%mzn-stat boolVariables=3

%%%mzn-stat failures=0

%%%mzn-stat propagations=46

%%%mzn-stat solveTime=0.001925

---

==========

%%%mzn-stat objective=6

%%%mzn-stat objectiveBound=6

%%%mzn-stat boolVariables=3

%%%mzn-stat failures=1

%%%mzn-stat propagations=62

%%%mzn-stat solveTime=0.002108

Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00

Le ven. 21 juin 2019 à 08:29, glebbelov notifications@github.com a écrit :

Thank you for the questions.

The info can be before of after every printed solution, but before its '----------' separator. For the final '==========' marker, assuming you run with -a, the last solution's info is printed simultaneously, but after '==========', the final output is needed in any case, see example as added on the docs.

No prefix, the fields can be in any order.

Statistics can be output at any time during the solving, i.e., before the first solution, between solutions, and after the search has finished. Statistics output corresponding to a solution should be the last one before its '----------' separator.

...........

Example %%%mzn-stat objective=1e+308 %%%mzn-stat objectiveBound=0 %%%mzn-stat nodes=0 %%%mzn-stat solveTime=2.3567 %%%mzn-stat-end

(no feasible solution found yet but something can be printed...)

%%%mzn-stat objective=12345 %%%mzn-stat objectiveBound=122 %%%mzn-stat nodes=35 %%%mzn-stat solveTime=78.5799 %%%mzn-stat-end

(the corresponding feasible solution with value 12345 goes here or before its statistics but above the separator) ---------- (<- the solution separator)

%%%mzn-stat objective=379 %%%mzn-stat objectiveBound=379 %%%mzn-stat nodes=4725 %%%mzn-stat solveTime=178.5799 %%%mzn-stat-end (the corr. optimal solution with value 379 goes here)

========== (<- the 'search complete' marker)

%%%mzn-stat objective=379 (<- this is the concluding output) %%%mzn-stat objectiveBound=379 %%%mzn-stat nodes=13456 %%%mzn-stat solveTime=2378.5799 %%%mzn-stat-end

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/google/or-tools/issues/1367?email_source=notifications&email_token=ACUPL3N2EKHMDCWZTYXYDILP3RYOBA5CNFSM4HZPR2AKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODYHSAOQ#issuecomment-504307770, or mute the thread https://github.com/notifications/unsubscribe-auth/ACUPL3ONILZ675HJAXU5M7LP3RYOBANCNFSM4HZPR2AA .

[glebbelov]

Yes, except for colons: %%%mzn-stat: name=value, I forgot in the example. Probably no need for boolVariables every time.

[lperron]

I will not write to output code :-)