Z3-Solver 的“TransitiveClosure”功能是否有 bug？

Question

这是使用

TransitiveClosure

的简单示例的代码。

from z3 import *

def compute_transitive_closure(graph):
    num_nodes = len(graph)

    # Create a Z3 context
    ctx = Context()

    # Create a Z3 solver
    s = Solver(ctx=ctx)

    # Define a function to represent the adjacency relation
    adj = Function('adj', IntSort(ctx), IntSort(ctx), BoolSort(ctx))

    # Add edges to the adjacency relation based on the graph
    for i in range(num_nodes):
        for j in range(num_nodes):
            if graph[i][j] == 1:
                s.add(adj(i, j))
            else:
                s.add(Not(adj(i, j)))

    # Define the transitive closure of the adjacency relation
    tc = TransitiveClosure(adj)

    # Define a Z3 array to represent the transitive closure matrix
    closure_matrix = [[Bool(f'tc_{i}_{j}', ctx=ctx) for j in range(num_nodes)] for i in range(num_nodes)]

    # Add constraints for the transitive closure matrix
    for i in range(num_nodes):
        for j in range(num_nodes):
            s.add(closure_matrix[i][j] == tc(i, j))

    # Solve the model
    if s.check() == sat:
        m = s.model()
        result = []
        for i in range(num_nodes):
            row = []
            for j in range(num_nodes):
                # Use is_true() to convert symbolic expressions to concrete booleans
                row.append(1 if is_true(m.evaluate(closure_matrix[i][j])) else 0)
            result.append(row)
        return result
    else:
        return None

# Example graph adjacency matrix
graph = [
    [0, 1, 0, 0],
    [0, 0, 1, 0],
    [0, 0, 0, 1],
    [0, 0, 0, 0]
]

# Compute the transitive closure
closure = compute_transitive_closure(graph)

# Print the transitive closure
if closure:
    print("Transitive Closure:")
    for row in closure:
        print(row)
else:
    print("No solution found.")

我期望输出一个矩阵，指示任意两个节点之间存在路径。但是，我得到一个全零的矩阵。 Z3有bug吗？还是我做错了什么？

Answer 1

这里的行为确实令人困惑，我没有一个好的答案给你。但有几点观察：

1. 当您在整数上定义

   adj

   并断言矩阵的条目时，您将保留其他所有内容。也就是说，求解器可以自由选择

   adj(200, -533)

   是什么。因此，这可能会影响您获得的结果。

2. 当你这样做

   is_true(m.evaluate(closure_matrix[i][j]))

   时，你总会得到

   False

   。您可以通过在代码中添加

   print(m.evaluate(closure_matrix[i][j]))

   来检查这一点：您会看到它打印了明显的术语，即评估实际上并未发生。

这是一个错误吗？我不确定..我会尝试一些事情：

1. 不要使用整数，而是使用枚举排序或未解释的排序。 （您可能想从仅支持固定大小矩阵的实现开始。）

2. 添加一个量化公理，表示如果索引“越界”，则

   adj(i, j)

   为假。

3. 而不是

   evaluate

   ，您可能想要

   push

   ，断言

   Not(tc(i, j))

   ，如果结果是

   unsat

   ，则推断

   tc(i, j)

   一定是

   1

   。您弹出该断言，然后继续其余部分。

我自己尝试了一下，但我无法让 z3 可靠地解决这个问题。一旦您尝试了这些想法，您应该在 z3 的问题跟踪器上报告您的发现，以便开发人员可以提出意见。另外，请告诉我们您发现了什么！