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)
labeling(
:Options,
+Variables)
first_bound(
+BB0,
-BB)
later_bound(
+BB0,
-BB)
value(
Enum)
option
(see below).
minimize(
:Goal,
?X)
maximize(
:Goal,
?X)
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.
leftmost
min
max
ff
ffc
variable(
Sel)
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
#=
B
and X #\=
B, where B is the lower or upper
bound of X. This is the default.
enum
bisect
#=<
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 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
down
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
minimize(
X)
maximize(
X)
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)
A limit on the discrepancy of the search can be imposed:
discrepancy(
D)
Finally, a time limit on the search can be imposed:
time_out(
Time,
Flag)
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.