4.2.2.2. Lexicographic constraints

In this section: lex2, lex2_strict, lex_chain, lex_chain_greater, lex_chain_greatereq, lex_chain_greatereq_orbitope, lex_chain_less, lex_chain_lesseq, lex_chain_lesseq_orbitope, lex_greater, lex_greatereq, lex_less, lex_lesseq, seq_precede_chain, strict_lex2, value_precede, value_precede_chain, var_perm_sym, var_sqr_sym.

lex2

predicate lex2(array [$$E,$$F] of var $$T: xs)

Require adjacent rows and adjacent columns in the array xs to be lexicographically ordered. Adjacent rows and adjacent columns may be equal.

lex2_strict

predicate lex2_strict(array [$$E,$$F] of var $$T: xs)

Require adjacent rows and adjacent columns in the array xs to be lexicographically ordered. Adjacent rows and adjacent columns cannot be equal.

lex_chain

predicate lex_chain(array [$$E,$$F] of var bool: xs)
predicate lex_chain(array [$$E,$$F] of var $$T: xs)

Requires that the columns of matrix xs are lexicographically sorted, non-decreasing.

lex_chain_greater

predicate lex_chain_greater(array [$$E,$$F] of var bool: xs)
predicate lex_chain_greater(array [$$E,$$F] of var $$T: xs)

Requires that the columns of matrix xs are lexicographically sorted, strictly decreasing.

lex_chain_greatereq

predicate lex_chain_greatereq(array [$$E,$$F] of var bool: xs)
predicate lex_chain_greatereq(array [$$E,$$F] of var $$T: xs)

Requires that the columns of matrix xs are lexicographically sorted, non-increasing.

lex_chain_greatereq_orbitope

predicate lex_chain_greatereq_orbitope(array [$$E,$$F] of var int: xs,
                                       int: _kind)

Requires that the columns of binary matrix xs are lexicographically sorted, non-increasing. Moreover, the second parameter _kind has the following meaning: 0: no further constraints, 1: set-partitioning orbitope, 2: set-packing orbitope

lex_chain_less

predicate lex_chain_less(array [$$E,$$F] of var bool: xs)
predicate lex_chain_less(array [$$E,$$F] of var $$T: xs)

Requires that the columns of matrix xs are lexicographically sorted, strictly increasing.

lex_chain_lesseq

predicate lex_chain_lesseq(array [$$E,$$F] of var bool: xs)
predicate lex_chain_lesseq(array [$$E,$$F] of var $$T: xs)

Requires that the columns of matrix xs are lexicographically sorted, non-decreasing.

lex_chain_lesseq_orbitope

predicate lex_chain_lesseq_orbitope(array [$$E,$$F] of var int: xs,
                                    int: _kind)

Requires that the columns of binary matrix xs are lexicographically sorted, non-decreasing. Moreover, the second parameter _kind has the following meaning: 0: no further constraints, 1: set-partitioning orbitope, 2: set-packing orbitope

lex_greater

predicate lex_greater(array [$$E] of var bool: xs,
                      array [$$F] of var bool: ys)
predicate lex_greater(array [$$E] of var $$T: xs,
                      array [$$F] of var $$T: ys)
predicate lex_greater(array [$$E] of var float: xs,
                      array [$$F] of var float: ys)
predicate lex_greater(array [$$E] of var set of $$T: xs,
                      array [$$F] of var set of $$T: ys)

Requires that the array xs is strictly lexicographically greater than array ys. Compares them from first to last element, regardless of indices.

lex_greatereq

predicate lex_greatereq(array [$$E] of var bool: xs,
                        array [$$F] of var bool: ys)
predicate lex_greatereq(array [$$E] of var $$T: xs,
                        array [$$F] of var $$T: ys)
predicate lex_greatereq(array [$$E] of var float: xs,
                        array [$$F] of var float: ys)
predicate lex_greatereq(array [$$E] of var set of $$T: xs,
                        array [$$F] of var set of $$T: ys)

Requires that the array xs is lexicographically greater than or equal to array ys. Compares them from first to last element, regardless of indices.

lex_less

predicate lex_less(array [$$E] of var bool: xs,
                   array [$$F] of var bool: ys)
predicate lex_less(array [$$E] of var $$T: xs,
                   array [$$F] of var $$T: ys)
predicate lex_less(array [$$E] of var float: xs,
                   array [$$F] of var float: ys)
predicate lex_less(array [$$E] of var set of $$T: xs,
                   array [$$F] of var set of $$T: ys)

Requires that the array xs is strictly lexicographically less than array ys. Compares them from first to last element, regardless of indices.

lex_lesseq

predicate lex_lesseq(array [$$E] of var bool: xs,
                     array [$$F] of var bool: ys)
predicate lex_lesseq(array [$$E] of var float: xs,
                     array [$$F] of var float: ys)
predicate lex_lesseq(array [$$E] of var $$T: xs,
                     array [$$F] of var $$T: ys)
predicate lex_lesseq(array [$$E] of var set of $$T: xs,
                     array [$$F] of var set of $$T: ys)

Requires that the array xs is lexicographically less than or equal to array ys. Compares them from first to last element, regardless of indices.

seq_precede_chain

 predicate seq_precede_chain(array [int] of var int: xs)

 predicate seq_precede_chain(array [int] of var set of int: xs)

Requires that i precedes i+1 in the array xs for all positive i.
Requires that i appears in a set in array xs before i+1 for all positive i

strict_lex2

predicate strict_lex2(array [$$E,$$F] of var $$T: xs)

Requires adjacent rows and adjacent columns in the array xs to be lexicographically ordered. Adjacent rows and adjacent columns cannot be equal.

value_precede

1.  predicate value_precede($$E: before,
                            $$E: after,
                            array [$$X] of var $$E: xs)

2.  predicate value_precede($$E: before,
                            $$E: after,
                            array [$$X] of var opt $$E: xs)

3.  predicate value_precede($$E: before,
                            $$E: after,
                            array [$$X] of var set of $$E: xs)

1, 2.: Requires that before precede after in the array xs.

Precedence means that if any element of xs is equal to after, then another element of xs with a lower index is equal to before.

Requires that before precede after in the array xs.

Precedence means that if an element of xs contains after but not before, then another element of xs with lower index contains before but not after.

value_precede_chain

1.  predicate value_precede_chain(array [$$X] of $$E: order,
                                  array [$$Y] of var $$E: xs)

2.  predicate value_precede_chain(array [$$X] of $$E: order,
                                  array [$$Y] of var opt $$E: xs)

3.  predicate value_precede_chain(array [$$X] of $$E: order,
                                  array [$$Y] of var set of $$E: xs)

1, 2.: Requires that order[i] precedes order[i +1] in the array xs.

Precedence means that if any element of xs is equal to order[i +1], then another element of xs with a lower index is equal to order[i].

Requires that order[i] precedes order[i +1] in the array xs.

Precedence means that if an element of xs contains order[i +1] but not order[i], then another element of xs with lower index contains order[i] but not order[i +1].

var_perm_sym

predicate var_perm_sym(array [$$X] of var $$Y: xs,
                       array [$$Z,$$X] of $$X: permutations)

Requires that the array xs is lex least under the given list of permutations permutations

var_sqr_sym

predicate var_sqr_sym(array [$$X,$$X] of var $$Y: xs)

Requires that the square array xs is lex least under the 7 symmetries: 3 rotations and 4 reflections