Implement state-of-the-art MIP models for lexicographic order

[dourouc05]

Looks like only one inequality is enough to encode a lexicographic inequality, for binary variables at least.

10.1007@s10013-016-0220-0.pdf

[dourouc05]

Other improvements, for integer variables: orbitope constraints.

https://github.com/MiniZinc/libminizinc/blob/master/share/minizinc/std/fzn_lex_chain_lesseq_orbitope.mzn