Global Constraint Catalog: Clex

5.230. lex_greatereq

DESCRIPTION

LINKS

GRAPH

AUTOMATON

Origin

CHIP

Constraint

$𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚 (𝚅𝙴𝙲𝚃𝙾𝚁 1, 𝚅𝙴𝙲𝚃𝙾𝚁 2)$

Synonyms

$𝚕𝚎𝚡𝚎𝚚$ , $𝚕𝚎𝚡_𝚌𝚑𝚊𝚒𝚗$ , $𝚛𝚎𝚕$ , $𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ , $𝚐𝚎𝚚$ , $𝚕𝚎𝚡_𝚐𝚎𝚚$ .

Arguments

$𝚅𝙴𝙲𝚃𝙾𝚁 1$	$𝚌𝚘𝚕𝚕𝚎𝚌𝚝𝚒𝚘𝚗 (𝚟𝚊𝚛 - 𝚍𝚟𝚊𝚛)$
$𝚅𝙴𝙲𝚃𝙾𝚁 2$	$𝚌𝚘𝚕𝚕𝚎𝚌𝚝𝚒𝚘𝚗 (𝚟𝚊𝚛 - 𝚍𝚟𝚊𝚛)$

Restrictions

𝚛𝚎𝚚𝚞𝚒𝚛𝚎𝚍

(𝚅𝙴𝙲𝚃𝙾𝚁 1, 𝚟𝚊𝚛)

𝚛𝚎𝚚𝚞𝚒𝚛𝚎𝚍

(𝚅𝙴𝙲𝚃𝙾𝚁 2, 𝚟𝚊𝚛)

| 𝚅𝙴𝙲𝚃𝙾𝚁 1 | = | 𝚅𝙴𝙲𝚃𝙾𝚁 2 |

Purpose

$𝚅𝙴𝙲𝚃𝙾𝚁 1$ is lexicographically greater than or equal to $𝚅𝙴𝙲𝚃𝙾𝚁 2$ . Given two vectors, $\vec{X}$ and $\vec{Y}$ of $n$ components, $〈 X_{0}, \dots, X_{n - 1} 〉$ and $〈 Y_{0}, \dots, Y_{n - 1} 〉$ , $\vec{X}$ is lexicographically greater than or equal to $\vec{Y}$ if and only if $n = 0$ or $X_{0} > Y_{0}$ or $X_{0} = Y_{0}$ and $〈 X_{1}, \dots, X_{n - 1} 〉$ is lexicographically greater than or equal to $〈 Y_{1}, \dots, Y_{n - 1} 〉$ .

Example

(〈5, 2, 8, 9〉, 〈5, 2, 6, 2〉)

(〈5, 2, 3, 9〉, 〈5, 2, 3, 9〉)

The $𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ constraints associated with the first and second examples hold since:

Within the first example $𝚅𝙴𝙲𝚃𝙾𝚁 1 = 〈 5, 2, 8, 9 〉$ is lexicographically greater than or equal to $𝚅𝙴𝙲𝚃𝙾𝚁 2 = 〈 5, 2, 6, 2 〉$ .
Within the second example $𝚅𝙴𝙲𝚃𝙾𝚁 1 = 〈 5, 2, 3, 9 〉$ is lexicographically greater than or equal to $𝚅𝙴𝙲𝚃𝙾𝚁 2 = 〈 5, 2, 3, 9 〉$ .

Typical

| 𝚅𝙴𝙲𝚃𝙾𝚁 1 | > 1

⋁ (\begin{matrix} | 𝚅𝙴𝙲𝚃𝙾𝚁 1 | < 5, \\ 𝚗𝚟𝚊𝚕 ([𝚅𝙴𝙲𝚃𝙾𝚁 1 . 𝚟𝚊𝚛, 𝚅𝙴𝙲𝚃𝙾𝚁 2 . 𝚟𝚊𝚛]) < 2 * | 𝚅𝙴𝙲𝚃𝙾𝚁 1 | \end{matrix})

⋁ (\begin{matrix} 𝚖𝚊𝚡𝚟𝚊𝚕 ([𝚅𝙴𝙲𝚃𝙾𝚁 1 . 𝚟𝚊𝚛, 𝚅𝙴𝙲𝚃𝙾𝚁 2 . 𝚟𝚊𝚛]) \leq 1, \\ 2 * | 𝚅𝙴𝙲𝚃𝙾𝚁 1 | - 𝚖𝚊𝚡_𝚗𝚟𝚊𝚕𝚞𝚎 ([𝚅𝙴𝙲𝚃𝙾𝚁 1 . 𝚟𝚊𝚛, 𝚅𝙴𝙲𝚃𝙾𝚁 2 . 𝚟𝚊𝚛]) > 2 \end{matrix})

