3

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

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

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

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

如果有可能的方法来编码这种情况，任何人都可以抛出任何指针吗？仅供参考，我正在使用 Z3 Sat Solver。

网状网络

4

1 回答 1

1

以下编码可用于任何具有N节点和M边的图。它使用(N+1)*M变量和2*M*M3-SAT 子句。这个ipython 笔记本通过比较 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。对于循环中的所有节点都可以从循环中每个边的两侧到达的循环来说，这是不可能的。

于 2014-12-19T08:54:03.813 回答