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:
)option (see below).
labeling/2goal. 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.
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
The following options control the way in which choices are made for the selected variable X:
#=B and X
#\=B, where B is the lower or upper bound of X. This is the default.
#=<M and X
#>M, where M is the midpoint of the domain of X. This strategy is also known as domain splitting.
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
) in its first solution.
Similarly, it must call the auxiliary predicate
) 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
it will be called as
The following options control the order in which the choices are made
for the selected variable X. Not useful with the
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.
time_out/2option (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:
A limit on the discrepancy of the search can be imposed:
Finally, a time limit on the search can be imposed:
time_out(labeling(...),Time,Flag)(see lib-timeout). Furthermore, if combined with the
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).
library('clpfd/examples/tsp.pl') contains an example of
user-defined variable and value choice heuristics.