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

Question

我正在尝试在 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] 暗示存在从 n 到 [= 的边16=]。有没有人对这里出了什么问题有任何提示？或者更好的是，关于在 z3 中建模图形的任何一般技巧？

编辑：

根据的解释，我想出了以下稍微hacky的解决方案：

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)

Answer 1

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

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

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

要为此类图建模，您应该只在图节点的各个实例上陈述这些公理，而不是 generalized/quantified 公理。不要断言这个公理，而是关注你试图建模的其他方面。由于您没有真正向我们提供有关您要解决的问题的更多详细信息，因此很难进一步发表意见。

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

z3 modeling graph with datatype of arrays

python

z3

z3py