10.35.4 Enumeration Predicates

As is usually the case with finite domain constraint solvers, this solver is not complete. That is, it does not ensure that the set of posted constraints is satisfiable. One must resort to search (enumeration) to check satisfiability and get particular solutions.

The following predicates provide several variants of search:

indomain(?X)

where X is a domain variable with a bounded domain or an integer. Assigns, in increasing order via backtracking, a feasible value to X.

labeling(:Options, +Variables)

where Variables is a list of domain variables or integers and Options is a list of search options. The domain variables must all have bounded domains. True if an assignment of the variables can be found, which satisfies the posted constraints.

first_bound(+BB0, -BB)

later_bound(+BB0, -BB)

Provides an auxiliary service for the value(Enum) option (see below).

minimize(:Goal,?X)

maximize(:Goal,?X)

Uses a branch-and-bound algorithm with restart to find an assignment that minimizes (maximizes) the domain variable X. Goal should be a Prolog goal that constrains X to become assigned, and could be a labeling/2 goal. The algorithm calls Goal repeatedly with a progressively tighter upper (lower) bound on X until a proof of optimality is obtained, at which time Goal and X are unified with values corresponding to the optimal solution.

The Options argument of labeling/2 controls the order in which variables are selected for assignment (variable choice heuristic), the way in which choices are made for the selected variable (value choice heuristic), and whether all solutions or a single, optimal solution should be found. The options are divided into four groups. One option may be selected per group. Also, the number of assumptions (choices) made during the search can be collected. Finally, a discrepancy limit can be imposed.

The following options control the order in which the next variable is selected for assignment.

leftmost

The leftmost variable is selected. This is the default.

min

The leftmost variable with the smallest lower bound is selected.

max

The leftmost variable with the greatest upper bound is selected.

ff

The first-fail principle is used: the leftmost variable with the smallest domain is selected.

ffc

The most constrained heuristic is used: a variable with the smallest domain is selected, breaking ties by (a) selecting the variable that has the most constraints suspended on it and (b) selecting the leftmost one.

variable(Sel)

Sel is a predicate to select the next variable. Given Vars, the variables that remain to label, it will be called as Sel(Vars,Selected,Rest).

Sel is expected to succeed determinately, unifying Selected and Rest with the selected variable and the remaining list, respectively.

Sel should be a callable term, optionally with a module prefix, and the arguments Vars,Selected,Rest will be appended to it. For example, if Sel is mod:sel(Param), it will be called as mod:sel(Param,Vars,Selected,Rest).

The following options control the way in which choices are made for the selected variable X:

step

Makes a binary choice between X #= B and X #\= B, where B is the lower or upper bound of X. This is the default.

enum

Makes a multiple choice for X corresponding to the values in its domain.

bisect

Makes a binary choice between X #=< M and X #> M, where M is the midpoint of the domain of X. This strategy is also known as domain splitting.

value(Enum)

Enum is a predicate that should prune the domain of X, possibly but not necessarily to a singleton. It will be called as Enum(X,Rest,BB0,BB) where Rest is the list of variables that need labeling except X, and BB0 and BB are parameters described below.

Enum is expected to succeed nondeterminately, pruning the domain of X, and to backtrack one or more times, providing alternative prunings. To ensure that branch-and-bound search works correctly, it must call the auxiliary predicate first_bound(BB0,BB) in its first solution. Similarly, it must call the auxiliary predicate later_bound(BB0,BB) in any alternative solution.

Enum should be a callable term, optionally with a module prefix, and the arguments X,Rest,BB0,BB will be appended to it. For example, if Enum is mod:enum(Param), it will be called as mod:enum(Param,X,Rest,BB0,BB).

The following options control the order in which the choices are made for the selected variable X. Not useful with the value(Enum) option:

up

The domain is explored in ascending order. This is the default.

down

The domain is explored in descending order.

The following options control whether all solutions should be enumerated by backtracking or whether a single solution that minimizes (maximizes) X is returned, if one exists.

all

All solutions are enumerated. This is the default.

minimize(X)

maximize(X)

Uses a branch-and-bound algorithm to find an assignment that minimizes (maximizes) the domain variable X. The labeling should constrain X to become assigned for all assignments of Variables. It is useful to combine these option with the time_out/2 option (see below). If these options occur more than once, the last occurrence overrides previous ones.

The following option counts the number of assumptions (choices) made during the search:

assumptions(K)

When a solution is found, K is unified with the number of choices made.

A limit on the discrepancy of the search can be imposed:

discrepancy(D)

On the path leading to the solution there are at most D choicepoints in which a non-leftmost branch was taken.

Finally, a time limit on the search can be imposed:

time_out(Time,Flag)

This is equivalent to a goal time_out(labeling(...),Time,Flag) (see lib-timeout). Furthermore, if combined with the minimize(V) or maximize(V) option, and the time limit is reached, the values of Variables and V will be those of the best solution found.

For example, to enumerate solutions using a static variable ordering, use:

     | ?- constraints(Variables),
          labeling([], Variables).
          %same as [leftmost,step,up,all]

To minimize a cost function using branch-and-bound search, a dynamic variable ordering using the first-fail principle, and domain splitting exploring the upper part of domains first, use:

     | ?- constraints(Variables, Cost),
          labeling([ff,bisect,down,minimize(Cost)], Variables).

The file library('clpfd/examples/tsp.pl') contains an example of user-defined variable and value choice heuristics.