子图同构（subgraph isomorphism)问题

图 $S$ 和图 $G$ 的子图有哪些同构的问题可以看成一个约束满足问题(CSP) $\mathcal{\langle X,D,C\rangle}$ ，CSP的详细定义见：约束规划，约束传播和CSP问题

子图同构问题的形式化

简单地说，图 $S$ 在 $G$ 中的嵌入（embedding） $f:V(S)\to V(G)$ 满足

(1) $\nexists v_1,v_2\in V(S), v_1\neq v_2,f(v_1)=f(v_2)$ ,

(2) $\forall e=(v_1,v_2)\in E(S), f(e)=(f(v_1),f(v_2))\in E(G)$ ,

(3) $\forall e\notin E(S), f(e)\notin E(G)$ ,

是 $S$ 和 $G$ 的某个子图的同构

标准形式的子图同构问题

$S$ 的每个结点 $v\in V(S)$ 都对应一个变量 $X(v)$ ，因此可以定义双射 $X:V(S)\to \mathcal X$ ，变量集 $\mathcal X=X(V(S))$

每个结点 $v\in V(S)$ 的嵌入一定是 $G$ 中的结点 $u\in V(G)$ ，因此变量$X(v)$ 对应的域为 $D(X(v))=V(G)$ ，域集 $\mathcal D=D(\mathcal X)$

由条件（1）知，有约束条件 $\mathtt{Alldifferent}(X(V(S))$

由条件（2）知，对 $\forall (v_1,v_2)\in E(S)$ ，有约束条件 $\mathtt{AllowedAssignments}((X(v_1),X(v_2)), E(G))$

由条件（3）知，对 $\forall (v_1,v_2)\notin E(S)$ ，有约束条件 $\mathtt{ForbiddenAssignments}((X(v_1),X(v_2)), E(G))$

综合以上3种约束，有约束集 $\mathcal C=\{\mathtt{Alldifferent}(X(V(S))\}\cup \\ \{ \mathtt{AllowedAssignments}((X(v_1),X(v_2)), E(G)): \forall (v_1,v_2)\in E(S)\}\cup \\ \{\mathtt{ForbiddenAssignments}((X(v_1),X(v_2)), E(G)):\forall (v_1,v_2)\notin E(S)\}$

使用求解器求解同构问题

我们已经把子图同构对应的CSP问题$\mathcal{\langle X,D,C\rangle}$表示成了标准形式，因此可以使用求解器进行求解

OR-tools是谷歌开源的运筹学求解器库，详细介绍见：使用谷歌的OR-Tools求解鸡兔同笼

networkx是python的一个图算法库，详细介绍见：python常用代码的第12和13节

以下代码使用OR-tools和networkx求解子图同构问题：

import networkx as nx
from ortools.sat.python import cp_model
from itertools import combinations
def var_from_domain(model, name, domain):
    "initialize a variable with integer domain defined by domain"
    domain = cp_model.Domain.FromIntervals([[i] for i in domain])
    val = model.NewIntVarFromDomain(domain, name)
    return val

# 五角星
G=nx.Graph([(1,3),(1,4),(2,4),(2,5),(3,5)])
# 五边形
S=nx.Graph([(1,2),(2,3),(3,4),(4,5),(5,1)])

model = cp_model.CpModel()

D = list(G.nodes)
X = {i:var_from_domain(model, "X("+str(i)+")", D) for i in S.nodes}

# 约束：嵌入 S -> subgraph of G
model.AddAllDifferent([X[i] for i in S.nodes])
E_G = list(G.edges) + [e[::-1] for e in G.edges]
for v1, v2 in combinations(S.nodes,2):
    if (v1,v2) in S.edges:
        model.AddAllowedAssignments((X[v1],X[v2]), E_G)
    else:
        model.AddForbiddenAssignments((X[v1],X[v2]), E_G)

solver = cp_model.CpSolver()
status = solver.Solve(model)
if status == cp_model.FEASIBLE:
    print("有嵌入:")
    for v, x in X.items():
        print('f(%s)=%i' % (v, solver.Value(x)))
else:
    print("不存在子图同构")