Z3 中的子图同构（或什至集合成员）？

Question

我试图找到一种方法来在 Z3（最好是 z3py）中编码一种基本的子图同构。虽然我知道在摘要中有关于此的论文，但即使对于非常微不足道的情况，我也找不到任何机制来做到这一点，因为我对 Z3 总体来说还是个新手！

假设您只有最基本的子图，其中节点 (0,1,2) 和边 (0,1) 节点 2 独立，并且超图有节点 (0,1,2)和边缘 (1,2) 与节点 0 自己关闭。您可以使用

将子图的节点映射到超图中

0->1,
1->2,
2->0

...作为满足“如果这两个节点在子图中连接，则它们的映射节点在超图中连接”的一种可能映射

很好 :) 我试过了

from networkx import Graph
from networkx.linalg.graphmatrix import adjacency_matrix

subgraph = Graph()
subgraph.add_nodes_from([0,1,2])
subgraph.add_edges_from([(0,1)])

supergraph = Graph()
supergraph.add_nodes_from([0,1,2])
supergraph.add_edges_from([(1,2)])

s = Solver()
assignments = [Int(f'n{node}') for node in subgraph.nodes]

# each bit assignment in the subgraph belongs to one in the supergraph
assignment_constraint = [ And(assignments[i] >= 0, assignments[i] <= max(supergraph.nodes)) for i in subgraph.nodes ]
# subgraph bits can't be assigned to the same supergraph bits
assignment_distinct = [ Distinct([assignments[i] for i in subgraph.nodes])]

这让我明白“从子图到超图的每个分配都应该将子图中的一个节点映射到超图中的某个节点，并且不能将两个子图节点分配给同一个超图节点”

...但后来我卡住了，因为我一直在思考

for edge in subgraph.edges:
  s.add( (assignments[edge[0]], assignments[edge[1]]) in supergraph.edges )

...但这当然行不通，因为在 Python 中，这些键不是正确的类型，所以它总是错误的或损坏的。

那么如何处理呢？我可以添加诸如“this_var == 1”之类的约束，但在检查成员资格等事情上会感到非常困惑，即

>>> assignments[0] == 1.0
n0 == 1  # so that's OK then
>>> assignments[0] in [1.0, 2.0, 3.0]
False  # woops, that fails horribly

我觉得我在这里缺少一个非常基本的“心态”。

Answer 1

在 z3 中编码子图同构相对简单，几乎与您描述的方式一致。然而，这种编码不太可能扩展到大图。你肯定知道，子图同构一般来说是NP完全的，这种编码会导致z3简单地枚举所有的可能性，从而呈指数爆炸。

话虽如此，这里有一个简单的编码：

from z3 import *

# Subgraph, number of nodes and edges.
# Nodes will be named implicitly from 0 to noOfNodesA - 1
noOfNodesA = 3
edgesA = [(0, 1)]

# Supergraph:
noOfNodesB = 3
edgesB = [(1, 2)]

# Mapping of subgraph nodes to supergraph nodes:
mapping = Array('Map', IntSort(), IntSort())

s = Solver()

# Check that elt is between low and high, inclusive
def InRange(elt, low, high):
    return And(low <= elt, elt <= high)

# Check that (x, y) is in the list
def Contains(x, y, lst):
    return Or([And(x == x1, y == y1) for x1, y1 in lst])


# Make sure mapping is into the supergraph
s.add(And([InRange(Select(mapping, n1), 0, noOfNodesB-1) for n1 in range(noOfNodesA)]))

# Make sure we map nodes to distinct nodes
s.add(Distinct([Select(mapping, n1) for n1 in range(noOfNodesA)]))

# Make sure edges are preserved:
for x, y in edgesA:
    s.add(Contains(Select(mapping, x), Select(mapping, y), edgesB))

# Solve:
r = s.check()
if r == sat:
    m = s.model()
    for x in range(noOfNodesA):
        print ("%s -> %s" % (x, m.evaluate(Select(mapping, x))))
else:
    print ("Solver said: %s" % r)

我在整个过程中添加了注释，希望您能够通读代码；欢迎提出具体问题。

当我运行这个时，我得到：

$ python a.py
0 -> 1
1 -> 2
2 -> 0

它准确地找到了您在问题中提到的映射。

祝你好运！

Z3 中的子图同构（或什至集合成员）？

Subgraph isomorphism (or even set membership) in Z3?

z3

z3py