The finite domain (FD) constraint solver extends Prolog with constraints over FD. This facility is available if the FD part of GNU Prolog has been installed. The solver is an instance of the Constraint Logic Programming scheme introduced by Jaffar and Lassez in 1987 [7]. Constraints on FD are solved using propagation techniques, in particular arc-consistency (AC). The interested reader can refer to “Constraint Satisfaction in Logic Programming” of P. Van Hentenryck (1989) [8]. The solver is based on the clp(FD) solver [4]. The GNU Prolog FD solver offers arithmetic constraints, boolean constraints, reified constraints and symbolic constraints on an new kind of variables: Finite Domain variables.
A new type of data is introduced: FD variables which can only take values in their domains. The initial domain of an FD variable is 0..fd_max_integer where fd_max_integer represents the greatest value that any FD variable can take. The predicate fd_max_integer/1 returns this value which may be different from the max_integer Prolog flag (section 7.22.1). The domain of an FD variable X is reduced step by step by constraints in a monotonic way: when a value has been removed from the domain of X it will never reappear in the domain of X. An FD variable is fully compatible with both Prolog integers and Prolog variables. Namely, when an FD variable is expected by an FD constraint it is possible to pass a Prolog integer (considered as an FD variable whose domain is a singleton) or a Prolog variable (immediately bound to an initial range 0..fd_max_integer). This avoids the need for specific type declaration. Although it is not necessary to declare the initial domain of an FD variable (since it will be bound 0..fd_max_integer when appearing for the fist time in a constraint) it is advantageous to do so and thus reduce as soon as possible the size of its domain: particularly because GNU Prolog, for efficiency reasons, does not check for overflows. For instance, without any preliminary domain definitions for X, Y and Z, the non-linear constraint X*Y#=Z will fail due to an overflow when computing the upper bound of the domain of Z: fd_max_integer × fd_max_integer. This overflow causes a negative result for the upper bound and the constraint then fails.
There are two internal representations for an FD variable:
The initial representation for an FD variable X is always an interval representation and is switched to a sparse representation when a “hole” appears in the domain (e.g. due to an inequality constraint). Once a variable uses a sparse representation it will not switch back to an interval representation even if there are no longer holes in its domain. When this switching occurs some values in the domain of X can be lost since vector_max is less than fd_max_integer. We say that “X is extra-constrained” since X is constrained by the solver to the domain 0..vector_max (via an imaginary constraint X #=< vector_max). An extra_cstr is associated with each FD variable to indicate that values have been lost due to the switch to a sparse representation. This flag is updated on every operations. The domain of an extra-constrained FD variable is output followed by the @ symbol. When a constraint fails on a extra-constrained variable a message Warning: Vector too small - maybe lost solutions (FD Var:N) is displayed (N is the address of the involved variable).
Example 1 (vector_max = 127):
Constraint on X | Domain of X | extra_cstr | Lost values |
X #=< 512 | 0..512 | off | none |
X #\= 10 | 0..9:11..127 | on | 128..512 |
X #=< 100 | 0..9:11..100 | off | none |
In this example, when the constraint X #\= 10 is posted some values are lost, the extra_cstr is then switched on. However, posting the constraint X #=< 100 will turn off the flag (no values are lost).
Example 2:
Constraint on X | Domain of X | extra_cstr | Lost values |
X #=< 512 | 0..512 | off | none |
X #\= 10 | 0..9:11..127 | on | 128..512 |
X #>= 256 | Warning: Vector too small… | on | 128..512 |
In this example, the constraint X #>= 256 fails due to the lost of 128..512 so a message is displayed onto the terminal. The solution would consist in increasing the size of the vector either by setting the environment variable VECTORMAX (e.g. to 512) or using fd_set_vector_max(512).
Finally, bit-vectors are not dynamic, i.e. all vectors have the same size (0..vector_max). So the use of fd_set_vector_max/1 is limited to the initial definition of vector sizes and must occur before any constraint. As seen before, the solver tries to display a message when a failure occurs due to a too short vector_max. Unfortunately, in some cases it cannot detect the lost of values and no message is emitted. So the user should always take care to this parameter to be sure that it is large to encode any vector.