5.198. lex_greatereq

DESCRIPTIONLINKSGRAPHAUTOMATON
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, X โ†’ and Y โ†’ of n components, โŒฉX 0 ,...,X n-1 โŒช and โŒฉY 0 ,...,Y n-1 โŒช, X โ†’ is lexicographically greater than or equal to Y โ†’ if and only if n=0 or X 0 >Y 0 or X 0 =Y 0 and โŒฉX 1 ,...,X n-1 โŒช is lexicographically greater than or equal to โŒฉY 1 ,...,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โŒช.

Symmetries
  • ๐š…๐™ด๐™ฒ๐šƒ๐™พ๐š1.๐šŸ๐šŠ๐š› can be increased.

  • ๐š…๐™ด๐™ฒ๐šƒ๐™พ๐š2.๐šŸ๐šŠ๐š› can be decreased.

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 X โ†’ and Y โ†’ into numbers and post an inequality constraint. It assumes all components of X โ†’ and Y โ†’ to be within [0,a-1]:

a n-1 Y 0 +a n-2 Y 1 +...+a 0 Y n-1 โ‰คa n-1 X 0 +a n-2 X 1 +...+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 +(...+(Y n-1 <X n-1 +1)...)))=1

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

Y 0 โ‰คX 0 โˆงY 0 =X 0 โ‡’Y 1 โ‰คX 1 โˆงY 0 =X 0 โˆงY 1 =X 1 โ‡’Y 2 โ‰คX 2 โˆงโ‹ฎY 0 =X 0 โˆงY 1 =X 1 โˆง...โˆงY n-2 =X n-2 โ‡’Y n-1 โ‰คX n-1 Y 0 <X 0 โˆจY 0 =X 0 โˆงY 1 <X 1 โˆจY 0 =X 0 โˆงY 1 =X 1 โˆงY 2 <X 2 โˆจโ‹ฎY 0 =X 0 โˆงY 1 =X 1 โˆง...โˆงY n-2 =X n-2 โˆงY n-1 โ‰คX n-1

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

Systems

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

See also

common keyword: ๐šŒ๐š˜๐š—๐š_๐š•๐šŽ๐šก_๐š๐š›๐šŽ๐šŠ๐š๐šŽ๐š›๐šŽ๐šš, ๐š•๐šŽ๐šก_๐š‹๐šŽ๐š๐š ๐šŽ๐šŽ๐š—, ๐š•๐šŽ๐šก_๐šŒ๐š‘๐šŠ๐š’๐š—_๐š•๐šŽ๐šœ๐šœ, ๐š•๐šŽ๐šก_๐šŒ๐š‘๐šŠ๐š’๐š—_๐š•๐šŽ๐šœ๐šœ๐šŽ๐ššย (lexicographic order), ๐š•๐šŽ๐šก_๐š๐š’๐š๐š๐šŽ๐š›๐šŽ๐š—๐šย (vector).

implied by: ๐š•๐šŽ๐šก_๐šŽ๐šš๐šž๐šŠ๐š•, ๐š•๐šŽ๐šก_๐š๐š›๐šŽ๐šŠ๐š๐šŽ๐š›.

implies if swap arguments: ๐š•๐šŽ๐šก_๐š•๐šŽ๐šœ๐šœ๐šŽ๐šš.

negation: ๐š•๐šŽ๐šก_๐š•๐šŽ๐šœ๐šœ.

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
๐šŒ๐š˜๐š•๐™ณ๐™ด๐š‚๐šƒ๐™ธ๐™ฝ๐™ฐ๐šƒ๐™ธ๐™พ๐™ฝ-๐šŒ๐š˜๐š•๐š•๐šŽ๐šŒ๐š๐š’๐š˜๐š—(๐š’๐š—๐š๐šŽ๐šก-๐š’๐š—๐š,๐šก-๐š’๐š—๐š,๐šข-๐š’๐š—๐š),๐š’๐š๐šŽ๐š–(๐š’๐š—๐š๐šŽ๐šก-0,๐šก-0,๐šข-0)]
๐šŒ๐š˜๐š•๐™ฒ๐™พ๐™ผ๐™ฟ๐™พ๐™ฝ๐™ด๐™ฝ๐šƒ๐š‚-๐šŒ๐š˜๐š•๐š•๐šŽ๐šŒ๐š๐š’๐š˜๐š—(๐š’๐š—๐š๐šŽ๐šก-๐š’๐š—๐š,๐šก-๐š๐šŸ๐šŠ๐š›,๐šข-๐š๐šŸ๐šŠ๐š›),๐š’๐š๐šŽ๐š–(๐š’๐š—๐š๐šŽ๐šก-๐š…๐™ด๐™ฒ๐šƒ๐™พ๐š1.๐š”๐šŽ๐šข,๐šก-๐š…๐™ด๐™ฒ๐šƒ๐™พ๐š1.๐šŸ๐šŠ๐š›,๐šข-๐š…๐™ด๐™ฒ๐šƒ๐™พ๐š2.๐šŸ๐šŠ๐š›)
Arc input(s)

