Feature request: syntax for lexicographic and Pareto optimality

[matsc-at-sics-se]

Currently, solve items have the syntax:

<solve-item> ::= "solve" <annotations> "satisfy"
               | "solve" <annotations> "minimize" <expr>
               | "solve" <annotations> "maximize" <expr>

Sometimes, it's useful or desirable to have a lexicographic objective instead of a scalar one. I suggest adding the following syntax for that:

               | "solve" <annotations> "lex_minimize" <variables>
               | "solve" <annotations> "lex_maximize" <variables>

I think that's what you, Guido, had in mind when we were chatting at CP 2023.
It later occurred to me that a very similar syntax suggests itself for Pareto optimization for multiple objectives. I suggest:

               | "solve" <annotations> "pareto_minimize" <variables>
               | "solve" <annotations> "pareto_maximize" <variables>

The idea for the latter items is:

• Without the -a flag: the search runs to completion (or timeout), at which point the collected set of mutually non-dominated solutions are output.
• With the -a flag: each time an intermediate non-dominated solution is found, it is output. Note that such a solution can turn out to be dominated by solutions found later.

It is well known how and not too complicated to implement this functionality in solvers. I thought that having a standardized MiniZinc syntax for it might encourage solver implementers to get it done.

What do you think?

[informarte]

Notice that MiniZinc already has experimental annotations for lexicographic optimization, see https://github.com/MiniZinc/libminizinc/blob/master/share/minizinc/std/experimental.mzn.