寻找两个节点之间的路径答案

【问题标题】：Finding path between two nodes寻找两个节点之间的路径
【发布时间】：2014-11-25 08:12:58
【问题描述】：

我想知道是否有一种方法可以在 z3py 中构建拓扑，如果我有 6 个节点，即：n1、n2、n3、n4、n5、n6，并且它们之间有某些链接，例如l12（这意味着节点 n1 和 n2 之间存在链接）、l16、l23、l25、l34、l35、l36。我可以将 l_{i}{j} 定义为 bool 变量，以便它可以参考 2 个节点或节点之间是否存在任何链接（当然我必须以这种方式定义所有可能的链接）。问题是如何在 Z3py 中定义路径的概念，以便我可以确定 2 个节点之间是否存在任何路径（SAT 或 UNSAT，如果 SAT 是哪条路径？）。我尝试寻找 z3py 教程，但它不再在线提供，我是 z3 的新手，所以请多多包涵。我只能在非常幼稚的python中弄清楚以下建模。是否可以在 z3py 中将路径建模为未解释的函数？

graph = {'n1': ['n2', 'n6'],
         'n2': ['n3', 'n5'],
         'n3': ['n4', 'n5','n6'],
         'n4': ['n3'],
         'n5': ['n2', 'n3'],
         'n6': ['n3','n1']}
def path_finder (graph, start, end, path=[]):
    path = path + [start]
    if start == end:
        return path
    if not graph.has_key(start):
        return None
    for node in graph[start]:
        if node not in path:
            newpath = path_finder (graph, node, end, path)
            if newpath: return newpath
    return None

print path_finder (graph, 'n1','n4')

【问题讨论】：

是否有理由为此使用 SMT/SAT？像 Dijkstra 的算法这样简单的东西应该可以解决问题？
附言。一种 SAT 公式如下。让 n_i 是一个布尔变量，表示节点 i 是否在您感兴趣的路径上。如果存在从节点 i 到节点 j 的链接，则将含义 n_i => n_j 添加到您的公式中。然后假设你想要一条从节点 s 到节点 d 的路径，然后假设 n_s = true，并检查 n_d 的可满足性。

标签： z3 smt z3py

【解决方案1】：

我修改了一个Fixpoint example来完成路径搜索

from z3 import *

#  cf. https://ericpony.github.io/z3py-tutorial/fixpoint-examples.htm

fp = Fixedpoint()
fp.set(engine='datalog')

#  3 bits are sufficient to model our 6 nodes
s = BitVecSort(3)
edge = Function('edge', s, s, BoolSort())
path = Function('path', s, s, BoolSort())
a = Const('a', s)
b = Const('b', s)
c = Const('c', s)

#  the rules:
#  a path can be a single edge or
#  a combination of a path and an edge
fp.register_relation(path,edge)
fp.declare_var(a, b, c)
fp.rule(path(a, b), edge(a, b))
fp.rule(path(a, c), [edge(a, b), path(b, c)])

n1 = BitVecVal(1, s)
n2 = BitVecVal(2, s)
n3 = BitVecVal(3, s)
n4 = BitVecVal(4, s)
n5 = BitVecVal(5, s)
n6 = BitVecVal(6, s)
n7 = BitVecVal(7, s)

graph = {n1: [n2, n6, n7],
         n2: [n3, n5],
         n3: [n4, n5, n6],
         n4: [n3],
         n5: [n2, n3],
         n6: [n3, n1]}

#  establish facts by enumerating the graph dictionary
for i, (source, nodes) in enumerate(graph.items()):
    for destination in nodes:
        fp.fact(edge(source, destination))

print("current set of rules:\n", fp)

print(fp.query(path(n1, n4)), "yes, we can reach n4 from n1\n")

print(fp.query(path(n7, n1)), "no, we cannot reach n1 from n7\n")

【讨论】：