5.69. clause_and

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

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

Arg. properties
  • Extensible wrt. π™Ώπ™Ύπš‚πš…π™°πšπš‚ when πš…π™°πš=0.

  • Extensible wrt. π™½π™΄π™Άπš…π™°πšπš‚ when πš…π™°πš=0.

Remark

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

Systems

reifiedAnd 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.

Automaton

FigureΒ 5.69.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.69.1. Automaton of the πšŒπš•πšŠπšžπšœπšŽ_πšŠπš—πš constraint (π™Ώπš…π™°πš i and π™½πš…π™°πš i respectively denote variables of π™Ώπ™Ύπš‚πš…π™°πšπš‚ and π™½π™΄π™Άπš…π™°πšπš‚)
ctrs/clause_and-1-tikz
Figure 5.69.2. Hypergraph of the reformulation corresponding to the automaton of the πšŒπš•πšŠπšžπšœπšŽ_πšŠπš—πš constraint (πš…π™°πš 1 ,β‹―,πš…π™°πš n denotes π™Ώπš…π™°πš 1 ,β‹―,π™Ώπš…π™°πš |π™Ώπ™Ύπš‚πš…π™°πšπš‚| ,1-π™½πš…π™°πš 1 ,β‹―,1-π™½πš…π™°πš |π™½π™΄π™Άπš…π™°πšπš‚| )
ctrs/clause_and-2-tikz