5.234. not_all_equal

DESCRIPTIONLINKSGRAPHAUTOMATON
Origin

CHIP

Constraint

πš—πš˜πš_πšŠπš•πš•_πšŽπššπšžπšŠπš•(πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚)

Argument
πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚πšŒπš˜πš•πš•πšŽπšŒπšπš’πš˜πš—(πšŸπšŠπš›-πšπšŸπšŠπš›)
Restrictions
πš›πšŽπššπšžπš’πš›πšŽπš(πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚,πšŸπšŠπš›)
|πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚|>1
Purpose

The variables of the collection πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚ should take more than one single value.

Example
(3,1,3,3,3)

The πš—πš˜πš_πšŠπš•πš•_πšŽπššπšžπšŠπš• constraint holds since the collection 〈3,1,3,3,3βŒͺ involves more than one value (i.e.,Β values 1 and 3).

Symmetries
  • Items of πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚ are permutable.

  • All occurrences of two distinct values of πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚.πšŸπšŠπš› can be swapped; all occurrences of a value of πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚.πšŸπšŠπš› can be renamed to any unused value.

Algorithm

If the intersection of the domains of the variables of the πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚ collection is empty the πš—πš˜πš_πšŠπš•πš•_πšŽπššπšžπšŠπš• constraint is entailed. Otherwise, when only one single variable V remains not fixed, remove the unique value (unique since the constraint is not entailed) taken by the other variables from the domain of V.

Reformulation

The πš—πš˜πš_πšŠπš•πš•_πšŽπššπšžπšŠπš•(πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚) constraint can be expressed as πšŠπšπš•πšŽπšŠπšœπš_πš—πšŸπšŠπš•πšžπšŽ(2,πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚).

See also

generalisation: πš—πšŸπšŠπš•πšžπšŽΒ (introduce a variable for counting the number of distinct values).

implied by: πšŠπš•πš•πšπš’πšπšπšŽπš›πšŽπš—πš.

negation: πšŠπš•πš•_πšŽπššπšžπšŠπš•.

specialisation: πš—πšŽπššΒ (when go down to two variables).

used in reformulation: πšŠπšπš•πšŽπšŠπšœπš_πš—πšŸπšŠπš•πšžπšŽ.

Keywords

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

constraint network structure: sliding cyclic(1) constraint network(1).

constraint type: value constraint.

filtering: arc-consistency.

final graph structure: equivalence.

Arc input(s)

πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚

Arc generator
πΆπΏπΌπ‘„π‘ˆπΈβ†¦πšŒπš˜πš•πš•πšŽπšŒπšπš’πš˜πš—(πšŸπšŠπš›πš’πšŠπš‹πš•πšŽπšœ1,πšŸπšŠπš›πš’πšŠπš‹πš•πšŽπšœ2)

Arc arity
Arc constraint(s)
πšŸπšŠπš›πš’πšŠπš‹πš•πšŽπšœ1.πšŸπšŠπš›=πšŸπšŠπš›πš’πšŠπš‹πš•πšŽπšœ2.πšŸπšŠπš›
Graph property(ies)
𝐍𝐒𝐂𝐂>1

Graph model

PartsΒ (A) andΒ (B) of FigureΒ 5.234.1 respectively show the initial and final graph associated with the Example slot. Since we use the 𝐍𝐒𝐂𝐂 graph property we show the different strongly connected components of the final graph. Each strongly connected component corresponds to a value that is assigned to some variables of the πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚ collection. The πš—πš˜πš_πšŠπš•πš•_πšŽπššπšžπšŠπš• holds since the final graph contains more than one strongly connected component.

Figure 5.234.1. Initial and final graph of the πš—πš˜πš_πšŠπš•πš•_πšŽπššπšžπšŠπš• constraint
ctrs/not_all_equalActrs/not_all_equalB
(a) (b)
Automaton

FigureΒ 5.234.2 depicts the automaton associated with the πš—πš˜πš_πšŠπš•πš•_πšŽπššπšžπšŠπš• constraint. To each pair of consecutive variables (πš…π™°πš i ,πš…π™°πš i+1 ) of the collection πš…π™°πšπ™Έπ™°π™±π™»π™΄πš‚ corresponds a signature variable πš‚ i . The following signature constraint links πš…π™°πš i , πš…π™°πš i+1 and πš‚ i : πš…π™°πš i =πš…π™°πš i+1 β‡”πš‚ i .

Figure 5.234.2. Automaton of the πš—πš˜πš_πšŠπš•πš•_πšŽπššπšžπšŠπš• constraint
ctrs/not_all_equal1
Figure 5.234.3. Hypergraph of the reformulation corresponding to the automaton of the πš—πš˜πš_πšŠπš•πš•_πšŽπššπšžπšŠπš• constraint
ctrs/not_all_equal2