Symmetries

$𝚅𝙴𝙲𝚃𝙾𝚁 1 . 𝚟𝚊𝚛$ can be increased.
$𝚅𝙴𝙲𝚃𝙾𝚁 2 . 𝚟𝚊𝚛$ can be decreased.

Arg. properties

Suffix-contractible wrt. $𝚅𝙴𝙲𝚃𝙾𝚁 1$ and $𝚅𝙴𝙲𝚃𝙾𝚁 2$ (remove items from same position).

Remark

A multiset ordering constraint and its corresponding filtering algorithm are described in [FriHniKizMigWal03].

Algorithm

The first filtering algorithm maintaining arc-consistency for this constraint was presented in [FrischHnichKiziltanMiguelWalsh02]. A second filtering algorithm maintaining arc-consistency and detecting entailment in a more eager way, was given in [BeldiceanuCarlsson02b]. This second algorithm was derived from a deterministic finite automata. A third filtering algorithm extending the algorithm presented in [FrischHnichKiziltanMiguelWalsh02] detecting entailment is given in the PhD thesis of Z. Kızıltan [Kiziltan04]. The previous thesis [Kiziltan04] presents also a filtering algorithm handling the fact that a given variable has more than one occurrence. Finally, T. Frühwirth shows how to encode lexicographic ordering constraints within the context of CHR [Fruhwirth98] in [Fruhwirth06].

Reformulation

The following reformulations in term of arithmetic and/or logical expressions exist for enforcing the lexicographically greater than or equal to constraint. The first one converts $\vec{X}$ and $\vec{Y}$ into numbers and post an inequality constraint. It assumes all components of $\vec{X}$ and $\vec{Y}$ to be within $[0, a - 1]$ :

$a^{n - 1} Y_{0} + a^{n - 2} Y_{1} + \dots + a^{0} Y_{n - 1} \leq a^{n - 1} X_{0} + a^{n - 2} X_{1} + \dots + a^{0} X_{n - 1}$

Since the previous reformulation can only be used with small values of $n$ and $a$ , W. Harvey came up with the following alternative model that maintains arc-consistency:

$(Y_{0} < X_{0} + (Y_{1} < X_{1} + (\dots + (Y_{n - 1} < X_{n - 1} + 1) \dots))) = 1$

Finally, the lexicographically greater than or equal to constraint can be expressed as a conjunction or a disjunction of constraints:

$\begin{matrix} Y_{0} \leq X_{0} & \land \\ (Y_{0} = X_{0}) \Rightarrow Y_{1} \leq X_{1} & \land \\ (Y_{0} = X_{0} \land Y_{1} = X_{1}) \Rightarrow Y_{2} \leq X_{2} & \land \\ ⋮ \\ (Y_{0} = X_{0} \land Y_{1} = X_{1} \land \dots \land Y_{n - 2} = X_{n - 2}) \Rightarrow Y_{n - 1} \leq X_{n - 1} \\ Y_{0} < X_{0} & \lor \\ Y_{0} = X_{0} \land Y_{1} < X_{1} & \lor \\ Y_{0} = X_{0} \land Y_{1} = X_{1} \land Y_{2} < X_{2} & \lor \\ ⋮ \\ Y_{0} = X_{0} \land Y_{1} = X_{1} \land \dots \land Y_{n - 2} = X_{n - 2} \land Y_{n - 1} \leq X_{n - 1} \end{matrix}$

When used separately, the two previous logical decompositions do not maintain arc-consistency.

Systems

lexEq in Choco, rel in Gecode, lex_greatereq in MiniZinc, lex_chain in SICStus.

implied by: $𝚕𝚎𝚡_𝚎𝚚𝚞𝚊𝚕$ , $𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛$ , $𝚜𝚘𝚛𝚝$ .

implies (if swap arguments): $𝚕𝚎𝚡_𝚕𝚎𝚜𝚜𝚎𝚚$ .

negation: $𝚕𝚎𝚡_𝚕𝚎𝚜𝚜$ .

system of constraints: $𝚕𝚎𝚡_𝚌𝚑𝚊𝚒𝚗_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ .

uses in its reformulation: $𝚕𝚎𝚡_𝚌𝚑𝚊𝚒𝚗_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ .

Keywords

characteristic of a constraint: vector, automaton, automaton without counters, reified automaton constraint, derived collection.

