The source code of SWI-Prolog says that the unification deployed is based on some idea from Bart Demoen. The core of the SWI-Prolog unification does detect reoccuring compounds and can therefore handle cyclic terms. But reoccuring compounds are also detected when no cyclic terms are involved.
The later features makes the unification kind of linear in time for acyclic terms. But I am not 100% sure whether Wielemaker-Demoen unification is really linear in time for acyclic terms?
A known algorithm that is linear in time is the Paterson-Wegman unification. It is linear in the input equational system size. A typical example where the Paterson-Wegman unification shines is this example here, where naive unification gets exponential:
X1 = f(X0, X0),
X2 = f(X1, X1),
..
Xn-1 = f(Xn-2, Xn-2),
Xn = f(Xn-1, Xn-1).
Y1 = f(Y0, Y0),
Y2 = f(Y1, Y1),
..
Yn-1 = f(Yn-2, Yn-2),
Yn = f(Yn-1, Yn-1).
Xn = Yn
Here is a test with SWI-Prolog and GNU Prolog using n=4,6,8,10. With SWI-Prolog:
SWI-Prolog (threaded, 64 bits, version 8.3.17)
?- run.
% 200,000 inferences, 0.031 CPU in 0.032 seconds (98% CPU, 6400000 Lips)
% 200,000 inferences, 0.047 CPU in 0.042 seconds (112% CPU, 4266667 Lips)
% 200,000 inferences, 0.063 CPU in 0.055 seconds (114% CPU, 3200000 Lips)
% 200,000 inferences, 0.063 CPU in 0.064 seconds (98% CPU, 3200000 Lips)
true.
With GNU-Prolog:
GNU Prolog 1.4.5
?- run.
% 36 ms
% 74 ms
% 206 ms
% 738 ms
Does SWI-Prolog in essence implement Paterson-Wegman Unification when faced with acyclic terms? Another Prolog system that also fares well in the above example is YAP 6.3.3, but I didn't check their source for some references.
Open source:
Linear or Exponential II?
https://gist.github.com/jburse/279b6280ab4311de456e458a7386c1da#file-paterson-pl
question from:
https://stackoverflow.com/questions/65884340/paterson-wegman-versus-wielemaker-demoen-unification 
