Support for lexicographic constraints

[algebravic]

It would be nice if you had support for lexicographic comparison between two lists of literals, somewhat analogous to the support that you have for cardinality constraints.

[alexeyignatiev]

@algebravic, could you please explain what kind of constraint you need here?

[algebravic]

If a and b are two lists (for now of equal length) of boolean variables, and a <=lex b if and only if the following: either a[0] < b[0] or ((a[0] == b[0]) and a[1:] <= lex b[1:]. Here's a survey of possible implementations: https://digitalcommons.iwu.edu/cgi/viewcontent.cgi?article=1022&context=cs_honproj

This has even more details: https://www.cs.york.ac.uk/aig/constraints/SMT/ElgabouThesis.pdf

They are used all the time in symmetry breaking: https://eprints.soton.ac.uk/263661/1/jpms-sat07.pdf

[alexeyignatiev]

OK, I see what you mean now. It would be indeed nice to have a separate module providing CNF encodings for a list of typical constraints, including this one and some others, e.g. alldifferent.