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

我有一组N个无向、不相连的图，它们共享相同的M个顶点，但有不同的边。我也有一组约束形式为"V₀连接到V₁"的每个图;或"V₃未连接到V₅;等。

我想找到一组边，使每个图都满足约束条件。

对于一个简单的例子，考虑对于两个给定的图，顶点V₀， V₁， V₂， V₃， V₄:

图G有一条边(V₀， V₁)，约束V₀连接到V₂">
一个边为(V₁， V₃)且约束条件为V₂的图H与V₄相连，且V₀不连接到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如果边缘(,)中给出了k图
¬g<子>i, j, k如果边缘(,)不是中给出图k
c_i,j,k如果图k要求i与j相连接
¬s<子>i, j∧¬c<子>i, j, k如果图k需要我和j不连接
s<子>i, j⇒c<子>我,j, k为所有图k
c<子>i, j, k=<子>我,j∨g子> <我,j,>∨((s<子>,z∨g子> <我,z,>)∧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 (,,k,) = s<子>i, j∨g子> <我,j,>∨(∃z。z∉(忽略∪{i, j})∧(s<子>,z∨g子> <我,z,>)∧c (z, j, k,忽略∪{我}))

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

然而，将其简化为未量化的布尔项显然会花费M的数量级!时间和空间。

在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]，而不是我正在寻找的解决方案。我做错了什么?

正如@alias在评论中建议的那样，可以通过使用传递闭包来解决这个问题。

由:

定义关系给定_G(v1, v2)和直接连接_G(v1, v2)对于每个图G和关系in_solution(v1, v2)，其中v1, v2为每个顶点
断言direcly_connected_G(v1, v2) = in_solution(v1, v2)G v2)∨<子>(v1、v2)为每个v1,v2
为每个图G

TC_connected_G(v1, v2)

根据TC_connected

我得到了求解器返回所有测试用例的正确解决方案。

修改后的代码:

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]}")

相关内容

最新更新

热门标签：