constraint network structure: Berge-acyclic constraint network.

constraint type: order constraint.

filtering: duplicated variables, arc-consistency.

heuristics: heuristics and lexicographical ordering.

symmetry: symmetry, matrix symmetry, lexicographic order, multiset ordering.

Derived Collections

𝚌𝚘𝚕 (\begin{matrix} 𝙳𝙴𝚂𝚃𝙸𝙽𝙰𝚃𝙸𝙾𝙽 - 𝚌𝚘𝚕𝚕𝚎𝚌𝚝𝚒𝚘𝚗 (𝚒𝚗𝚍𝚎𝚡 - 𝚒𝚗𝚝, 𝚡 - 𝚒𝚗𝚝, 𝚢 - 𝚒𝚗𝚝), \\ 𝚒𝚝𝚎𝚖 (𝚒𝚗𝚍𝚎𝚡 - 0, 𝚡 - 0, 𝚢 - 0)] \end{matrix})

𝚌𝚘𝚕 (\begin{matrix} 𝙲𝙾𝙼𝙿𝙾𝙽𝙴𝙽𝚃𝚂 - 𝚌𝚘𝚕𝚕𝚎𝚌𝚝𝚒𝚘𝚗 (𝚒𝚗𝚍𝚎𝚡 - 𝚒𝚗𝚝, 𝚡 - 𝚍𝚟𝚊𝚛, 𝚢 - 𝚍𝚟𝚊𝚛), \\ [\begin{matrix} 𝚒𝚝𝚎𝚖 (\begin{matrix} 𝚒𝚗𝚍𝚎𝚡 - 𝚅𝙴𝙲𝚃𝙾𝚁 1 . 𝚔𝚎𝚢, \\ 𝚡 - 𝚅𝙴𝙲𝚃𝙾𝚁 1 . 𝚟𝚊𝚛, \\ 𝚢 - 𝚅𝙴𝙲𝚃𝙾𝚁 2 . 𝚟𝚊𝚛 \end{matrix}) \end{matrix}] \end{matrix})

Arc input(s)

$𝙲𝙾𝙼𝙿𝙾𝙽𝙴𝙽𝚃𝚂$ $𝙳𝙴𝚂𝚃𝙸𝙽𝙰𝚃𝙸𝙾𝙽$

Arc generator

𝑃𝑅𝑂𝐷𝑈𝐶𝑇

(

𝑃𝐴𝑇𝐻

,

𝑉𝑂𝐼𝐷

) \mapsto 𝚌𝚘𝚕𝚕𝚎𝚌𝚝𝚒𝚘𝚗 (𝚒𝚝𝚎𝚖 1, 𝚒𝚝𝚎𝚖 2)

Arc arity

Arc constraint(s)

⋁ (\begin{matrix} 𝚒𝚝𝚎𝚖 2 . 𝚒𝚗𝚍𝚎𝚡 > 0 \land 𝚒𝚝𝚎𝚖 1 . 𝚡 = 𝚒𝚝𝚎𝚖 1 . 𝚢, \\ ⋀ (\begin{matrix} 𝚒𝚝𝚎𝚖 1 . 𝚒𝚗𝚍𝚎𝚡 < | 𝚅𝙴𝙲𝚃𝙾𝚁 1 |, \\ 𝚒𝚝𝚎𝚖 2 . 𝚒𝚗𝚍𝚎𝚡 = 0, \\ 𝚒𝚝𝚎𝚖 1 . 𝚡 > 𝚒𝚝𝚎𝚖 1 . 𝚢 \end{matrix}), \\ ⋀ (\begin{matrix} 𝚒𝚝𝚎𝚖 1 . 𝚒𝚗𝚍𝚎𝚡 = | 𝚅𝙴𝙲𝚃𝙾𝚁 1 |, \\ 𝚒𝚝𝚎𝚖 2 . 𝚒𝚗𝚍𝚎𝚡 = 0, \\ 𝚒𝚝𝚎𝚖 1 . 𝚡 \geq 𝚒𝚝𝚎𝚖 1 . 𝚢 \end{matrix}) \end{matrix})

Graph property(ies)

𝐏𝐀𝐓𝐇_𝐅𝐑𝐎𝐌_𝐓𝐎

(𝚒𝚗𝚍𝚎𝚡, 1, 0) = 1

Graph model

Parts (A) and (B) of Figure 5.230.1 respectively show the initial and final graph associated with the first example of the Example slot. Since we use the $𝐏𝐀𝐓𝐇_𝐅𝐑𝐎𝐌_𝐓𝐎$ graph property we show on the final graph the following information:

