Author(s): Claudio Vaucheret, Manuel Hermenegildo.
Version: 1.10#7 (2006/4/26, 19:22:13 CEST)
Version of last change: 1.7#119 (2001/8/28, 15:39:1 CEST)
This package applies a compiling control technique to implement depth first iterative deepening execution [Kor85]. It changes the usual depth-first computation rule by iterative-deepening on those predicates specifically marked. This is very useful in search problems when a complete proof procedure is needed.
When this computation rule is used, first all goals are expanded only up to a given depth. If no solution is found or more solutions are needed by backtracking, the depth limit is incremented and the whole goal is repeated. Although it might seem that this approach is very inefficient because all higher levels are repeated for the deeper ones, it has been shown that is performs only about b/(b - 1) times as many operations than the corresponding breadth-first search, (where b is the branching factor of the proof tree) while the waste of memory is the same as depth first.
The usage is by means of the following directive:
:- iterative(Name, FirstCut, Formula).
which states than the predicate 'Name' given in functor/arity form will be executed using iterative deepening rule starting at the depth 'FirstCut' with depth being incremented by the predicate 'Formula'. This predicate compute the new depth using the previous one. It must implement a dilating function i.e. the new depth must be greater. For example, to start with depth 5 and increment by 10 you can write:
:- iterative(p/1,5,f).
f(X,Y) :- Y is X + 10.
or if you prefer,
:- iterative(p/1,5,(_(X,Y):- Y is X + 10)).
You can also use a fourth parameter to set a limiting depth. All goals below the given depth limit simply fail. Thus, with the following directive:
:- iterative(p/1,5,(_(X,Y):- Y is X + 10),100).
all goals deeper than 100 will fail.
An example of code using this package would be:
:- module(example_id, _,[id]).
test(id) :-
idchain(a,d).
test(df) :-
chain(a,d). % loops!
:- iterative(idchain/2, 3, ( _(X,Z) :- Z is X + 1) ).
idchain(X,X).
idchain(X,Y) :-
arc(X,Z),
idchain(Z,Y).
chain(X,X).
chain(X,Y) :-
arc(X,Z),
chain(Z,Y).
arc(a,b).
arc(a,d).
arc(b,c).
arc(c,a).
The order of solutions are first the shallower and then the deeper. Solutions which are between two cutoff are given in the usual left to right order. For example,
% OLD EXAMPLE - Won't work!
:- module(_, _, [det_hook]).
:- use_module(engine(internals)).
pr(I, X, Y) :-
display(open(I)), nl,
'$metachoice'(C),
det_try(pr2(X, Y, C), (display(close_done(I)), nl), (display(close_abort(I)), nl)).
pr2(X, _, _) :- X =< 0, !, fail.
pr2(2, 2, C) :- '$metacut'(C).
pr2(X, Y, C) :- (X = Y ; X1 is X - 1, pr2(X1, Y, C)).
test1 :-
pr(x, 4, X), pr(y, 4, Y), display(X), display(Y), nl, X = 1, Y = 3, !.
It is possible to preserve the iterative-deepening behavior for calls to predicates defined in other modules. These modules should obviously also use this package. In addition all predicates from such modules should imported, i.e., the directive :- use_module(module), should be used in this case instead of :- use_module(module,[...]). Otherwise calls to predicates outside the module will be treated in the usual way i.e. by depth-first computation.
Another complete proof procedure implemented is the
bf package (
breadth first execution).
id):- use_package(id).
or
:- module(...,...,[id]).
Go to the first, previous, next, last section, table of contents.