## A.7 clpfd.pl -- Constraint Logic Programming over Finite Domains

author
  Markus Triska

Constraint programming is a declarative formalism that lets you describe conditions a solution should satisfy. This library provides CLP(FD), Constraint Logic Programming over Finite Domains. It can be used to model and solve various combinatorial problems such as planning, scheduling and allocation tasks.

Most predicates of this library are finite domain constraints, which are relations over integers. They generalise arithmetic evaluation of integer expressions in that propagation can proceed in all directions. This library also provides enumeration predicates, which let you systematically search for solutions on variables whose domains have become finite. A finite domain expression is one of:

> an integer | Given value
> a variable | Unknown value
> -Expr | Unary minus
> Expr + Expr | Addition
> Expr * Expr | Multiplication
> Expr - Expr | Subtraction
> min(Expr,Expr) | Minimum of two expressions
> max(Expr,Expr) | Maximum of two expressions
> Expr mod Expr | Remainder of integer division
> abs(Expr) | Absolute value
> Expr / Expr | Integer division

The most important finite domain constraints are:

> Expr1 `#>=` Expr2 | Expr1 is larger than or equal to Expr2
> Expr1 `#=<` Expr2 | Expr1 is smaller than or equal to Expr2
> Expr1 `#=` Expr2 | Expr1 equals Expr2
> Expr1 `#\=` Expr2 | Expr1 is not equal to Expr2
> Expr1 `#>` Expr2 | Expr1 is strictly larger than Expr2
> Expr1 `#<` Expr2 | Expr1 is strictly smaller than Expr2

The constraints #=/2, #\=/2, #</2, #>/2, #=</2, and #>=/2 can be reified, which means reflecting their truth values into Boolean values represented by the integers 0 and 1. Let P and Q denote reifiable constraints or Boolean variables, then:

> `#\` Q | True iff Q is false
> P `#\/` Q | True iff either P or Q
> P `#/\` Q | True iff both P and Q
> P `#<==>` Q | True iff P and Q are equivalent
> P `#==>` Q | True iff P implies Q
> P `#<==` Q | True iff Q implies P

As an example, consider the cryptoarithmetic puzzle SEND + MORE = MONEY, where different letters denote distinct integers between 0 and 9. It can be modeled in CLP(FD) as follows:

    :- use_module(library(clpfd)).

    puzzle([S,E,N,D] + [M,O,R,E] = [M,O,N,E,Y]) :-
            Vars = [S,E,N,D,M,O,R,Y],
            Vars ins 0..9,
            all_different(Vars),
                      S*1000 + E*100 + N*10 + D +
                      M*1000 + O*100 + R*10 + E #=
            M*10000 + O*1000 + N*100 + E*10 + Y,
            M #> 0, S #> 0.

Sample query and its result:

    ?- puzzle(As+Bs=Cs).
    As = [9, _G5402{4..7}, _G5405{5..8}, _G5408{2..8}],
    Bs = [1, 0, _G5417{2..8}, _G5402{4..7}],
    Cs = [1, 0, _G5405{5..8}, _G5402{4..7}, _G5435{2..8}].

Here, the constraint solver could deduce more stringent bounds for many variables. Labeling can be used to search for solutions:

    ?- puzzle(As+Bs=Cs), label(As), label(Bs).
    As = [9, 5, 6, 7],
    Bs = [1, 0, 8, 5],
    Cs = [1, 0, 6, 5, 2]

?Var in +Domain
  Constrain Var to elements of Domain. Domain is one of:
  Lower .. Upper
    All integers I such that Lower `=<` I `=<` Upper. The atoms inf and sup denote negative and positive infinity, respectively.
  Domain1 `\/` Domain2
    The union of Domain1 and Domain2.
+Vars ins +Domain
  Constrain the variables in the list Vars to elements of Domain.
indomain(?Var)
  Bind Var to all feasible values of its domain on backtracking. The domain of Var must be finite.
label(+Vars)
  Equivalent to labeling([], Vars).
