寻找一组边添加到一组图中以满足连通性约束

Question

我有一组 N 个无向、不连通的图，它们共享相同的 M 个顶点，但有不同的边。对于“V₀ 连接到 V₁”或“V_{”形式的每个图，我也有一组约束3}没有连接到V₅”等等

我想找到一组边，以便将这些边添加到每个图都会使每个图都满足其约束。

举个简单的例子，考虑两个给定的顶点为 V₀、V₁、V _的图2, V₃, V₄:

• 具有一条边的图 G (V₀, V₁) 和约束 "V₀ 连接到 V₂"
• 具有边（V₁、V₃）和约束“V₂ 连接到 V₄", "V₀ 是 not 连接到 V₂"

使用这些给定的参数，通过添加边 {(V₁, V₂), (V₃, V₄)} 到两个图。

---

在无法使用脚本解决问题后，我寻求 z3 的帮助，但我 运行 在尝试表达连接时遇到了麻烦。我当前的解决方案包含一个只有布尔项的未量化公式：

• c_i,j,k对于每对顶点i,j表示它们在图中是否连通k 添加了解
的边
• g_i,j,k对于每对顶点i,j表示它们之间的边是否在图中给出k
• s_i,j 每对顶点 i, j 表示在它们之间添加一条边是否是解决方案的一部分

和断言：

• g_i,j,k 如果边(i, j)在图k[中给出=164=]
• ¬g_i,j,k 如果边 (i, j) 是 not 图中给出 k
• c_i,j,k 如果图形 k 需要 i 和 j待连接
• ¬s_i,j ∧ ¬c_i,j,k 如果图 k需要i和j才能不连接
• s_i,j ⇒ c_i,j,k 对于所有图 k
• c_i,j,k = s_i,j ∨ g_i,j,k ∨ ((s_i,z ∨ g_i,z,k) ∧ c_z,j,k ) 所有顶点 i, j, z 和图 k

然而，最后一个子句似乎没有像预期的那样工作以表达连接性，z3 正在返回 sat 但显然必要的 s_i,j 是错误的在生成的模型中。

这是我能设法做出的最短的问题示例：

from itertools import combinations

from z3 import *

vertices = [0, 1, 2, 3, 4]
edges = [tuple(sorted(edge)) for edge in list(combinations(vertices, 2))]

graphs = {
    "G": [(0, 1)],
    "H": [(1, 3)],
}

facts = Solver()

connected_in_graph = {}
for graph in graphs:
    for edge in edges:
        connected_in_graph[(graph, edge)] = Bool(f"{edge}_conn_in_{graph}")

solution_edges = {}
graph_given_edges = {}
for edge in edges:
    edge_in_solution = Bool(f"{edge}_in_solution")
    solution_edges[edge] = edge_in_solution
    for graph in graphs:
        given = Bool(f"{graph}_{edge}_given")
        graph_given_edges[(graph, edge)] = given
        if edge in graphs[graph]:
            facts.append(given)
        else:
            facts.append(Not(given))

facts.append(
    connected_in_graph[("G", (0, 2))],
    connected_in_graph[("H", (2, 4))],
    Not(connected_in_graph[("H", (0, 2))]),
)

for edge in edges:
    for graph in graphs:
        ors = [
            solution_edges[edge],
            graph_given_edges[(graph, edge)],
        ]
        for vertex in vertices:
            if vertex in edge:
                continue
            l_edge = tuple(sorted((edge[0], vertex)))
            r_edge = tuple(sorted((edge[1], vertex)))
            ors.append(
                And(
                    Or(
                        solution_edges[l_edge],
                        graph_given_edges[(graph, l_edge)],
                    ),
                    connected_in_graph[(graph, r_edge)],
                )
            )
        facts.append(connected_in_graph[(graph, edge)] == Or(*ors))

print(facts.check())
model = facts.model()
for edge in edges:
    c = solution_edges[edge]
    if model[c]:
        print(c)

我想我真正需要表达的是关系：

c2(i, j, k, through) = s_i,j ∨ g_i,j,k ∨ (∃z. z ∉ (忽略 ∪ {i, j}) ∧ (s_i,z ∨ g_i,z,k) ∧ c(z, j, k, 忽略 ∪ {i }))

c(i, j, k) = c2(i, j, k, {})

但是，将其简化为未量化的布尔项显然需要 M 的数量级！时间和 space.

在 SAT/SMT 中是否有更好的方式来表达图中路径的存在，或者是否有更好的方式来解决这个问题？

---

Alias 关于使用传递闭包的建议似乎是解决这个问题的方法，但我似乎无法正确使用它。我修改后的代码：

from itertools import combinations

from z3 import *

vertices = [0, 1, 2, 3, 4]
edges = [tuple(sorted(edge)) for edge in list(combinations(vertices, 2))]

graphs = {
    "G": [(0, 1)],
    "H": [(1, 3)],
}

facts = Solver()

vs = {}
VertexSort = DeclareSort("VertexSort")
for vertex in vertices:
    vs[vertex] = Const(f"V{vertex}", VertexSort)
