5.57. clause_or

DESCRIPTIONLINKSAUTOMATON
Origin

Logic

Constraint

πšŒπš•πšŠπšžπšœπšŽ_πš˜πš›(π™Ώπ™Ύπš‚πš…π™°πšπš‚,π™½π™΄π™Άπš…π™°πšπš‚,πš…π™°πš)

Synonym

πšŒπš•πšŠπšžπšœπšŽ.

Arguments
π™Ώπ™Ύπš‚πš…π™°πšπš‚πšŒπš˜πš•πš•πšŽπšŒπšπš’πš˜πš—(πšŸπšŠπš›-πšπšŸπšŠπš›)
π™½π™΄π™Άπš…π™°πšπš‚πšŒπš˜πš•πš•πšŽπšŒπšπš’πš˜πš—(πšŸπšŠπš›-πšπšŸπšŠπš›)
πš…π™°πšπšπšŸπšŠπš›
Restrictions
|π™Ώπ™Ύπš‚πš…π™°πšπš‚|+|π™½π™΄π™Άπš…π™°πšπš‚|>0
πš›πšŽπššπšžπš’πš›πšŽπš(π™Ώπ™Ύπš‚πš…π™°πšπš‚,πšŸπšŠπš›)
π™Ώπ™Ύπš‚πš…π™°πšπš‚.πšŸπšŠπš›β‰₯0
π™Ώπ™Ύπš‚πš…π™°πšπš‚.πšŸπšŠπš›β‰€1
πš›πšŽπššπšžπš’πš›πšŽπš(π™½π™΄π™Άπš…π™°πšπš‚,πšŸπšŠπš›)
π™½π™΄π™Άπš…π™°πšπš‚.πšŸπšŠπš›β‰₯0
π™½π™΄π™Άπš…π™°πšπš‚.πšŸπšŠπš›β‰€1
πš…π™°πšβ‰₯0
πš…π™°πšβ‰€1
Purpose

Given a first collection of 0-1 variables π™Ώπ™Ύπš‚πš…π™°πšπš‚=U 1 ,U 2 ,...,U p , a second collection of 0-1 variables π™½π™΄π™Άπš…π™°πšπš‚=V 1 ,V 2 ,...,V n , and a variable πš…π™°πš, enforce πš…π™°πš=(U 1 ∨U 2 ∨...∨U p )∨(Β¬V 1 ∨¬V 2 ∨...∨¬V n ).

Example
(0,0,0,1)
Typical
|π™Ώπ™Ύπš‚πš…π™°πšπš‚|+|π™½π™΄π™Άπš…π™°πšπš‚|>1
Symmetries
  • Items of π™Ώπ™Ύπš‚πš…π™°πšπš‚ are permutable.

  • Items of π™½π™΄π™Άπš…π™°πšπš‚ are permutable.

Remark

The πšŒπš•πšŠπšžπšœπšŽ_πš˜πš› constraint is called πšŒπš•πšŠπšžπšœπšŽ in Gecode (http://www.gecode.org/).

Systems

reifiedOr in Choco, clause in Choco, clause in Gecode.

See also

common keyword: πšŒπš•πšŠπšžπšœπšŽ_πšŠπš—πš, πš˜πš›Β (Boolean constraint).

Keywords

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

constraint network structure: Berge-acyclic constraint network.

constraint type: Boolean constraint.

filtering: arc-consistency.

modelling: disjunction.

Automaton

FigureΒ 5.57.1 depicts the automaton associated with the πšŒπš•πšŠπšžπšœπšŽ_πš˜πš› constraint:

  • To the argument πš…π™°πš of the πšŒπš•πšŠπšžπšœπšŽ_πš˜πš› constraint corresponds the first signature variable.

  • To each variable of the argument π™Ώπ™Ύπš‚πš…π™°πšπš‚ corresponds a signature variable.

  • Finally, to each variable πš…π™°πš i of the argument π™½π™΄π™Άπš…π™°πšπš‚ corresponds a signature variable that is the negation of πš…π™°πš i .

Figure 5.57.1. Automaton of the πšŒπš•πšŠπšžπšœπšŽ_πš˜πš› constraint (π™Ώπš…π™°πš i and π™½πš…π™°πš i respectively denote variables of π™Ώπ™Ύπš‚πš…π™°πšπš‚ and π™½π™΄π™Άπš…π™°πšπš‚)
ctrs/clause_or1
Figure 5.57.2. Hypergraph of the reformulation corresponding to the automaton of the πšŒπš•πšŠπšžπšœπšŽ_πš˜πš› constraint
ctrs/clause_or2