labeling(+Options, +Vars)
  Labeling means systematically trying out values for the finite domain variables Vars until all of them are ground. The domain of each variable in Vars must be finite. Options is a list of options that let you exhibit some control over the search process. Several categories of options exist:

  The variable selection strategy lets you specify which variable of Vars should be labeled next and is one of:

  leftmost
    Label the variables in the order they occur in Vars. This is the default.
  ff
    First fail. Label the leftmost variable with smallest domain next, in order to detect infeasibility early. This is often a good strategy.
  ffc
    Of the variables with smallest domains, the leftmost one participating in most constraints is labeled next.
  min
    Label the leftmost variable whose lower bound is the lowest next.
  max
    Label the leftmost variable whose upper bound is the highest next.

  The value order is one of:

  up
    Try the elements of the chosen variable's domain in ascending order. This is the default.
  down
    Try the domain elements in descending order.

  The branching strategy is one of:

  step
    For each variable X, a choice is made between X = V and X `#\=` V, where V is determined by the value ordering options. This is the default.
  enum
    For each variable X, a choice is made between X = V_1, X = V_2 etc., for all values V_i of the domain of X. The order is determined by the value ordering options.
  bisect
    For each variable X, a choice is made between X `#=<` M and X `#>` M, where M is the midpoint of the domain of X.

  The order of solutions can be influenced with:

  min(Expr)
  max(Expr)

  This generates solutions in ascending/descending order with respect to the evaluation of the arithmetic expression Expr. Labeling Vars must make Expr ground. To obtain the incomplete behaviour that other systems exhibit with "maximize(Expr)" and "minimize(Expr)", use once/1, e.g.:

      once(labeling([max(Expr)], Vars))

  If more than one option of a category is specified, the one occurring rightmost in the option list takes precedence over all others of that category. Labeling is always complete, always terminates, and yields no redundant solutions.

all_different(+Vars)
  Constrain Vars to be pairwise distinct.
sum(+Vars, +Op, +Expr)
  Constrain the sum of a list. The sum/3 constraint demands that "sumlist(Vars) Op Expr" hold, e.g.:

      sum(List, #=<, 100)

?X #>= ?Y
  X is greater than or equal to Y.
?X #=< ?Y
  X is less than or equal to Y.
?X #= ?Y
  X equals Y.
?X #\= ?Y
  X is not Y.
?X #> ?Y
  X is greater than Y.
?X #< ?Y
  X is less than Y.
#\ +Q
  The reifiable constraint Q does not hold.
?P #<==> ?Q
  P and Q are equivalent.
?P #==> ?Q
  P implies Q.
?P #<== ?Q
  Q implies P.
?P #/\ ?Q
  P and Q hold.
?P #\/ ?Q
  P or Q holds.
lex_chain(+Lists)
  Constrains Lists to be lexicographically non-decreasing.
tuples_in(+Tuples, +Relation)
  Relation is a ground list of lists of integers. The elements of the list Tuples are constrained to be elements of Relation.
all_distinct(+Ls)
  Like all_different/1, with stronger propagation.
serialized(+Starts, +Durations)
  Constrain a set of intervals to a non-overlapping sequence. Starts = [S_1,...,S_n], is a list of variables or integers, Durations = [D_1,...,D_n] is a list of non-negative integers. Constrains Starts and Durations to denote a set of non-overlapping tasks, i.e.: S_i + D_i `=<` S_j or S_j + D_j `=<` S_i for all 1 `=<` i < j `=<` n.
  See also
    Dorndorf et al. 2000, "Constraint Propagation Techniques for the Disjunctive Scheduling Problem"
fd_var(+Var)
  True iff Var is a CLP(FD) variable.
fd_inf(+Var, -Inf)
  Inf is the infimum of the current domain of Var.
fd_sup(+Var, -Sup)
  Sup is the supremum of the current domain of Var.
fd_size(+Var, -Size)
  Size is the number of elements of the current domain of Var, or the atom sup if the domain is unbounded.
fd_dom(+Var, -Dom)
  Dom is the current domain (see in/2) of Var.
[det]copy_term(+Term, -Copy, -Gs)
  Creates a regular term Copy as a copy of Term (without any attributes), and a list Gs of goals that when executed reinstate all attributes onto Copy. The nonterminal attribute_goals/3, as defined in the modules the attributes stem from, is used to convert attributes to lists of goals.