- #(?SetExpression, ?Cardinality)
- Cardinality of a set expression
- ?SetVar1 `$ ?SetVar2
- Set disjointness constraint
- ?Element `-@ ?SetVariable
- Set non-membership constraint
- ?SetVar1 `/= ?SetVar2
- Set inequality constraint
- ?SetVariable `:: ?Domain
- Set variable declaration
- ?SetVar1 `< ?SetVar2
- Set inclusion constraint (obsolete)
- ?SetVar1 `<> ?SetVar2
- Set disjointness constraint (obsolete)
- ?SetExp1 `= ?SetExp2
- Set equality constraint
- ?SetVar1 `>= ?SetVar2
- Set inclusion constraint
- ?Element `@ ?SetVariable
- Set membership constraint
- all_disjoint(+SetVars)
- All sets disjointness global constraint
- all_union(+SetVars, ?Union)
- Union constraint of a list of sets
- card_labeling(?SetVars)
- Label cardinality of set variables
- cardinality(?SetVariable, ?Cardinality)
- Cardinality of a set
- complement(?SetVar, ?Complement)
- Set complement constraint
- complement(?SetVar, ++Universe, ?Complement)
- Set complement constraint
- domain(?SetVariable, -Domain)
- Accessing the domain of a set
- domain(?SetVariable, ?Cardinality, ?Domain)
- Accessing the domain of a set
- glb(?SetVariable, -Glb)
- Obtaining a set's glb
- glb_poss(?SetVariable, -Glb, -Poss)
- Obtaining both the glb and the still possible elements of a set
- ?Element in ?SetVariable
- Set membership constraint
- lub(?SetVariable, -Lub)
- Obtaining a set's lub
- lub(?SetVariable, -Glb, -Poss, -Lub)
- Obtaining a set's lub, together with its glb and poss (lub\glb)
- maximum(?SetVariable, ?Max)
- Maximum of a set of integers
- minimum(?SetVariable, ?Min)
- Minimum of a set of integers
- ?Element notin ?SetVariable
- Set non-membership constraint
- poss(?SetVariable, -Poss)
- Obtaining the still possible elements of a set (lub\glb)
- refine(++UpDown, ?SetVar)
- Refine a set variable's domain
- set(?SetVariable, ++Glb, ++Poss, +Functions)
- Set variable declaration with optional functions
- set_labeling(?SetVars)
- Label set variable(s)
- set_labeling(++UpDown, +SetVars)
- Label set variables
- sets(+SetVariables, ++Glb, ++Poss, +Functions)
- Set variables declaration with optional functions
- union_var(?SetVariable, ?UnionVar)
- Union of a set of sets
- struct cardinal(domain, cardinality, minimum, maximum, union, bounded, glb, lub, bound)
- Cardinal attributes of a set variable
- export chtab(96, symbol)
- export op(650, xfx, `=)
- export op(650, xfx, `/=)
- export op(650, xfx, `$)
- export op(650, xfx, `@)
- export op(650, xfx, `-@)
- export op(650, xfx, `::)
- export op(550, xfx, `>=)
- export op(500, yfx, `\/)
- export op(400, yfx, `/\)
- export op(300, yfx, `\)
- export op(650, fx, #)
- export op(650, xfx, `<>)
- export op(650, xfx, in)
- export op(650, xfx, notin)
- export op(650, xfx, `<)
- export op(300, yfx, \)
A set is naturally used to collect distinct elements sharing some property. Combinatorial search problems over these data structures can thus be naturally modelled by high level languages with set abstraction facilities, and efficiently solved if constraint reasoning prunes search space when the sets are not fully known a priori (i.e. they are variables ranging over a set domain).
Many complex relations between sets can be expressed with constraints such as set inclusion, disjointness and equality over set expressions that may include such operators as intersection, union or difference of sets. Also, as it is often the case, one is not interested simply on these relations but on some attribute or function of one or more sets (e.g. the cardinality of a set). For instance, the goal of many problems is to maximise or minimise the cardinality of a set. Even for satisfaction problems, some sets, although still variables, may be constrained to a fixed cardinality or a stricter cardinality domain than just the one inferred by the domain of a set variable (for instance, the cardinality of a set may have to be restricted to be an even number).
Cardinal represents set variables by set intervals with a lower and an upper bound considering set inclusion as a partial ordering. Consistency techniques are then applied to set constraints by interval reasoning. A set domain variable S may be specified by an interval [A,B] where A and B are known sets ordered by set inclusion, representing the greatest lower bound and the lowest upper bound of S, respectively.
The cardinality of a set S, given as a finite domain variable C (#S=C), is not a bijective function since two distinct sets may have the same cardinality. Still, it can be constrained by the cardinalities of the set bounds.
A simple inference that can be done using cardinality information is to instantiate the set to one of the set bounds, when it is known that the set cardinality must be equal to the cardinality of that bound. But Cardinal does much more than that. For instance, consider two set variables S1,S2, that can assume either set value {} (empty set) or {a,b}. Their set domain is thus [{},{a,b}] with cardinality 0 or 2. The intersection of S1 and S2 also yelds set domain [{},{a,b}]. But we need a special inference to conclude that the intersection cardinality is also either 0 or 2 (it can not be 1). Set solvers other than Cardinal do not make such inferences.
Inferences using cardinalities can be very useful to deduce more rapidly the non-satisfiability of a set of constraints, thus improving efficiency of combinatorial search problem solving. As another simple example, if Z is known to be the set difference between Y and X, both contained in set {a,b,c,d}, and it is known that X has exactly 2 elements, it should be inferred that the cardinality of Z can never exceed 2 elements (i.e. from X,Y in {a,b,c,d}, #X=2, Z=Y\X it should be inferred that #Z =< 2). A failure could thus be immediately detected upon the posting of a constraint such as #Z=3.
Inference capabilities such as these are particularly important when solving set problems where cardinality plays a special role. Cardinal thus fully uses constraint propagation on sets cardinality.
Intervals and Lattices
Set intervals define a lattice of sets. The set inclusion relation between two sets defines a partial order on P(U), the powerset over a certain universe U, the set of all subsets of U.
Due to the transitivity rule, the top set, U, includes all sets of P(U); while the bottom set, {}, is included in all sets of P(U). Consequently, sets U and {} constitute an upper bound and a lower bound of P(U), respectively. In addition, they are the least upper bound (lub) or join, and the greatest lower bound (glb) or meet of P(U), since there is no other upper bound contained in (‘less’ than) U nor other lower bound containing (‘greater’ than) the empty set {}.
Let us now consider for U={a,b,c,d}, the sub-lattice connecting {a,b,d} and {b} (thus also including sets {a,b} and {b,d}). Sets {} and {a,b,c,d} are still a lower and an upper bound, but this time the glb is {b} and the lub is {a,b,d}.
The two bounds (glb and lub) define a set interval (e.g. [{b},{a,b,d}]) and may form the domain of a set variable S, meaning that set S is one of those defined by its interval (lattice); all other sets outside this domain are excluded from the solution. Thus, b is definitely an element of S, while a and d are the only other possible elements.
Set interval reasoning allows us to apply consistency techniques such as Bounded Arc Consistency, due to the monotonic property of set inclusion.
Any set variable must then have a domain consisting of a set interval. In addition, this interval should be kept as small as possible, in order to discard all sets that are known not to belong to the solution, while not loosing any of the still possible values (sets). The smallest such domain is the one with equal glb and lub, i.e. a domain of the form [B,B], corresponding to a constant set B. For a set variable that can assume any set value from a collection of known sets, such as {{a,b},{a,c},{d}}, the corresponding interval is the convex closure of such collection (which in this case is the set interval [{},{a,b,c,d}]). In general, for n possible arbitrary sets S1...Sn, the corresponding set variable X has an interval domain [glb, lub] where glb is the intersection of all S1...Sn, and lub is their union.
Implementation Notes
In Cardinal, all sets are represented as sorted lists, which eases working with sets and lists interchangeably.
Set variable bounds are represented by its glb and its lub\glb, the set of additional possible elements, which we refer to as poss.
Cardinal implements a number of set constraints such as inclusion, equality, inequality, membership, disjointness, and even complement, together with set operations (union, intersection and difference), as built-in.
As mentioned, Cardinal also allows the definition and use of optional set functions (other than cardinality): minimum and maximum, for sets of integers, and union, for sets of sets. Refer to the available predicates for details.