5.116. elem_from_to

DESCRIPTIONLINKSAUTOMATON
Origin

Derived from πšŽπš•πšŽπš–.

Constraint

πšŽπš•πšŽπš–_πšπš›πš˜πš–_𝚝𝚘(π™Έπšƒπ™΄π™Ό,πšƒπ™°π™±π™»π™΄)

Synonym

πšŽπš•πšŽπš–πšŽπš—πš_πšπš›πš˜πš–_𝚝𝚘.

Arguments
π™Έπšƒπ™΄π™ΌπšŒπš˜πš•πš•πšŽπšŒπšπš’πš˜πš—πšπš›πš˜πš–-πšπšŸπšŠπš›,𝚌𝚜𝚝_πšπš›πš˜πš–-πš’πš—πš,𝚝𝚘-πšπšŸπšŠπš›,𝚌𝚜𝚝_𝚝𝚘-πš’πš—πš,πšŸπšŠπš•πšžπšŽ-πšπšŸπšŠπš›
πšƒπ™°π™±π™»π™΄πšŒπš˜πš•πš•πšŽπšŒπšπš’πš˜πš—(πš’πš—πšπšŽπš‘-πš’πš—πš,πšŸπšŠπš•πšžπšŽ-πšπšŸπšŠπš›)
Restrictions
πš›πšŽπššπšžπš’πš›πšŽπš(π™Έπšƒπ™΄π™Ό,[πšπš›πš˜πš–,𝚌𝚜𝚝_πšπš›πš˜πš–,𝚝𝚘,𝚌𝚜𝚝_𝚝𝚘,πšŸπšŠπš•πšžπšŽ])
π™Έπšƒπ™΄π™Ό.πšπš›πš˜πš–β‰₯1
π™Έπšƒπ™΄π™Ό.πšπš›πš˜πš–β‰€|πšƒπ™°π™±π™»π™΄|
π™Έπšƒπ™΄π™Ό.𝚝𝚘β‰₯1
π™Έπšƒπ™΄π™Ό.πšπš˜β‰€|πšƒπ™°π™±π™»π™΄|
π™Έπšƒπ™΄π™Ό.πšπš›πš˜πš–β‰€π™Έπšƒπ™΄π™Ό.𝚝𝚘
|π™Έπšƒπ™΄π™Ό|=1
πš›πšŽπššπšžπš’πš›πšŽπš(πšƒπ™°π™±π™»π™΄,[πš’πš—πšπšŽπš‘,πšŸπšŠπš•πšžπšŽ])
πšƒπ™°π™±π™»π™΄.πš’πš—πšπšŽπš‘β‰₯1
πšƒπ™°π™±π™»π™΄.πš’πš—πšπšŽπš‘β‰€|πšƒπ™°π™±π™»π™΄|
πš’πš—πšŒπš›πšŽπšŠπšœπš’πš—πš_𝚜𝚎𝚚(πšƒπ™°π™±π™»π™΄,[πš’πš—πšπšŽπš‘])
Purpose

Let π™΅πšπ™Ύπ™Ό, π™²πš‚πšƒ_π™΅πšπ™Ύπ™Ό, πšƒπ™Ύ, π™²πš‚πšƒ_πšƒπ™Ύ, πš…π™°π™»πš„π™΄ respectively denote the attributes π™Έπšƒπ™΄π™Ό[1].πšπš›πš˜πš–, π™Έπšƒπ™΄π™Ό[1].𝚌𝚜𝚝_πšπš›πš˜πš–, π™Έπšƒπ™΄π™Ό[1].𝚝𝚘, π™Έπšƒπ™΄π™Ό[1].𝚌𝚜𝚝_𝚝𝚘, π™Έπšƒπ™΄π™Ό[1].πšŸπšŠπš•πšžπšŽ of the unique item of the π™Έπšƒπ™΄π™Ό collection.