The vertices, which respectively correspond to the start and the end of the required path, are stressed in bold.
The arcs on the required path are also stressed in bold.

Figure 5.230.1. Initial and final graph of the $𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ constraint


(a)	(b)

The vertices of the initial graph are generated in the following way:

We create a vertex $c_{i}$ for each pair of components that both have the same index $i$ .
We create an additional dummy vertex called $d$ .

The arcs of the initial graph are generated in the following way:

We create an arc between $c_{i}$ and $d$ . When $c_{i}$ was generated from the last components of both vectors We associate to this arc the arc constraint ${𝚒𝚝𝚎𝚖}_{1} . x \geq {𝚒𝚝𝚎𝚖}_{2} . y$ ; Otherwise we associate to this arc the arc constraint ${𝚒𝚝𝚎𝚖}_{1} . x > {𝚒𝚝𝚎𝚖}_{2} . y$ ;
We create an arc between $c_{i}$ and $c_{i + 1}$ . We associate to this arc the arc constraint ${𝚒𝚝𝚎𝚖}_{1} . x = {𝚒𝚝𝚎𝚖}_{2} . y$ .

The $𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ constraint holds when there exist a path from $c_{1}$ to $d$ . This path can be interpreted as a maximum sequence of equality constraints on the prefix of both vectors, possibly followed by a greater than constraint.

Signature

Since the maximum value returned by the graph property $𝐏𝐀𝐓𝐇_𝐅𝐑𝐎𝐌_𝐓𝐎$ is equal to 1 we can rewrite $𝐏𝐀𝐓𝐇_𝐅𝐑𝐎𝐌_𝐓𝐎 (𝚒𝚗𝚍𝚎𝚡, 1, 0) = 1$ to $𝐏𝐀𝐓𝐇_𝐅𝐑𝐎𝐌_𝐓𝐎 (𝚒𝚗𝚍𝚎𝚡, 1, 0) \geq 1$ . Therefore we simplify $\underset{̲}{\bar{𝐏𝐀𝐓𝐇_𝐅𝐑𝐎𝐌_𝐓𝐎}}$ to $\bar{𝐏𝐀𝐓𝐇_𝐅𝐑𝐎𝐌_𝐓𝐎}$ .

Automaton: Figure 5.230.2 depicts the automaton associated with the $𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ constraint. Let $𝚅𝙰𝚁 1_{i}$ and $𝚅𝙰𝚁 2_{i}$ respectively be the $𝚟𝚊𝚛$ attributes of the $i^{t h}$ items of the $𝚅𝙴𝙲𝚃𝙾𝚁 1$ and the $𝚅𝙴𝙲𝚃𝙾𝚁 2$ collections. To each pair $(𝚅𝙰𝚁 1_{i}, 𝚅𝙰𝚁 2_{i})$ corresponds a signature variable $S_{i}$ as well as the following signature constraint: $(𝚅𝙰𝚁 1_{i} < 𝚅𝙰𝚁 2_{i} \Leftrightarrow S_{i} = 1) \land (𝚅𝙰𝚁 1_{i} = 𝚅𝙰𝚁 2_{i} \Leftrightarrow S_{i} = 2) \land (𝚅𝙰𝚁 1_{i} > 𝚅𝙰𝚁 2_{i} \Leftrightarrow S_{i} = 3)$ .

Figure 5.230.2. Automaton of the $𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ constraint

Figure 5.230.3. Hypergraph of the reformulation corresponding to the automaton of the $𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ constraint

Global Constraint Catalog

5. Global Constraint Catalogue

5.230. lex_greatereq

Figure 5.230.1. Initial and final graph of the $𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ constraint

Figure 5.230.2. Automaton of the $𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ constraint

Figure 5.230.3. Hypergraph of the reformulation corresponding to the automaton of the $𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ constraint

Global Constraint Catalog

5. Global Constraint Catalogue

5.230. lex_greatereq

Figure 5.230.1. Initial and final graph of the 𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚 constraint

Figure 5.230.2. Automaton of the 𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚 constraint

Figure 5.230.3. Hypergraph of the reformulation corresponding to the automaton of the 𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚 constraint

Figure 5.230.1. Initial and final graph of the $𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ constraint

Figure 5.230.2. Automaton of the $𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ constraint

Figure 5.230.3. Hypergraph of the reformulation corresponding to the automaton of the $𝚕𝚎𝚡_𝚐𝚛𝚎𝚊𝚝𝚎𝚛𝚎𝚚$ constraint