Z3-Solver的TransitiveClosure函数存在Bug吗？我的代码为何返回全零矩阵？

我编写了一段使用Z3-Solver中TransitiveClosure函数计算图传递闭包的Python代码，预期输出能指示任意两节点间路径存在性的矩阵，但实际得到全零矩阵。请问是Z3存在Bug，还是我的代码有误？

代码如下：

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，而是代码对TransitiveClosure的使用逻辑有误。核心问题在于额外定义了closure_matrix布尔变量并将其与tc(i,j)绑定，但Z3的模型不会自动为这些中间变量推导传递闭包的真值。正确的做法是直接通过模型评估tc(i,j)的结果，不需要中间变量。

修正后的代码 #

from z3 import *

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

    ctx = Context()
    s = Solver(ctx=ctx)

    # 定义邻接关系函数
    adj = Function('adj', IntSort(ctx), IntSort(ctx), BoolSort(ctx))

    # 添加图的边约束
    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)))

    # 计算传递闭包
    tc = TransitiveClosure(adj)

    if s.check() == sat:
        m = s.model()
        result = []
        for i in range(num_nodes):
            row = []
            for j in range(num_nodes):
                # 直接评估tc(i,j)的真值
                row.append(1 if is_true(m.evaluate(tc(i, j), model_completion=True)) else 0)
            result.append(row)
        return result
    else:
        return None

# 示例图
graph = [
    [0, 1, 0, 0],
    [0, 0, 1, 0],
    [0, 0, 0, 1],
    [0, 0, 0, 0]
]

closure = compute_transitive_closure(graph)

if closure:
    print("传递闭包矩阵:")
    for row in closure:
        print(row)
else:
    print("未找到可行解。")

关键修正点 #

1. 移除了closure_matrix的定义，直接在模型中评估tc(i,j)的结果，避免中间变量导致的真值推导问题。
2. 在m.evaluate中添加了model_completion=True参数，确保Z3为所有未显式约束的tc(i,j)实例生成符合传递闭包性质的真值。

运行修正后的代码，会得到预期的传递闭包矩阵：

传递闭包矩阵:
[0, 1, 1, 1]
[0, 0, 1, 1]
[0, 0, 0, 1]
[0, 0, 0, 0]

内容的提问来源于stack exchange，提问作者Sai Kiran