๐™ฒ๐™พ๐™ผ๐™ฟ๐™พ๐™ฝ๐™ด๐™ฝ๐šƒ๐š‚ ๐™ณ๐™ด๐š‚๐šƒ๐™ธ๐™ฝ๐™ฐ๐šƒ๐™ธ๐™พ๐™ฝ

Arc generator
๐‘ƒ๐‘…๐‘‚๐ท๐‘ˆ๐ถ๐‘‡(๐‘ƒ๐ด๐‘‡๐ป,๐‘‰๐‘‚๐ผ๐ท)โ†ฆ๐šŒ๐š˜๐š•๐š•๐šŽ๐šŒ๐š๐š’๐š˜๐š—(๐š’๐š๐šŽ๐š–1,๐š’๐š๐šŽ๐š–2)

Arc arity
Arc constraint(s)
โ‹๐š’๐š๐šŽ๐š–2.๐š’๐š—๐š๐šŽ๐šก>0โˆง๐š’๐š๐šŽ๐š–1.๐šก=๐š’๐š๐šŽ๐š–1.๐šข,๐š’๐š๐šŽ๐š–1.๐š’๐š—๐š๐šŽ๐šก<|๐š…๐™ด๐™ฒ๐šƒ๐™พ๐š1|โˆง๐š’๐š๐šŽ๐š–2.๐š’๐š—๐š๐šŽ๐šก=0โˆง๐š’๐š๐šŽ๐š–1.๐šก>๐š’๐š๐šŽ๐š–1.๐šข,๐š’๐š๐šŽ๐š–1.๐š’๐š—๐š๐šŽ๐šก=|๐š…๐™ด๐™ฒ๐šƒ๐™พ๐š1|โˆง๐š’๐š๐šŽ๐š–2.๐š’๐š—๐š๐šŽ๐šก=0โˆง๐š’๐š๐šŽ๐š–1.๐šกโ‰ฅ๐š’๐š๐šŽ๐š–1.๐šข
Graph property(ies)
๐๐€๐“๐‡_๐…๐‘๐Ž๐Œ_๐“๐Ž(๐š’๐š—๐š๐šŽ๐šก,1,0)=1

Graph model

Partsย (A) andย (B) of Figureย 5.198.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.198.1. Initial and final graph of the ๐š•๐šŽ๐šก_๐š๐š›๐šŽ๐šŠ๐š๐šŽ๐š›๐šŽ๐šš constraint
ctrs/lex_greatereqActrs/lex_greatereqB
(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โ‰ฅ๐š’๐š๐šŽ๐š– 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)โ‰ฅ1. Therefore we simplify ๐๐€๐“๐‡_๐…๐‘๐Ž๐Œ_๐“๐Ž ยฏ ฬฒ to ๐๐€๐“๐‡_๐…๐‘๐Ž๐Œ_๐“๐Ž ยฏ.

Automaton

Figureย 5.198.2 depicts the automaton associated with the ๐š•๐šŽ๐šก_๐š๐š›๐šŽ๐šŠ๐š๐šŽ๐š›๐šŽ๐šš constraint. Let ๐š…๐™ฐ๐š1 i and ๐š…๐™ฐ๐š2 i respectively be the ๐šŸ๐šŠ๐š› attributes of the i th items of the ๐š…๐™ด๐™ฒ๐šƒ๐™พ๐š1 and the ๐š…๐™ด๐™ฒ๐šƒ๐™พ๐š2 collections. To each pair (๐š…๐™ฐ๐š1 i ,๐š…๐™ฐ๐š2 i ) corresponds a signature variable ๐š‚ i as well as the following signature constraint: (๐š…๐™ฐ๐š1 i <๐š…๐™ฐ๐š2 i โ‡”๐š‚ i =1) โˆง (๐š…๐™ฐ๐š1 i =๐š…๐™ฐ๐š2 i โ‡”๐š‚ i =2) โˆง (๐š…๐™ฐ๐š1 i >๐š…๐™ฐ๐š2 i โ‡”๐š‚ i =3).

Figure 5.198.2. Automaton of the ๐š•๐šŽ๐šก_๐š๐š›๐šŽ๐šŠ๐š๐šŽ๐š›๐šŽ๐šš constraint
ctrs/lex_greatereq1
Figure 5.198.3. Hypergraph of the reformulation corresponding to the automaton of the ๐š•๐šŽ๐šก_๐š๐š›๐šŽ๐šŠ๐š๐šŽ๐š›๐šŽ๐šš constraint
ctrs/lex_greatereq2