Next: CLPFD Desiderata, Previous: CLPFD Intro, Up: lib-clpfd [Contents][Index]
We now introduce some terminology that will be used in this chapter.
Given a tuple T of domain variables, an assignment of T is a tuple of the same size as T where each variable has been replaced by an integer or real number in its domain.
An integer in 0..1 or an integer variable with domain contained in 0..1.
A constraint over a tuple T is bounds-consistent if for all lower and upper bounds of all domains, there is at least one assignment of T in its solution set. Achieving bounds consistency consists in trimming the domains until bounds consistency holds. That is often an NP-complete problem, but it is usually easier to achieve than domain consistency and is a good “second best”. Some constraints over integers maintain bounds consistency. All constraints over reals endeavor to maintain bounds consistency.
A mathematical relation over a tuple of domain variables. The constraint is true for some assignments of the tuple but may be false for others.
A constraint over a tuple T is domain-consistent if for all values of all domains, there is at least one assignment of T in its solution set. Achieving domain consistency consists in removing domain values until bounds consistency holds. That is often an NP-complete problem, but is usually desirable, because it achieves the best reduction of the search space. Some constraints over integers maintain domain consistency. Domain consistency for constaints over reals does not make much sense, because their domains contain infinitely many real numbers.
The set of all variables and their domains in the model.
A variable that is known to the solver. Attached to it is its domain, a subset of the integers or the reals. Attached to it is also a list of the propagators in which the variable occurs. While the domain contains more than one value, the variable remains an attributed Prolog variable. When and if the domain becomes a singleton, the variable gets bound to that single value. If the domain gets wiped out, then this leads to a Prolog failure, i.e., backtracking.
A constraint over a tuple T is entailed if all assignments of T are members of the solution set. The practical effect of entailment is that no more pruning is possible, i.e., the propagator has no more work to do and can be disabled.
Domain store S is an extension of domain store T if each domain in S is a subset of the corresponding domain in T.
An integer or an integer variable.
A Prolog term that is used to denote an integer domain. See Syntax of Range Expressions, IntegerRange.
A domain variable whose value varies over the small integers
(see Glossary). The lower (upper) bound of its domain does not
need to be a small integer; it can be minus (plus) infinity, denoted
by the atom inf (sup). Integer domains do not need to
be intervals; they can consist of multiple, disjoint intervals. An
integer variable may be unified with another integer variable or with
a small integer, equating their values.
Same as CSP.
An integer or real argument.
For an optimization problem, the solver will seek to minimize or maximize the value of an integer variable O (with some variants; see Enumeration Predicates). For that to work, the model should contain constraints that constrain O accordingly.
If during the computation an integer 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.
A function that is not defined for all combinations of input values.
The act of adding a constraint to the model, i.e., of calling the constraint as a Prolog goal.
Triggered by the posting of a constraint or the pruning of a domain, propagation is a phase of execution where propagators trigger each other in a “chain reaction” to fixpoint. This fixpoint is a domain store in which no propagator can do any pruning.
The procedural aspect of a constraint: a coroutine that endeavors to remove such domain values that cannot be part of a satisfying assignment. The coroutine is run when the constraint is posted or is resumed. Resumption is triggered when some domain has been pruned by another propagator or by search. Also, a propagator is responsible for detecting entailment or failure, at the very latest when all domain variables have been assigned. Note that a constraint as described in this chapter does not necessarily correspond to a single propagator; it can be implemented by a combination of propagators; sometimes, it has multiple, alternative implementations depending on option choices or the chosen level of consistency. For a propagator P and domain store S, we sometimes use the notation P(S) to denote the domain store that exists after running P.
The act of removing values from a domain. If the whole domain is wiped out as a result, that leads to backtracking, i.e., to a Prolog failure.
A real or a real variable.
A Prolog term that is used to denote a real domain. See Syntax of Range Expressions, RealRange.
A domain variable whose value varies over the real numbers.
Real domains are always intervals.
The lower bound of its domain is a float or the atom finf, denoting minus infinity.
The upper bound of its domain is a float or the atom fsup, denoting plus infinity.
An real variable may be unified with another real variable or with a float,
equating their values.
A constraint C can be reified by a 0..1 variable B,
meaning that B = 1 if C is true and B = 0 if C
is false. Procedurally, reification can be though of as a 2-way
channel between C and B: if entailment (failure) is
detected for C, then B is fixed to 1 (0); if B is
fixed to 1, then C is enforced; if B is fixed to 0, then
the negation of C is enforced. Syntactically, a constraint is
reified whenever it occurs in a propositional formula. Although
reification is a general concept, only a few of the solver’s
constraints support it natively.
Given a constraint over a tuple T of domain variables, an assignment of T for which the constraint is true.
At the end of a successful computation, one expects all domains to become singletons, i.e., all domain variables to become assigned. Usually, domains do not become singletons by propagation alone; it takes some amount of search to find an assignment that satisfies all constraints. That is the job of the search procedure, a procedure that explores the search space, i.e., in principle, all possible assignments of the domain variables. The solver exports predicates for that purpose, but their use is not mandatory, custom search procedures can be formulated using other exported predicates that inspect domains.
The solution set of a constraint over a tuple T is the set of its satisfying assignments. Note that if real variables are part of T, the solution set is usually infinite in theory. But the solver cannot represent real numbers exactly; it uses floating-point numbers. Restricting solutions sets to integers and floating-point numbers would lead to loss of solutions, so to prevent that, the solver treats every floating-point number X as a tiny interval of real numbers centered around X.