facts.add(Distinct(*vs.values()))

given = {}
directly_connected = {}
tc_connected = {}
for graph in graphs:
    given[graph] = Function(
        f"{graph}_given", VertexSort, VertexSort, BoolSort()
    )
    directly_connected[graph] = Function(
        f"directly_connected_{graph}", VertexSort, VertexSort, BoolSort()
    )
    tc_connected[graph] = TransitiveClosure(directly_connected[graph])

in_solution = Function("in_solution", VertexSort, VertexSort, BoolSort())


for edge in edges:
    # commutativity
    facts.add(
        in_solution(vs[edge[0]], vs[edge[1]])
        == in_solution(vs[edge[1]], vs[edge[0]])
    )
    for graph in graphs:
        # commutativity
        facts.add(
            given[graph](vs[edge[0]], vs[edge[1]])
            == given[graph](vs[edge[1]], vs[edge[0]])
        )
        facts.add(
            directly_connected[graph](vs[edge[0]], vs[edge[1]])
            == directly_connected[graph](vs[edge[1]], vs[edge[0]])
        )
        # definition of direct connection
        facts.add(
            directly_connected[graph](vs[edge[0]], vs[edge[1]])
            == Or(
                in_solution(vs[edge[0]], vs[edge[1]]),
                given[graph](vs[edge[0]], vs[edge[1]]),
            ),
        )
        if edge in graphs[graph]:
            facts.add(given[graph](vs[edge[0]], vs[edge[1]]))
        else:
            facts.add(Not(given[graph](vs[edge[0]], vs[edge[1]])))


facts.append(
    tc_connected["G"](vs[0], vs[2]),
    tc_connected["H"](vs[2], vs[4]),
    Not(tc_connected["H"](vs[0], vs[2])),
)

print(facts.check())
model = facts.model()
print(model)
print(f"solution: {model[in_solution]}")

打印 sat 但找到定义 in_solution = [else -> False] 而不是我正在寻找的解决方案。我做错了什么？

Answer 1

根据 @alias in , solving the problem was made possible by using transitive closures 的建议。

作者：

• 定义关系 给定_G(v1, v2) 和 directly_connected _G(v1, v2) 每个图 G 和关系 in_solution(v1, v2) 其中 v1, v2 是枚举类型，每个顶点都有构造函数
• 断言 directly_connected_G(v1, v2) = in_solution(v1, v2) ∨ given_G(v1, v2) 每个 v1, v2
• 为每个图 G
声明传递闭包 TC_connected_G(v1, v2)
• 根据 TC_connected
声明约束

我让求解器 return 为我的所有测试用例提供了正确的解决方案。

修改后的代码：

from itertools import combinations

from z3 import *

vertices = [0, 1, 2, 3, 4]
edges = [tuple(sorted(edge)) for edge in list(combinations(vertices, 2))]

graphs = {
    "G": [(0, 1)],
    "H": [(1, 3)],
}

facts = Solver()


VertexSort = Datatype("VertexSort")
for vertex in vertices:
    VertexSort.declare(str(vertex))
VertexSort = VertexSort.create()

vs = {}
for vertex in vertices:
    vs[vertex] = getattr(VertexSort, str(vertex))


given = {}
directly_connected = {}
tc_connected = {}
for graph in graphs:
    given[graph] = Function(
        f"{graph}_given", VertexSort, VertexSort, BoolSort()
    )
    directly_connected[graph] = Function(
        f"directly_connected_{graph}", VertexSort, VertexSort, BoolSort()
    )
    tc_connected[graph] = TransitiveClosure(directly_connected[graph])

in_solution = Function("in_solution", VertexSort, VertexSort, BoolSort())


for edge in edges:
    # commutativity
    facts.add(
        in_solution(vs[edge[0]], vs[edge[1]])
        == in_solution(vs[edge[1]], vs[edge[0]])
    )
    for graph in graphs:
        # commutativity
        facts.add(
            given[graph](vs[edge[0]], vs[edge[1]])
            == given[graph](vs[edge[1]], vs[edge[0]])
        )
        facts.add(
            directly_connected[graph](vs[edge[0]], vs[edge[1]])
            == directly_connected[graph](vs[edge[1]], vs[edge[0]])
        )
        # definition of direct connection
        facts.add(
            directly_connected[graph](vs[edge[0]], vs[edge[1]])
            == Or(
                in_solution(vs[edge[0]], vs[edge[1]]),
                given[graph](vs[edge[0]], vs[edge[1]]),
            ),
        )
        if edge in graphs[graph]:
            facts.add(given[graph](vs[edge[0]], vs[edge[1]]))
        else:
            facts.add(Not(given[graph](vs[edge[0]], vs[edge[1]])))


facts.append(
    tc_connected["G"](vs[0], vs[2]),
    tc_connected["H"](vs[2], vs[4]),
    Not(tc_connected["H"](vs[0], vs[2])),
)

print(facts.check())
model = facts.model()
print(f"solution: {model[in_solution]}")