Breadth-first search
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).
Tip
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).
Exercise 5.2 #
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
a(Literals,OrigGoal)
where 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 ?-likes(X,Y):
[ 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)) ]
Here, Y1, X2 and Y2 denote new variables introduced by findall/3. It can be clearly seen that for each item a(R,G) on the agenda, R and 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 a(true,Goal), then 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 true/0, findall/3 will generate an empty list of children and search will proceed with the rest of the agenda.
Tip
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!
Exercise 5.4 #
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.