Search code examples
prologsubsetbacktracking

How does prolog uses backtracking to find solutions?

I have this prolog code that generates subsets.

subset([], []).

subset([E|Tail], [E|NTail]):-
     subset(Tail, NTail).

subset([_|Tail], NTail):-
     subset(Tail, NTail).

The code works but I don't understand how. I have tried to use trace to walk through how it finds it solutions but I simply do not understand.

If someone could walk me through, step by step, how prolog finds it solutions for a simple query such as

subset([1,2,3],X).

that would be most helpful.

Solution

  • Prolog is trying to prove subset([1,2,3],X). is a fact. It does that by trying to see if any of the predicates support this goal.

    Initially it tries subset([], []). - which does not succeed as [1,2,3] cannot unify with [].

    It then tries subset([E|Tail], [E|NTail]):- subset(Tail, NTail).. It can unify with the head so now it tries to prove the tail. It tries to prove subset([2,3], NTail).

    Which leads to proving subset([3], NTail) (different NTail) and then subset([], NTail) (again different NTail). Now it succeeds with subset([], []). - which terminates the depth-first-search and now it progresses back up the call stack building the result for X - which is [1|[2|[3|[]]]] or [1, 2, 3].

    The result is that the goal ?- subset([1,2,3],X). succeeds with [1, 2, 3].

    Now if you ask Prolog to provide a second answer it then looks at the last predicate that succeeded and assumes it failed instead. That was the goal subset([], NTail). There are no predicates that can succeed for that goal, so it goes back one more step. It proved subset([3], NTail) with subset([E|Tail], [E|NTail]):- subset(Tail, NTail). but now it will assume this failed so it moves on and tries subset([_|Tail], NTail):- subset(Tail, NTail). That succeeds, and effectively drops the 3, so it then continues like before to continue proving the goal. It finally results in [1, 2].

    If you ask Prolog for another answer it just continues with this approach, going back and finding the last thing that succeeded and assume it failed and continue on.

    Ultimately you get to this result:

    [1, 2, 3]
[1, 2]
[1, 3]
[1]
[2, 3]
[2]
[3]
[]