|• Posting Constraints:||Posting Constraints|
|• A Constraint Satisfaction Problem:||A Constraint Satisfaction Problem|
|• Reified Constraints:||Reified Constraints|
The solver contains predicates for checking the consistency and entailment of finite domain constraints, as well as solving for solution values for your problem variables.
In the context of this constraint solver, a finite domain is a subset of small integers, and a finite domain constraint denotes a relation over a tuple of small integers (see Glossary). Hence, only small integers and unbound variables are allowed in finite domain constraints.
All domain variables, i.e. variables that occur as arguments to
finite domain constraints get associated with a finite domain, either
explicitly declared by the program, or implicitly imposed by the
constraint solver. Temporarily, the domain of a variable may actually
be infinite, if it does not have a finite lower or upper bound. If
during the computation a variable receives a new lower or upper bound
that cannot be represented as a small integer, an overflow condition is
issued. This is expressed as silent failure or as a representation
error, subject to the
overflow option of
The set of current domains of all domain variables is called the domain store. Domain store S is an extension of domain store T if each domain in S is a subset of the corresponding domain in T. If some domain is empty, the store is contradictory and execution backtracks; otherwise, it is consistent.
At the end of a successful computation, all domains have usually become singletons, i.e. the domain variables have become assigned. The domains don’t become singletons automatically. Usually, it takes some amount of search to find an assignment that satisfies all constraints. It is the programmer’s responsibility to do so. If some domain variables are left unassigned in a computation, the garbage collector will preserve all constraint data that is attached to them.
Please note: if a term containing domain variables is written,
copied, asserted, gathered as a solution to
friends, or raised as an exception, those domain variables will be
replaced by brand new variables in the copy. To retain the domains and
any attached constraints, you can use
clpfd:full_answer asserted (see ref-lte-cpt and Answer Constraints). API change wrt. release 3.
Every finite domain constraint is implemented by a propagator, or a set of such. Some constraints have alternative propagators with differing properties. All propagators act as coroutines performing incremental constraint solving, removing values from domains, and/or entailment checking. They wake up by changes in the domains of its arguments. A propagator P can be seen as a function on constraint store S: P(S) denotes the extension of S resulting from applying P on S.
Propagators come in two kinds: indexicals, stateless reactive functional rules implemented by a stack machine and running, and global propagators, usually stateful, implemented in C or Prolog, and using algorithms from many fields of computer science. At the heart of the constraint solver is a scheduler for propagators, where indexicals have priority over global propagators.
Certain properties of propagators are desirable:
A correct propagator never removes values that are consistent wrt. its constraint. This property is mandatory.
A checking propagator accepts all ground assignments that satisfies the given constraint, and rejects all ground assignments that violate it. This property is also mandatory.
A contracting propagator never adds any value to any domain. This property is also mandatory.
A propagator P is monotone if, for all domain stores S and T, S is an extension of T implies that P(S) is an extension of P(T). This property is not mandatory but helps understanding and debugging.
A propagator P is idempotent if, for all domain stores S, P(S) equals P(P(S)).
A domain-consistent propagator removes all inconsistent values. This property is not mandatory and only a few propagators have it. The reason is that the complexity of maintaining domain consistency is often prohibitively high.
A bounds-consistent propagator adjusts all inconsistent upper and lower domain bounds. This property is not mandatory, and is implied by domain consistency. This property is more widespread and usually less costly to maintain than domain consistency, but far from all propagators have it.