Beside imposing the fact that π™΅πšπ™Ύπ™Όβ‰€πšƒπ™Ύ and that both π™΅πšπ™Ύπ™Ό and πšƒπ™Ύ are assigned a value in [1,|πšƒπ™°π™±π™»π™΄|], the πšŽπš•πšŽπš–_πšπš›πš˜πš–_𝚝𝚘 constraint enforces the following condition: All entries of the πšƒπ™°π™±π™»π™΄ collection from position max(1,π™΅πšπ™Ύπ™Ό+π™²πš‚πšƒ_π™΅πšπ™Ύπ™Ό) to position min(|πšƒπ™°π™±π™»π™΄|,πšƒπ™Ύ+π™²πš‚πšƒ_πšƒπ™Ύ) are equal to πš…π™°π™»πš„π™΄. When max(1,π™΅πšπ™Ύπ™Ό+π™²πš‚πšƒ_π™΅πšπ™Ύπ™Ό) is strictly greater than min(|πšƒπ™°π™±π™»π™΄|,πšƒπ™Ύ+π™²πš‚πšƒ_πšƒπ™Ύ) the constraint holds no matter what value is assigned to πš…π™°π™»πš„π™΄.

Example
πšπš›πš˜πš–-1 𝚌𝚜𝚝_πšπš›πš˜πš–-1 𝚝𝚘-4 𝚌𝚜𝚝_𝚝𝚘--1 πšŸπšŠπš•πšžπšŽ-2,πš’πš—πšπšŽπš‘-1πšŸπšŠπš•πšžπšŽ-6,πš’πš—πšπšŽπš‘-2πšŸπšŠπš•πšžπšŽ-2,πš’πš—πšπšŽπš‘-3πšŸπšŠπš•πšžπšŽ-2,πš’πš—πšπšŽπš‘-4πšŸπšŠπš•πšžπšŽ-9,πš’πš—πšπšŽπš‘-5πšŸπšŠπš•πšžπšŽ-9

The πšŽπš•πšŽπš–_πšπš›πš˜πš–_𝚝𝚘 constraint holds since all entries between position max(1,π™΅πšπ™Ύπ™Ό+π™²πš‚πšƒ_π™΅πšπ™Ύπ™Ό)=max(1,1+1)=2 and position min(|πšƒπ™°π™±π™»π™΄|,πšƒπ™Ύ+π™²πš‚πšƒ_πšƒπ™Ύ)=min(5,4-1)=3 are equal to 2.

Typical
π™Έπšƒπ™΄π™Ό.𝚌𝚜𝚝_πšπš›πš˜πš–β‰₯0
π™Έπšƒπ™΄π™Ό.𝚌𝚜𝚝_πšπš›πš˜πš–β‰€1
π™Έπšƒπ™΄π™Ό.𝚌𝚜𝚝_𝚝𝚘β‰₯-1
π™Έπšƒπ™΄π™Ό.𝚌𝚜𝚝_πšπš˜β‰€1
|πšƒπ™°π™±π™»π™΄|>1
πš›πšŠπš—πšπšŽ(πšƒπ™°π™±π™»π™΄.πšŸπšŠπš•πšžπšŽ)>1
Symmetry

All occurrences of two distinct values in π™Έπšƒπ™΄π™Ό.πšŸπšŠπš•πšžπšŽ or πšƒπ™°π™±π™»π™΄.πšŸπšŠπš•πšžπšŽ can be swapped; all occurrences of a value in π™Έπšƒπ™΄π™Ό.πšŸπšŠπš•πšžπšŽ or πšƒπ™°π™±π™»π™΄.πšŸπšŠπš•πšžπšŽ can be renamed to any unused value.

Usage

Given an array t[1..n] of integers (i.e.,Β an array of integers for which the entries are defined between 1 and n), the πšŽπš•πšŽπš–_πšπš›πš˜πš–_𝚝𝚘 constraint is for instance useful for encoding expressions of the form βˆƒi∈[1,n], βˆ€j∈[i+1,n] | t[i]=0. Note that, when the interval [i+1,n] is empty, the condition βˆ€j∈[i+1,n] | t[i]=0 is satisfied and i is equal to n. This example is encoded by using an πšŽπš•πšŽπš–_πšπš›πš˜πš–_𝚝𝚘 constraint and by respectively setting:

  • π™΅πšπ™Ύπ™Ό to i, where i is a variable that is assigned a value from interval [1,n],

  • π™²πš‚πšƒ_π™΅πšπ™Ύπ™Ό to constant 1,

  • πšƒπ™Ύ to n, the index of the last entry of the array t[1..n],

  • π™²πš‚πšƒ_πšƒπ™Ύ to constant 0,

  • πš…π™°π™»πš„π™΄ to 0, the value we are looking for.

  • πšƒπ™°π™±π™»π™΄ to the array of integers t[1..n].

Finally, note that j is not used at all.

See also

