z3 - 约束规划网状网络

Question

我有一个网状网络，如图所示。现在，我正在为这个 sat 网络中的所有边分配值。我想在我的程序中提出，我的分配中没有闭环。例如，最左上角的约束可以写成 -

E0 = 0 或 E3 = 0 或 E4 = 0 或 E7 = 0，因此任何一个链接都必须处于非事件状态才能不形成循环。然而，在这种网络中，存在许多可能的环路。

例如由边形成的循环 - E0、E3、E7、E11、E15、E12、E5、E1。

现在我的问题是我必须描述这个网络中可能出现的每个可能的环路组合。我试图在一种可能的公式中编写约束，但是我没能成功。

如果有可能的方法来编码这种情况，任何人都可以提出任何指示吗？仅供引用，我使用的是 Z3 Sat Solver。

Answer 1

以下编码可用于任何具有 N 个节点和 M 个边的图。它使用 (N+1)*M 变量和 2*M*M 3-SAT 子句。 This ipython notebook 通过将 SAT 求解器结果(存在循环时为 UNSAT，否则为 SAT)与直接循环查找算法的结果进行比较来演示编码。

免责声明:此编码是我针对该问题的临时解决方案。我很确定它是正确的，但我不知道它在性能方面与其他编码相比如何解决这个问题。由于我的解决方案适用于任何图表，因此可以预期存在更好的解决方案，该解决方案使用 OP 感兴趣的图表类的某些属性。

变量:

每条边都有一个变量。如果设置了相应的变量，则边缘是“事件的”或“已使用的”。在我的引用实现中，边缘有索引 0..(M-1) 并且这个变量有索引 1..M:

def edge_state_var(edge_idx):
    assert 0 <= edge_idx < M
    return 1 + edge_idx

然后我有一个 M 位宽度的状态变量用于每个边缘，或者总共 N*M 状态位(节点和位也使用从零开始的索引):

def node_state_var(node_idx, bit_idx):
    assert 0 <= node_idx < N
    assert 0 <=  bit_idx < M
    return 1 + M + node_idx*M + bit_idx

从句:

当边处于事件状态时，它将它所连接的两个节点的状态变量链接在一起。与该节点具有相同索引的状态位必须在两侧不同，并且其他状态位必须等于它们在另一个节点上的对应伙伴。在 python 代码中:

# which edge connects which nodes
connectivity = [
    ( 0,  1), # edge E0
    ( 1,  2), # edge E1
    ( 2,  3), # edge E2
    ( 0,  4), # edge E3
    ...
]

cnf = list()

for i in range(M):
    eb = edge_state_var(i)
    p, q = connectivity[i]
    for k in range(M):
        pb = node_state_var(p, k)
        qb = node_state_var(q, k)
        if k == i:
            # eb -> (pb != qb)
            cnf.append([-eb, -pb, -qb])
            cnf.append([-eb, +pb, +qb])
        else:
            # eb -> (pb == qb)
            cnf.append([-eb, -pb, +qb])
            cnf.append([-eb, +pb, -qb])

所以基本上每条边都试图将它所属的图分割成边一侧的一半，并将与边对应的所有状态位设置为 1 和另一边的一半边缘并将与边缘对应的状态位设置为 0。对于可以从循环中每个边缘的两侧都可以到达循环中的所有节点的循环来说，这是不可能的。