5.3. Breadth-first search¶
Breadth-first search is realised by implementing the agenda as a first in–first out datastructure. That is, while removing nodes from the front of the list, they are added at the end:
% breadth-first search search_bf([Goal|Rest],Goal):- goal(Goal). search_bf([Current|Rest],Goal):- children(Current,Children), append(Rest,Children,NewAgenda), search_bf(NewAgenda,Goal).
Here is breadth-first search applied to the palindrome example.
% nodes are lists of letters arc(T,[H|T]):- length(T,N),N<11, % try removing the depth bound member(H,[a,d,i,m]). % find palindromes goal(L):- reverse(L,L).
Implement the predicate
term_write_bf/1, which writes the tree represented by a term from the root downward (as opposed to the predicate
term_write/1 of Section 4.1, which writes from left to right). Employ breadth-first search with two agendas, one for nodes at depth \(n\) and the other for nodes at depth \(n + 1\).
In breadth-first search, the agenda is implemented as a queue. This means that the nodes on the agenda are ordered according to increasing depth: all the nodes on depth \(n\) occur before the nodes on depth \(n + 1\). This has profound consequences with regard to the properties of breadth-first search. First of all, breadth-first search is complete, even for infinite search spaces. This is so because every goal on depth \(n\) will be found before descending to depth \(n + 1\). Secondly, breadth-first search always finds a shortest solution path. It may seem that breadth-first search is much better than depth-first search. However, like every coin this one has a reverse side also: the number of nodes at depth \(n\) is \(B^n\), such that breadth-first search requires much more memory than depth-first search.
We will now show how to change Prolog into a complete SLD prover, by employing breadth-first search. We start from the meta-interpreter
prove_r/1 given in Section 3.8:
prove_r(true):-!. prove_r((A,B)):-!, clause(A,C), conj_append(C,B,D), prove_r(D). prove_r(A):- clause(A,B), prove_r(B).
As explained in that section, this meta-interpreter operates on the complete resolvent, which is exactly what we need. This predicate is turned into an agenda-based depth-first search procedure as follows:
% agenda-based version of prove_r/1 prove_df(Goal):- prove_df_a([Goal]). prove_df_a([true|Agenda]). prove_df_a([(A,B)|Agenda]):-!, findall(D,(clause(A,C),conj_append(C,B,D)),Children), append(Children,Agenda,NewAgenda), prove_df_a(NewAgenda). prove_df_a([A|Agenda]):- findall(B,clause(A,B),Children), append(Children,Agenda,NewAgenda), prove_df_a(NewAgenda).
The changes are relatively straightforward: all solutions to the calls in the bodies of the second and third
prove_r clauses are collected by means of the predicate
findall/3, and added to the front of the agenda.
In order to search in a breadth-first fashion, we swap the first two arguments of the
append/3 literals. One additional improvement is required, since
prove_df/1 succeeds for every proof that can be found, but it does not return an answer substitution for the variables in the query. This is because the call
findall(X,G,L) creates new variables for the unbound variables in the instantiation of
X before putting it in the list
L. In order to obtain an answer substitution, we should maintain the agenda as a list of pairs
OrigGoal is a copy of the original goal. To illustrate this, suppose the following clauses are given:
likes(peter,Y):-student(Y),friendly(Y). likes(X,Y):-friend(Y,X). student(maria). student(paul). friendly(maria). friend(paul,peter).
Below, the agenda obtained after each breadth-first search iteration is given for the query
[ a((student(Y1),friendly(Y1)), likes(peter,Y1)), a(friend(Y2,X2), likes(X2,Y2)) ] [ a(friend(Y2,X2), likes(X2,Y2)) a(friendly(maria), likes(peter,maria)), a(friendly(paul), likes(peter,paul)) ] [ a(friendly(maria), likes(peter,maria)), a(friendly(paul), likes(peter,paul)), a(true, likes(peter,paul)) ] [ a(friendly(paul), likes(peter,paul)), a(true, likes(peter,paul)), a(true, likes(peter,maria)) ] [ a(true, likes(peter,paul)), a(true, likes(peter,maria)) ]
Y2 denote new variables introduced by
findall/3. It can be clearly seen that for each item
a(R,G) on the agenda,
G share the right variables – thus, whenever the resolvent gets more instantiated during the proof, the corresponding copy of the goal is instantiated correspondingly. In particular, if the empty clause is found on the agenda in the form of a term
Goal will contain the correct answer substitutions.
The final, complete SLD prover looks as follows:
% breadth-first version of prove_r/1 + answer substitution prove_bf(Goal):- prove_bf_a([a(Goal,Goal)],Goal). prove_bf_a([a(true,Goal)|_Agenda],Goal). prove_bf_a([a((A,B),G)|Agenda],Goal):-!, findall(a(D,G), (cl(A,C),conj_append(C,B,D)), Children), append(Agenda,Children,NewAgenda), % breadth-first prove_bf_a(NewAgenda,Goal). prove_bf_a([a(A,G)|Agenda],Goal):- findall(a(B,G),cl(A,B),Children), append(Agenda,Children,NewAgenda), % breadth-first prove_bf_a(NewAgenda,Goal).
Notice that this program is able to find alternative solutions, since it will backtrack from the first clause into the third and, being unable to find a clause for the predicate
findall/3 will generate an empty list of children and search will proceed with the rest of the agenda.
The previous remark was true at the time of writing; however, modern Prolog interpreters will generate a runtime error for calling
clause/2 on built-in predicates such as
true/0. The above program therefore uses the user-defined meta-predicate
cl/2 to define and query the object-level program.
Consider the following program:
brother(peter,paul). brother(adrian,paul). brother(X,Y):-brother(Y,X). brother(X,Y):-brother(X,Z),brother(Z,Y).
Compare and explain the behaviour of
prove_bf/1 and Prolog on the query
?-brother(peter,adrian). Can you re-order the clauses, such that Prolog succeeds?
As a second, related example of a breadth-first search program, we give a program for finding refutation proofs in full clausal logic. Object-level clauses are given by the predicate
cl/1. Note that
true denotes the empty body, while
false denotes the empty head; thus,
false:-true denotes the empty clause.
% refute_bf(Clause) <- Clause is refuted by clauses % defined by cl/1 % (breadth-first search strategy) refute_bf(Clause):- refute_bf_a([a(Clause,Clause)],Clause). refute_bf_a([a((false:-true),Clause)|_Rest],Clause). refute_bf_a([a(A,C)|Rest],Clause):- findall(a(R,C),(cl(Cl),resolve(A,Cl,R)),Children), append(Rest,Children,NewAgenda), % breadth-first refute_bf_a(NewAgenda,Clause). % resolve(C1,C2,R) <- R is the resolvent of C1 and C2. resolve((H1:-B1),(H2:-B2),(ResHead:-ResBody)):- resolve(H1,B2,R1,R2), disj_append(R1,H2,ResHead), conj_append(B1,R2,ResBody). resolve((H1:-B1),(H2:-B2),(ResHead:-ResBody)):- resolve(H2,B1,R2,R1), disj_append(H1,R2,ResHead), conj_append(R1,B2,ResBody). resolve((A;B),C,B,E):- conj_remove_one(A,C,E). resolve((A;B),C,(A;D),E):- resolve(B,C,D,E). resolve(A,C,false,E):- conj_remove_one(A,C,E). %%% disj_append/3, conj_remove_one/3: see Section 10.2 (appendix)
For instance, given the following clauses:
cl((bachelor(X);married(X):-man(X),adult(X))). cl((has_wife(X):-man(X),married(X))). cl((false:-has_wife(paul))). cl((man(paul):-true)). cl((adult(paul):-true)).
and the query
?-refute_bf((false:-bachelor(X))) (refute that no-one is a bachelor), the program answers
X=paul. Note that there are many proofs for this answer!
Extend the meta-interpreter, such that it returns a proof tree (see Section 3.8). In order to ensure correct variable substitutions, each item on the agenda must be extended with a partial proof tree.
As a search program, the above program is complete. As a theorem prover, however, the program is incomplete. This is due to the resolution strategy used, in which every resolvent has at least one given clause as its parent. This strategy is called input resolution; it is refutation complete for definite clauses, but not for indefinite clauses.