时间戳

首页 > 解决方案 > 具有数组数据类型的 z3 建模图

python - 具有数组数据类型的 z3 建模图

问题描述

我正在尝试在 z3 中建模有向图，但我陷入了困境。我在这里的图中添加了一个公理，即边的存在意味着它连接的节点的存在。但仅此一项就会导致不满意

GraphSort = Datatype('GraphSort')
GraphSort.declare('Graph',
    ('V', ArraySort(IntSort(), BoolSort())),
    ('E', ArraySort(IntSort(), ArraySort(IntSort(), BoolSort()))),
)
GraphSort = GraphSort.create()
V = GraphSort.V
E = GraphSort.E

G = Const('G', GraphSort)
n, m = Consts('n m', IntSort())
Graph_axioms = [
    ForAll([G, n, m], Implies(E(G)[n][m], And(V(G)[n], V(G)[m]))),
]

s = Solver()
s.add(Graph_axioms)

我正在尝试对图形进行建模，以V(G)[n]暗示节点的存在n并暗示从到E(G)[n][m]的边的存在。有人对这里出了什么问题有任何提示吗？或者更好的是，在 z3 中建模图形的任何一般技巧？nm

编辑：

通过alias给出的解释，我想出了以下稍微笨拙的解决方案：

from itertools import product
from z3 import *
import networkx as nx


GraphSort = Datatype('GraphSort')
GraphSort.declare('Graph',
    ('V', ArraySort(IntSort(), BoolSort())),
    ('E', ArraySort(IntSort(), ArraySort(IntSort(), BoolSort()))),
)
GraphSort = GraphSort.create()
V = GraphSort.V
E = GraphSort.E

class Graph(DatatypeRef):
    def __new__(cls, name):
        # Hijack z3 DatatypeRef instance
        inst = Const(name, GraphSort)
        inst.__class__ = Graph
        return inst

    def __init__(G, name):
        G.axioms = []
        n, m = Ints('n m')
        G.add(ForAll(
            [n, m],
            Implies(E(G)[n][m], And(V(G)[n], V(G)[m]))
        ))

    def add(G, *v):
        G.axioms.extend(v)

    def add_networkx(G, nx_graph):
        g = nx.convert_node_labels_to_integers(nx_graph)

        Vs = g.number_of_nodes()
        Es = g.number_of_edges()

        n = Int('n')
        G.add(ForAll(n, V(G)[n] == And(0 <= n, n < Vs)))
        G.add(*[E(G)[i][k] for i, k in g.edges()])
        G.add(Sum([
            If(E(G)[i][k], 1, 0) for i, k in product(range(Vs), range(Vs))
        ]) == Es)

    def assert_into(G, solver):
        for ax in G.axioms:
            solver.add(ax)


s = Solver()
G = Graph('G')
G.add_networkx(nx.petersen_graph())
G.assert_into(s)

标签： pythonz3z3py

解决方案

您的模型是unsat因为数据类型是自由生成的。这是一个常见的误解：当您创建数据类型并断言公理时，您并没有限制 z3 只考虑那些满足公理的模型。相反，您要说的是检查此数据类型的所有实例是否满足公理。这显然不是真的，因此unsat. 这类似于说：

a = Int("a")
s.add(ForAll([a], a > 0))

这也是unsat出于同样的原因；但希望更容易理解为什么。另请参阅此答案以了解“自由生成”的含义：https ://stackoverflow.com/a/60998125/936310

要对此类图进行建模，您应该只在图节点的各个实例上陈述这些公理，而不是概括/量化的公理。与其断言这个公理，不如关注你试图建模的其他方面。由于您没有真正向我们提供有关您要解决的问题的任何进一步细节，因此很难进一步发表意见。

推荐阅读