采用数组数据类型的Z3建模图 [英] z3 modeling graph with datatype of arrays

问题描述

我试图在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到m的边的存在。有没有人对这里出了什么问题有什么建议？或者更好的是，有什么在Z3中建模的通用提示吗？

编辑：

按照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)

推荐答案

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

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

这也是unsat的原因；但希望更容易看出原因。另请参阅此答案，了解免费生成的https://stackoverflow.com/a/60998125/936310

的含义

要为这样的图建模，您应该只在图的节点的单个实例上声明这些公理，而不是泛化/量化公理。与其断言这一公理，不如专注于你试图建模的其他方面。由于您并未就您想要解决的问题向我们提供任何进一步的细节，因此很难再给出进一步的意见。

这篇关于采用数组数据类型的Z3建模图的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！