(sec: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: ```Prolog % 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. ```{swish} swish:search_bf --- source-text-start: search_bf-start --- ``` ```` ```{exercise} ex:5.2 ``` +++ 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 {numref}`sec:3.8`: ```Prolog 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: ```Prolog % 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 ```Prolog a(Literals,OrigGoal) ``` where `OrigGoal` is a copy of the original goal. To illustrate this, suppose the following clauses are given: ```Prolog 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)`: ```Prolog [ 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: ```{swish} swish:prove_bf --- source-text-end: prove_bf-end --- ``` 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. ``` ```{exercise} ex:5.3 ``` +++ 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. ```{swish} swish:refute_bf --- source-text-end: refute_bf-end --- ``` For instance, given the following clauses: ```pProlog 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} ex:5.4 ``` +++ 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.