Prolog 同构图
Prolog isomorphic graphs
正在尝试解决这里的同构图问题。
作业信息：
- 判断2个无向图是否同构
- 没有孤立的顶点。
- 顶点数小于30
图的边作为谓词给出，即
e(1, 2).
f(1, 2).
我正在尝试使用以下方法：
- 对于每对边（即图 1 和 2 中的每条边）
- 尝试绑定2条边的顶点
- 如果无法绑定顶点（即已经存在与其中一个顶点的另一个绑定），则回溯并尝试另一对边。
- 否则添加绑定并继续处理其余图形（即删除每个图形的一条边并再次应用程序）。
除非两个图都为空（意味着所有顶点都从一个图绑定到另一个图），否则程序会重复进行，这意味着成功。
否则程序应该总是失败（即没有其他可用的绑定组合等）
我的代码似乎有效，但仅适用于小图（猜测是因为它尝试了所有对 :)）。
因此，如果有人知道如何优化代码（我相信可以插入几个削减并且 try_bind 可以用更好的方式编写）或者可以提前告诉更好的方法。
P.s。为了检查非同构，我知道我们可以检查不变量等。现在这并不重要。
代码：
%define graph, i.e. graph is a list of edges
graph1(RES):-findall(edge(X,Y), e(X, Y), RES).
graph2(RES):-findall(edge(X,Y), f(X, Y), RES).
%define required predicate
iso:-graph1(G1), graph2(G2), iso_acc(G1, G2, [], _).
%same as above but outputs result
iso_w:-graph1(G1), graph2(G2), iso_acc(G1, G2, [], RES_MAP), write(RES_MAP).
iso_acc([], [], MAP, RES):-append(MAP, [], RES), !.
iso_acc([X|X_Rest], Y_LS, MAP, RES_MAP):-
select(Y, Y_LS, Y_Rest),
bind(X, Y, MAP, UPD_MAP),
iso_acc(X_Rest, Y_Rest, UPD_MAP, RES_MAP).
% if edges bind is successful then in RES or UPD_MAP updated binding map is returned (may return the same map
% if bindings are already defined), otherwise fails
bind([], [], MAP, RES):-append(MAP, [], RES), !.
bind(edge(X1, Y1), edge(X2, Y2), MAP, UPD_MAP):-
try_bind(b(X1, X2), MAP, RES),
try_bind(b(Y1, Y2), RES, UPD_MAP).
bind(edge(X1, Y1), edge(X2, Y2), MAP, UPD_MAP):-
try_bind(b(X1, Y2), MAP, RES),
try_bind(b(Y1, X2), RES, UPD_MAP).
%if an absolute member, we're OK (absolute member means b(X,Y) is already defined
try_bind(b(X, Y), MAP, UPD_MAP):-
member(b(X, Y), MAP),
append(MAP, [], UPD_MAP), !.
%otherwise check that we don't have other binding to X or to Y
try_bind(b(X, Y), MAP, UPD_MAP):-
member(b(X, Z), MAP),
%check if Z != Y
Z=Y,
append(MAP, [], UPD_MAP).
try_bind(b(X, Y), MAP, UPD_MAP):-
member(b(W, Y), MAP),
%check if W == X
W=X,
append(MAP, [], UPD_MAP).
%finally if we not an absolute member and if no other bindings to X and Y we add new binding
try_bind(b(X, Y), MAP, UPD_MAP):-
not(member(b(X, Z), MAP)),
not(member(b(W, Y), MAP)),
append([b(X, Y)], MAP, UPD_MAP).
首先，祝贺您很好地介绍了问题并提出了详尽的解决方案。
在下一段中，我将讨论您的解决方案的实施细节。
不幸的是，我必须说我没有看到这种解决方案的方法可以扩展到更大的尺寸。假设有 10 个边的图。 iso_acc/4 尝试将第一条边分配给第二条边中的任何一条边（10 种可能性），第二条边也绑定到任何一条边（前一条边有 10 种可能性：10*10），...。如果不是运气好的话，那就是 10^10 种可能性，10！考虑到其中大多数的修剪速度更快。
次要评论是：
您可以跳过append(X,[],Y)的用法，所以
bind([],[],MAP,RES) :- append(MAP,[],RES), !.
可以是：
bind([],[],MAP,MAP).
try_bind/3中的第二条和第三条规则似乎没有必要，在上一条中你已经验证了没有b(X,Y)属于MAP。换句话说，member(b(X,Y),MAP) 等价于 member(b(X,Z),MAP), Z=Y.
附录
让我们试试下面的方法。让示例图 e 为：
+----3----+
1 ---2--+ | +---5
+----4----+
和图表f是：
+----3----+
2 ---5--+ | +---1
+----4----+
基本算法可以是：
memb( X-A, [X-B|_] ) :- permutation(A,B).
memb( X, [_|Q] ) :- memb(X, Q).
match( [], _ ).
match( [H|Q], G2 ) :-
memb(H,G2),
match(Q,G2).
graph_equal(G1,G2,MAP) :-
bagof( X, graph_to_list(G1,X), L1 ),
length(MAP,40),
bagof( X, graph_to_list_vars(G2,MAP,X), L2 ), !,
length( L1, S ),
length( L2, S ),
match( L1, L2 ).
从这个出发点，可以进行优化。
此算法需要一些初始数据转换器，以将每个图形转换为 node-[peer1,peer2,...] 形式的项目列表。此转换的规则是：
bidir(G,X,Y) :- ( call(G,X,Y); call(G,Y,X) ).
bidir_vars(G,MAP,VX,VY) :-
bidir(G,X,Y), nth0(X,MAP,VX), nth0(Y,MAP,VY).
graph_to_list( G, N-XL ) :-
setof( X, bidir(G,N,X), XL).
graph_to_list_vars( G, MAP, N-XL ) :-
setof( X, bidir_vars(G,MAP,N,X), XL).
附录 2
这个例子的初始数据是：
e(1,2).
e(2,3).
e(2,4).
e(3,4).
e(3,5).
e(4,5).
f(2,5).
f(3,5).
f(4,5).
f(3,4).
f(1,4).
f(1,3).
附录 3
现在使用示例图 e 和 f 查询完整算法时，结果为：
[debug] ?- graph_equal(e,f,MAP).
MAP = [_G2295, 5, 1, 3, 4, 2, _G2313, _G2316, _G2319|...] ;
MAP = [_G2295, 5, 1, 4, 3, 2, _G2313, _G2316, _G2319|...] ;
这意味着这些图是同构的，具有可能的节点映射 e:[5,1,3,4,2] => f:[1,2,3,4,5] 和 e:[5,1,4,3,2] => f:[1,2,3,4,5]。
附录 4
基本基准。单解：
?- time( graph_equal(e,f,_) ).
% 443 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 1718453 Lips)
所有解决方案：
?- time( (graph_equal(e,f,_),fail) ).
% 567 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 2027266 Lips)
使用另一种方法解决。附上代码（算法在代码中）
上一个的一些谓词。案例仍然存在（如 try_bind）。
代码：
% Author: Denis Korekov
% Description of algorithm:
% G1 is graph 1, G2 is graph 2
% E1 is edge of G1, E2 is edge of G2
% V1 is vertex of G1, V2 is vertex of G2
% 0) Check that graphs can be isomorphic (refer to "initial_verify" predicate)
% 1) Pick V1 and some V2 and remove them from vertices lists
% 2) Ensure that none of chosen vertices are in relative closed lists (otherwise continue but remove them)
% 3) Bind (map) V1 to V2
% 4) Expand V1 and V2
% 5) Ensure that degrees of expansions are the same
% 6) Append expansion results to the end of vertices lists and repeat
% define graph predicates here
% graph predicates end
% as we have undirected edges
way_g1(X, Y):- e(X, Y).
way_g1(X, Y):- e(Y, X).
way_g2(X, Y):- f(X, Y).
way_g2(X, Y):- f(Y, X).
% returns all vertices of graphs (non-repeating)
graph1_v(RES):-findall(X, way_g1(X, _), LS), nodes(LS, [], RES).
graph2_v(RES):-findall(X, way_g2(X, _), LS), nodes(LS, [], RES).
% returns all edges of graphs in form "e(X, Y)"
graph1_e(RES):-findall(edge(X, Y), e(X, Y), RES).
graph2_e(RES):-findall(edge(X, Y), f(X, Y), RES).
% returns a list of vertices (removes repeating vertices in a list)
% 1 - list of vertices
% 2 - closed list (discovered vertices)
% 3 - resulting list
nodes([], CL_LS, RES):-append(CL_LS, [], RES).
nodes([X|Rest], CL_LS, RES):- not(member(X, CL_LS)), nodes(Rest, .(X, CL_LS), RES).
nodes([X|Rest], CL_LS, RES):-member(X, CL_LS), nodes(Rest, CL_LS, RES).
% required predicate
iso:-graph1_v(V1), graph2_v(V2), graph1_e(E1), graph2_e(E2), initial_verify(V1, V2, E1, E2), iso_acc(V1, V2, [], [], [], _).
% same as above but outputs result (outputs resulting binding map)
iso_w:-graph1_v(V1), graph2_v(V2), graph1_e(E1), graph2_e(E2), initial_verify(V1, V2, E1, E2), iso_acc(V1, V2, [], [], [], RES_MAP), write(RES_MAP).
% initial verification that graphs at least CAN BE isomorphic
% checks the number of vertices and edges as well as degrees
% 1 - vertices of G1
% 2 - vertices of G2
% 3 - edges of G1
% 4 - edges of G2
initial_verify(X_V, Y_V, X_E, Y_E):-
length(X_V, X_VL),
length(Y_V, Y_VL),
X_VL=Y_VL,
length(X_E, X_EL),
length(Y_E, Y_EL),
X_EL=Y_EL,
get_degree_sequence_g1(X_V, [], X_S),
get_degree_sequence_g2(Y_V, [], Y_S),
%compare degree sequences
compare_lists(X_S, Y_S).
% main algorithm
% 1 - list of vertices of G1
% 2 - list of vertices of G2
% 3 - closed list of G1
% 4 - closed list of G2
% 5 - initial binding map
% 6 - resulting binding map
% if both vertices lists are empty -> isomorphic, backtrack and cut
iso_acc([], [], _, _, ISO_MAP, RES):-append(ISO_MAP, [], RES), !.
% otherwise for every node of G1, for every root of G2
iso_acc([X|X_Rest], Y_LS, CL_X, CL_Y, ISO_MAP, RES):-
select(Y, Y_LS, Y_Rest),
%if X or Y in closed -> continue (next predicate)
not(member(X, CL_X)),
not(member(Y, CL_Y)),
%map X to Y
try_bind(b(X, Y), ISO_MAP, UPD_MAP),
%expand X and Y, use CL_X and CL_Y
expand_g1(X, CL_X, CL_X_UPD, X_RES, X_L),
expand_g2(Y, CL_Y, CL_Y_UPD, Y_RES, Y_L),
%compare lengths of expansions
X_L=Y_L,
%if OK continue with iso_acc with new closed lists and new mapping
append(X_Rest, X_RES, X_NEW),
append(Y_Rest, Y_RES, Y_NEW),
iso_acc(X_NEW, Y_NEW, CL_X_UPD, CL_Y_UPD, UPD_MAP, RES).
% executed in case X and some Y are in closed list (skips such elements)
iso_acc([X|X_Rest], Y_LS, CL_X, CL_Y, ISO_MAP, RES):-
select(Y, Y_LS, Y_Rest),
member(X, CL_X),
member(Y, CL_Y),
iso_acc(X_Rest, Y_Rest, CL_X, CL_Y, ISO_MAP, RES).
% returns sorted degree sequence
% 1 - list of vertices
% 2 - current degree sequence
% 3 - resulting degree sequence
get_degree_sequence_g1([], DEG_S, RES):-
insert_sort(DEG_S, RES).
get_degree_sequence_g1([X|Rest], DEG_S, RES):-
findall(X, way_g1(X, _), LS),
length(LS, L),
append([L], DEG_S, DEG_S_UPD),
get_degree_sequence_g1(Rest, DEG_S_UPD, RES).
get_degree_sequence_g2([], DEG_S, RES):-
insert_sort(DEG_S, RES).
get_degree_sequence_g2([X|Rest], DEG_S, RES):-
findall(X, way_g2(X, _), LS),
length(LS, L),
append([L], DEG_S, DEG_S_UPD),
get_degree_sequence_g2(Rest, DEG_S_UPD, RES).
% compares two lists element by element
compare_lists([], []).
compare_lists([X|X_Rest], [Y|Y_Rest]):-
X=Y,
compare_lists(X_Rest, Y_Rest).
% checks whether binding exist, if not adds it (binding cannot be added if some other binding referring to same
% variables exists already (i.e. (1, 2) cannot be added if (2, 2) exists)
% 1 - binding to add / check in form "b(X, Y)"
% 2 - initial binding map
% 3 - resulting binding map (may remain the same)
try_bind(b(X, Y), MAP, MAP):-
member(b(X, Z), MAP),
Z=Y,
member(b(W, Y), MAP),
W=X.
try_bind(b(X, Y), MAP, UPD_MAP):-
not(member(b(X, _), MAP)),
not(member(b(_, Y), MAP)),
append([b(X, Y)], MAP, UPD_MAP).
% returns updated closed list (X goes to CL), children of X, Length of children, TODO: members of closed lists should not be repeated.
% 1 - Node to expand
% 2 - initial closed list
% 3 - updated closed list (result)
% 4 - updated binding map (result)
% 5 - quantity of children (result)
expand_g1(X, CL, CL_UPD, RES, L):-
findall(Y, (way_g1(X, Y), (not(member(Y, CL)))), LS),
%set results
append(LS, [], RES),
%update closed list
append([X], CL, CL_UPD),
%set length
length(RES, L).
expand_g2(X, CL, CL_UPD, RES, L):-
findall(Y, (way_g2(X, Y), (not(member(Y, CL)))), LS),
%set results
append(LS, [], RES),
%update closed list
append([X], CL, CL_UPD),
%set length
length(RES, L).
% sort algorithm, used in degree sequence verification (simple insertion sort)
% 1 - list to sort
% 2 - result
insert_sort(LS, RES):-insert_sort_acc(LS, [], RES).
insert_sort_acc([], RES, RES).
insert_sort_acc([X|Rest], LS, RES):-insert(X, LS, RES1), insert_sort_acc(Rest, RES1, RES).
% insert item at list
% 1 - item to insert
% 2 - list to insert to
% 3 - result
insert(X,[],[X]).
insert(X, [Y|Rest], [X, Y|Rest]):-X=<Y, !.
insert(X, [Y|Y_Rest], [Y|RES_Rest]):-insert(X, Y_Rest, RES_Rest).
% ?- iso(ListArchiE,ListArchiF,ListNodiE,ListNodiF,Rel_archi).
e(a,b).
e(b,c).
e(b,d).
e(a,c).
e(d,a).
f(50,10).
f(10,11).
f(11,50).
f(10,45).
f(11,45).
iso(ListaArchiE,ListaArchiF,ListaNodiE,ListaNodiF,Rel_archi) :-
findall((X,Y), e(X,Y), ListaArchiE),
findall((X,Y), f(X,Y), ListaArchiF),
setof(X, Y^(e(X,Y);e(Y,X)), ListaNodiE),
setof(X, Y^(f(X,Y);f(Y,X)), ListaNodiF),
!,
rel_nodi(ListaNodiE,ListaNodiF,Rel_nodi),
rel_archi(ListaArchiE,ListaArchiF,Rel_nodi,Rel_archi).
rel_nodi([],[],[]).
rel_nodi([Nodo_e|Resto_e], ListaNodiF, [(Nodo_e,Nodo_f)|R]) :-
select(Nodo_f, ListaNodiF, Resto_f),
rel_nodi(Resto_e, Resto_f, R).
rel_archi([],[],_,[]).
rel_archi([(Ep,Ed)|Resto_e],ListaArchiF,Rel_nodi, [(e(Ep,Ed),f(Fp,Fd))|R]) :-
select((Fp,Fd),ListaArchiF,Resto_f),
member((Ep,Fp),Rel_nodi),
member((Ed,Fd),Rel_nodi),
rel_archi(Resto_e,Resto_f,Rel_nodi,R).
正在尝试解决这里的同构图问题。
作业信息：
- 判断2个无向图是否同构
- 没有孤立的顶点。
- 顶点数小于30
图的边作为谓词给出，即
e(1, 2). f(1, 2).
我正在尝试使用以下方法：
- 对于每对边（即图 1 和 2 中的每条边）
- 尝试绑定2条边的顶点
- 如果无法绑定顶点（即已经存在与其中一个顶点的另一个绑定），则回溯并尝试另一对边。
- 否则添加绑定并继续处理其余图形（即删除每个图形的一条边并再次应用程序）。
除非两个图都为空（意味着所有顶点都从一个图绑定到另一个图），否则程序会重复进行，这意味着成功。 否则程序应该总是失败（即没有其他可用的绑定组合等）
我的代码似乎有效，但仅适用于小图（猜测是因为它尝试了所有对 :)）。
因此，如果有人知道如何优化代码（我相信可以插入几个削减并且 try_bind 可以用更好的方式编写）或者可以提前告诉更好的方法。
P.s。为了检查非同构，我知道我们可以检查不变量等。现在这并不重要。
代码：
%define graph, i.e. graph is a list of edges
graph1(RES):-findall(edge(X,Y), e(X, Y), RES).
graph2(RES):-findall(edge(X,Y), f(X, Y), RES).
%define required predicate
iso:-graph1(G1), graph2(G2), iso_acc(G1, G2, [], _).
%same as above but outputs result
iso_w:-graph1(G1), graph2(G2), iso_acc(G1, G2, [], RES_MAP), write(RES_MAP).
iso_acc([], [], MAP, RES):-append(MAP, [], RES), !.
iso_acc([X|X_Rest], Y_LS, MAP, RES_MAP):-
select(Y, Y_LS, Y_Rest),
bind(X, Y, MAP, UPD_MAP),
iso_acc(X_Rest, Y_Rest, UPD_MAP, RES_MAP).
% if edges bind is successful then in RES or UPD_MAP updated binding map is returned (may return the same map
% if bindings are already defined), otherwise fails
bind([], [], MAP, RES):-append(MAP, [], RES), !.
bind(edge(X1, Y1), edge(X2, Y2), MAP, UPD_MAP):-
try_bind(b(X1, X2), MAP, RES),
try_bind(b(Y1, Y2), RES, UPD_MAP).
bind(edge(X1, Y1), edge(X2, Y2), MAP, UPD_MAP):-
try_bind(b(X1, Y2), MAP, RES),
try_bind(b(Y1, X2), RES, UPD_MAP).
%if an absolute member, we're OK (absolute member means b(X,Y) is already defined
try_bind(b(X, Y), MAP, UPD_MAP):-
member(b(X, Y), MAP),
append(MAP, [], UPD_MAP), !.
%otherwise check that we don't have other binding to X or to Y
try_bind(b(X, Y), MAP, UPD_MAP):-
member(b(X, Z), MAP),
%check if Z != Y
Z=Y,
append(MAP, [], UPD_MAP).
try_bind(b(X, Y), MAP, UPD_MAP):-
member(b(W, Y), MAP),
%check if W == X
W=X,
append(MAP, [], UPD_MAP).
%finally if we not an absolute member and if no other bindings to X and Y we add new binding
try_bind(b(X, Y), MAP, UPD_MAP):-
not(member(b(X, Z), MAP)),
not(member(b(W, Y), MAP)),
append([b(X, Y)], MAP, UPD_MAP).
首先，祝贺您很好地介绍了问题并提出了详尽的解决方案。
在下一段中，我将讨论您的解决方案的实施细节。
不幸的是，我必须说我没有看到这种解决方案的方法可以扩展到更大的尺寸。假设有 10 个边的图。 iso_acc/4 尝试将第一条边分配给第二条边中的任何一条边（10 种可能性），第二条边也绑定到任何一条边（前一条边有 10 种可能性：10*10），...。如果不是运气好的话，那就是 10^10 种可能性，10！考虑到其中大多数的修剪速度更快。
次要评论是：
您可以跳过append(X,[],Y)的用法，所以
bind([],[],MAP,RES) :- append(MAP,[],RES), !.
可以是：
bind([],[],MAP,MAP).
try_bind/3中的第二条和第三条规则似乎没有必要，在上一条中你已经验证了没有b(X,Y)属于MAP。换句话说，member(b(X,Y),MAP) 等价于 member(b(X,Z),MAP), Z=Y.
附录
让我们试试下面的方法。让示例图 e 为：
+----3----+
1 ---2--+ | +---5
+----4----+
和图表f是：
+----3----+
2 ---5--+ | +---1
+----4----+
基本算法可以是：
memb( X-A, [X-B|_] ) :- permutation(A,B).
memb( X, [_|Q] ) :- memb(X, Q).
match( [], _ ).
match( [H|Q], G2 ) :-
memb(H,G2),
match(Q,G2).
graph_equal(G1,G2,MAP) :-
bagof( X, graph_to_list(G1,X), L1 ),
length(MAP,40),
bagof( X, graph_to_list_vars(G2,MAP,X), L2 ), !,
length( L1, S ),
length( L2, S ),
match( L1, L2 ).
从这个出发点，可以进行优化。
此算法需要一些初始数据转换器，以将每个图形转换为 node-[peer1,peer2,...] 形式的项目列表。此转换的规则是：
bidir(G,X,Y) :- ( call(G,X,Y); call(G,Y,X) ).
bidir_vars(G,MAP,VX,VY) :-
bidir(G,X,Y), nth0(X,MAP,VX), nth0(Y,MAP,VY).
graph_to_list( G, N-XL ) :-
setof( X, bidir(G,N,X), XL).
graph_to_list_vars( G, MAP, N-XL ) :-
setof( X, bidir_vars(G,MAP,N,X), XL).
附录 2
这个例子的初始数据是：
e(1,2).
e(2,3).
e(2,4).
e(3,4).
e(3,5).
e(4,5).
f(2,5).
f(3,5).
f(4,5).
f(3,4).
f(1,4).
f(1,3).
附录 3
现在使用示例图 e 和 f 查询完整算法时，结果为：
[debug] ?- graph_equal(e,f,MAP).
MAP = [_G2295, 5, 1, 3, 4, 2, _G2313, _G2316, _G2319|...] ;
MAP = [_G2295, 5, 1, 4, 3, 2, _G2313, _G2316, _G2319|...] ;
这意味着这些图是同构的，具有可能的节点映射 e:[5,1,3,4,2] => f:[1,2,3,4,5] 和 e:[5,1,4,3,2] => f:[1,2,3,4,5]。
附录 4
基本基准。单解：
?- time( graph_equal(e,f,_) ).
% 443 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 1718453 Lips)
所有解决方案：
?- time( (graph_equal(e,f,_),fail) ).
% 567 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 2027266 Lips)
使用另一种方法解决。附上代码（算法在代码中）
上一个的一些谓词。案例仍然存在（如 try_bind）。
代码：
% Author: Denis Korekov
% Description of algorithm:
% G1 is graph 1, G2 is graph 2
% E1 is edge of G1, E2 is edge of G2
% V1 is vertex of G1, V2 is vertex of G2
% 0) Check that graphs can be isomorphic (refer to "initial_verify" predicate)
% 1) Pick V1 and some V2 and remove them from vertices lists
% 2) Ensure that none of chosen vertices are in relative closed lists (otherwise continue but remove them)
% 3) Bind (map) V1 to V2
% 4) Expand V1 and V2
% 5) Ensure that degrees of expansions are the same
% 6) Append expansion results to the end of vertices lists and repeat
% define graph predicates here
% graph predicates end
% as we have undirected edges
way_g1(X, Y):- e(X, Y).
way_g1(X, Y):- e(Y, X).
way_g2(X, Y):- f(X, Y).
way_g2(X, Y):- f(Y, X).
% returns all vertices of graphs (non-repeating)
graph1_v(RES):-findall(X, way_g1(X, _), LS), nodes(LS, [], RES).
graph2_v(RES):-findall(X, way_g2(X, _), LS), nodes(LS, [], RES).
% returns all edges of graphs in form "e(X, Y)"
graph1_e(RES):-findall(edge(X, Y), e(X, Y), RES).
graph2_e(RES):-findall(edge(X, Y), f(X, Y), RES).
% returns a list of vertices (removes repeating vertices in a list)
% 1 - list of vertices
% 2 - closed list (discovered vertices)
% 3 - resulting list
nodes([], CL_LS, RES):-append(CL_LS, [], RES).
nodes([X|Rest], CL_LS, RES):- not(member(X, CL_LS)), nodes(Rest, .(X, CL_LS), RES).
nodes([X|Rest], CL_LS, RES):-member(X, CL_LS), nodes(Rest, CL_LS, RES).
% required predicate
iso:-graph1_v(V1), graph2_v(V2), graph1_e(E1), graph2_e(E2), initial_verify(V1, V2, E1, E2), iso_acc(V1, V2, [], [], [], _).
% same as above but outputs result (outputs resulting binding map)
iso_w:-graph1_v(V1), graph2_v(V2), graph1_e(E1), graph2_e(E2), initial_verify(V1, V2, E1, E2), iso_acc(V1, V2, [], [], [], RES_MAP), write(RES_MAP).
% initial verification that graphs at least CAN BE isomorphic
% checks the number of vertices and edges as well as degrees
% 1 - vertices of G1
% 2 - vertices of G2
% 3 - edges of G1
% 4 - edges of G2
initial_verify(X_V, Y_V, X_E, Y_E):-
length(X_V, X_VL),
length(Y_V, Y_VL),
X_VL=Y_VL,
length(X_E, X_EL),
length(Y_E, Y_EL),
X_EL=Y_EL,
get_degree_sequence_g1(X_V, [], X_S),
get_degree_sequence_g2(Y_V, [], Y_S),
%compare degree sequences
compare_lists(X_S, Y_S).
% main algorithm
% 1 - list of vertices of G1
% 2 - list of vertices of G2
% 3 - closed list of G1
% 4 - closed list of G2
% 5 - initial binding map
% 6 - resulting binding map
% if both vertices lists are empty -> isomorphic, backtrack and cut
iso_acc([], [], _, _, ISO_MAP, RES):-append(ISO_MAP, [], RES), !.
% otherwise for every node of G1, for every root of G2
iso_acc([X|X_Rest], Y_LS, CL_X, CL_Y, ISO_MAP, RES):-
select(Y, Y_LS, Y_Rest),
%if X or Y in closed -> continue (next predicate)
not(member(X, CL_X)),
not(member(Y, CL_Y)),
%map X to Y
try_bind(b(X, Y), ISO_MAP, UPD_MAP),
%expand X and Y, use CL_X and CL_Y
expand_g1(X, CL_X, CL_X_UPD, X_RES, X_L),
expand_g2(Y, CL_Y, CL_Y_UPD, Y_RES, Y_L),
%compare lengths of expansions
X_L=Y_L,
%if OK continue with iso_acc with new closed lists and new mapping
append(X_Rest, X_RES, X_NEW),
append(Y_Rest, Y_RES, Y_NEW),
iso_acc(X_NEW, Y_NEW, CL_X_UPD, CL_Y_UPD, UPD_MAP, RES).
% executed in case X and some Y are in closed list (skips such elements)
iso_acc([X|X_Rest], Y_LS, CL_X, CL_Y, ISO_MAP, RES):-
select(Y, Y_LS, Y_Rest),
member(X, CL_X),
member(Y, CL_Y),
iso_acc(X_Rest, Y_Rest, CL_X, CL_Y, ISO_MAP, RES).
% returns sorted degree sequence
% 1 - list of vertices
% 2 - current degree sequence
% 3 - resulting degree sequence
get_degree_sequence_g1([], DEG_S, RES):-
insert_sort(DEG_S, RES).
get_degree_sequence_g1([X|Rest], DEG_S, RES):-
findall(X, way_g1(X, _), LS),
length(LS, L),
append([L], DEG_S, DEG_S_UPD),
get_degree_sequence_g1(Rest, DEG_S_UPD, RES).
get_degree_sequence_g2([], DEG_S, RES):-
insert_sort(DEG_S, RES).
get_degree_sequence_g2([X|Rest], DEG_S, RES):-
findall(X, way_g2(X, _), LS),
length(LS, L),
append([L], DEG_S, DEG_S_UPD),
get_degree_sequence_g2(Rest, DEG_S_UPD, RES).
% compares two lists element by element
compare_lists([], []).
compare_lists([X|X_Rest], [Y|Y_Rest]):-
X=Y,
compare_lists(X_Rest, Y_Rest).
% checks whether binding exist, if not adds it (binding cannot be added if some other binding referring to same
% variables exists already (i.e. (1, 2) cannot be added if (2, 2) exists)
% 1 - binding to add / check in form "b(X, Y)"
% 2 - initial binding map
% 3 - resulting binding map (may remain the same)
try_bind(b(X, Y), MAP, MAP):-
member(b(X, Z), MAP),
Z=Y,
member(b(W, Y), MAP),
W=X.
try_bind(b(X, Y), MAP, UPD_MAP):-
not(member(b(X, _), MAP)),
not(member(b(_, Y), MAP)),
append([b(X, Y)], MAP, UPD_MAP).
% returns updated closed list (X goes to CL), children of X, Length of children, TODO: members of closed lists should not be repeated.
% 1 - Node to expand
% 2 - initial closed list
% 3 - updated closed list (result)
% 4 - updated binding map (result)
% 5 - quantity of children (result)
expand_g1(X, CL, CL_UPD, RES, L):-
findall(Y, (way_g1(X, Y), (not(member(Y, CL)))), LS),
%set results
append(LS, [], RES),
%update closed list
append([X], CL, CL_UPD),
%set length
length(RES, L).
expand_g2(X, CL, CL_UPD, RES, L):-
findall(Y, (way_g2(X, Y), (not(member(Y, CL)))), LS),
%set results
append(LS, [], RES),
%update closed list
append([X], CL, CL_UPD),
%set length
length(RES, L).
% sort algorithm, used in degree sequence verification (simple insertion sort)
% 1 - list to sort
% 2 - result
insert_sort(LS, RES):-insert_sort_acc(LS, [], RES).
insert_sort_acc([], RES, RES).
insert_sort_acc([X|Rest], LS, RES):-insert(X, LS, RES1), insert_sort_acc(Rest, RES1, RES).
% insert item at list
% 1 - item to insert
% 2 - list to insert to
% 3 - result
insert(X,[],[X]).
insert(X, [Y|Rest], [X, Y|Rest]):-X=<Y, !.
insert(X, [Y|Y_Rest], [Y|RES_Rest]):-insert(X, Y_Rest, RES_Rest).
% ?- iso(ListArchiE,ListArchiF,ListNodiE,ListNodiF,Rel_archi).
e(a,b).
e(b,c).
e(b,d).
e(a,c).
e(d,a).
f(50,10).
f(10,11).
f(11,50).
f(10,45).
f(11,45).
iso(ListaArchiE,ListaArchiF,ListaNodiE,ListaNodiF,Rel_archi) :-
findall((X,Y), e(X,Y), ListaArchiE),
findall((X,Y), f(X,Y), ListaArchiF),
setof(X, Y^(e(X,Y);e(Y,X)), ListaNodiE),
setof(X, Y^(f(X,Y);f(Y,X)), ListaNodiF),
!,
rel_nodi(ListaNodiE,ListaNodiF,Rel_nodi),
rel_archi(ListaArchiE,ListaArchiF,Rel_nodi,Rel_archi).
rel_nodi([],[],[]).
rel_nodi([Nodo_e|Resto_e], ListaNodiF, [(Nodo_e,Nodo_f)|R]) :-
select(Nodo_f, ListaNodiF, Resto_f),
rel_nodi(Resto_e, Resto_f, R).
rel_archi([],[],_,[]).
rel_archi([(Ep,Ed)|Resto_e],ListaArchiF,Rel_nodi, [(e(Ep,Ed),f(Fp,Fd))|R]) :-
select((Fp,Fd),ListaArchiF,Resto_f),
member((Ep,Fp),Rel_nodi),
member((Ed,Fd),Rel_nodi),
rel_archi(Resto_e,Resto_f,Rel_nodi,R).