common keyword: πšŽπš•πšŽπš–, πšŽπš•πšŽπš–πšŽπš—πšΒ (array constraint).

Keywords

characteristic of a constraint: automaton, automaton without counters, reified automaton constraint.

constraint type: data constraint.

filtering: arc-consistency.

modelling: array constraint, table, variable indexing, variable subscript.

Automaton

FigureΒ 5.116.1 depicts the automaton associated with the πšŽπš•πšŽπš–_πšπš›πš˜πš–_𝚝𝚘 constraint.

Let us first introduce some notations:

  • Let n denote the number of items of the πšƒπ™°π™±π™»π™΄ collection.

  • Let π™Έπ™½π™³π™΄πš‡ i and πš…π™°π™»πš„π™΄ i respectively be the πš’πš—πšπšŽπš‘ and the πšŸπšŠπš•πšžπšŽ attributes of the i th item of the πšƒπ™°π™±π™»π™΄ collection.

  • Let π™΅πšπ™Ύπ™Ό, π™²πš‚πšƒ_π™΅πšπ™Ύπ™Ό, πšƒπ™Ύ, π™²πš‚πšƒ_πšƒπ™Ύ, πš…π™°π™»πš„π™΄ respectively denote the attributes π™Έπšƒπ™΄π™Ό[1].πšπš›πš˜πš–, π™Έπšƒπ™΄π™Ό[1].𝚌𝚜𝚝_πšπš›πš˜πš–, π™Έπšƒπ™΄π™Ό[1].𝚝𝚘, π™Έπšƒπ™΄π™Ό[1].𝚌𝚜𝚝_𝚝𝚘, π™Έπšƒπ™΄π™Ό[1].πšŸπšŠπš•πšžπšŽ of the unique item of the π™Έπšƒπ™΄π™Ό collection.

  • Let 𝙸𝙽 be a shortcut for condition 1β‰€π™΅πšπ™Ύπ™Ό βˆ§π™΅πšπ™Ύπ™Όβ‰€πšƒπ™Ύ βˆ§πšƒπ™Ύβ‰€n.

  • Let 𝙡 and πšƒ respectively denote the quantities max(1,π™΅πšπ™Ύπ™Ό+π™²πš‚πšƒ_π™΅πšπ™Ύπ™Ό) and min(|πšƒπ™°π™±π™»π™΄|,πšƒπ™Ύ+π™²πš‚πšƒ_πšƒπ™Ύ).

To each septuple (π™΅πšπ™Ύπ™Ό,πšƒπ™Ύ,𝙡,πšƒ,πš…π™°π™»πš„π™΄,π™Έπ™½π™³π™΄πš‡ i ,πš…π™°π™»πš„π™΄ i ) corresponds a signature variable πš‚ i as well as the following signature constraint:

(𝙸𝙽 βˆ§π™΅>πšƒ)⇔ πš‚ i =0 ∧(𝙸𝙽 βˆ§π™΅β‰€πšƒ βˆ§π™΅>π™Έπ™½π™³π™΄πš‡ i )⇔ πš‚ i =1 ∧(𝙸𝙽 βˆ§π™΅β‰€πšƒ βˆ§πšƒ<π™Έπ™½π™³π™΄πš‡ i )⇔ πš‚ i =2 ∧(𝙸𝙽 βˆ§π™΅β‰€πšƒ βˆ§π™΅β‰€π™Έπ™½π™³π™΄πš‡ i βˆ§π™Έπ™½π™³π™΄πš‡ i β‰€πšƒ βˆ§πš…π™°π™»πš„π™΄=πš…π™°π™»πš„π™΄ i )⇔ πš‚ i =3 ∧(𝙸𝙽 βˆ§π™΅β‰€πšƒ βˆ§π™΅β‰€π™Έπ™½π™³π™΄πš‡ i βˆ§π™Έπ™½π™³π™΄πš‡ i β‰€πšƒ βˆ§πš…π™°π™»πš„π™΄β‰ πš…π™°π™»πš„π™΄ i )⇔ πš‚ i =4.

Figure 5.116.1. Automaton of the πšŽπš•πšŽπš–_πšπš›πš˜πš–_𝚝𝚘 constraint
ctrs/elem_from_to1
Figure 5.116.2. Hypergraph of the reformulation corresponding to the automaton of the πšŽπš•πšŽπš–_πšπš›πš˜πš–_𝚝𝚘 constraint
ctrs/elem_from_to2