10.9.3 Solver Interface

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.

A finite domain is denoted symbolically by a ConstantRange (see Syntax of Indexicals), a special case of which is an interval, written as one of the expressions A..B, A..sup, inf..B, or inf..sup. Here, A and B should be small integers, inf denotes minus infinity, and sup denotes plus infinity. Please note: inf and sup do not denote integers, they only denote the absence of a lower resp. upper bound. Such ConstantRange terms occur in certain contexts, the most common of which is the unary constraint of the form:

| ?- X in 1..5.
X in 1..5

which constrains X to be in the given interval. Note that variables do not have to be “declared” in this way before they are used in constraints. If an unconstrained variable occurs in a constraint, then it will be treated as having the domain inf..sup.

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, then an overflow condition is issued. This is expressed as silent failure or as a representation error, subject to the overflow option of fd_flag/3.

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, then 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 do not 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, then 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 findall/3 and friends, or raised as an exception, then those domain variables will be replaced by brand new variables in the copy. To retain the domains and any attached constraints, you can use copy_term/3 with 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:

Correct

A correct propagator never removes values that are consistent wrt. its constraint. This property is mandatory.

Checking

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.

Contracting

A contracting propagator never adds any value to any domain. This property is also mandatory.

Monotone

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.

Idempotent

A propagator P is idempotent if, for all domain stores S, P(S) equals P(P(S)).

Domain-Consistent

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.

Bounds-Consistent

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.