Path: utzoo!attcan!uunet!lll-winken!lll-tis!ames!amdahl!pyramid!prls!philabs!micomvax!zap!iros1!ouareau!tarau
From: tarau@ouareau.iro.umontreal.ca (Paul Tarau)
Newsgroups: comp.lang.prolog
Subject: Minimum Spanning Tree with '=='
Keywords: minimum spanning tree, connected components, logical variable
Message-ID: <544@mannix.iros1.UUCP>
Date: 10 May 88 00:52:49 GMT
References: <12534@tut.cis.ohio-state.edu>
Sender: news@iros1.UUCP
Reply-To: tarau@iros1.UUCP (Paul Tarau)
Organization: Universite de Montreal
Lines: 58
Posted: Mon May  9 20:52:49 1988

The following program finds minimum spanning trees
in O(E) "Prolog time", (E = number of edges).
The program uses the impure '==' operation to deal with 
connected components.

% MinSpanTree is a minimum spanning tree of an undirected graph
% represented by its list of Edges of the form: "edge(Cost,From,To)"
% with From<To, sorted by cost (in ascending order),
% and having as vertices natural numbers in 1..NbOfVertices.

mst(NbOfVertices,Edges,MinSpanTree):- 
	% makes an array of connected components
	functor(Components,'$',NbOfVertices), 
	mst(NbOfVertices,Components,Edges,MinSpanTree).

mst(1,_,_,[]):-!.		% no more vertices left
mst(N,Cs,[edge(Cost,V1,V2)|Es],T):-
	N>1,
	arg(V1,Cs,C1),		% C1,C2 are the components of V1,V2
	arg(V2,Cs,C2),
	(	C1==C2->	% Both endpoints are already in the same
		T1=T,		% connected component - skip the edge
		N1 is N 	
	;	C1=C2,		% Put endpoints in the same component
		T=[edge(Cost,V1,V2)|T1],	% Take the edge
		N1 is N-1			% Count a new vertex
	),
	mst(N1,Cs,Es,T1).

test(MinSpanTree):-
  mst(
      % Number of vertices
        5,
      % sorted list of edges (by cost)
        [
	  edge(10,1,2),edge(20,4,5),edge(30,1,4),
	  edge(40,2,5),edge(50,3,5),edge(60,2,3),
	  edge(70,1,3),edge(80,3,4),edge(90,1,5)
	],
	MinSpanTree
      ).

If sorting by cost is not provided, it may take O(E*log(E)).
If the number of vertices is not provided it takes O(E) to
find it as the biggest vertex on the list of edges.
Unification may have chains of variables representing connected
components to follow, but that is C or machine-language time...

The point is is that the '==' hack seems very useful, and
this kind of algorithm works fine on many related problems.
In this example logical variables seem to work basically
as equivalence classes, and unification means replacing
two of them by their union. With this interpretation, the
program is sound, but I do not know at this time how to
to force '==' inherit this kind of soundness in the general case.

Does someone have an elegant (meta-)logical semantics for '==' ?

	Paul Tarau