CODEWITHSUNDEEP
z3z3pyconstraint-programmingoperations-researchtransitive-closure
Sai Kiran
Sai Kiran

Reputation: 1

Is there a bug in the "TransitiveClosure" function of Z3-Solver?

Here's the code of a simple example using 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.")

I'm expecting as output a matrix indicating the existence of a path b/w any two nodes. However, I'm getting a matrix with all zeros. Is there a bug in Z3? Or did I do something wrong?

Upvotes: 0

Views: 59

Answers (1)

alias
alias

Reputation: 30418

The behavior here is really confusing, and I don't have a good answer for you. But a couple of observations:

  1. When you define adj over integers and assert the entries for the matrix, you're leaving everything else open. That is, the solver is free to pick what adj(200, 0) is, for instance. So, that can impact the results you're getting.

  2. When you do is_true(m.evaluate(closure_matrix[i][j])) you'll always get False. You can check this by adding print(m.evaluate(closure_matrix[i][j])) to your code: You'll see that it prints the obvious term for it, i.e., evaluation doesn't actually happen.

Is this a bug? I'm not sure.. I'd experiment with a few things:

  1. Instead of using integers, use an enumerated-sort, or an uninterpreted sort. (You might want to start with an implementation that only supports a fixed size matrix.)

  2. Add a quantified axiom that says if the indices are "out-of-bounds" then adj(i, j) is false.

  3. Instead of evaluate, you might want to push, assert Not(tc(i, j)) and if the result is unsat, deduce that tc(i, j) must be 1. You pop that assertion, and continue with the rest.

I experimented with these myself a bit, but I couldn't get z3 to reliably address this problem. Once you experiment with these ideas, you should report your findings at z3's issue tracker so the developers can opine. Also, let us know what you find out!

Upvotes: 0

Related Questions