Parallel in z3 to speed up?

[XiangyuG]

Hi,

I am solving a complex SAT problem (NOT Optimize) using z3 and want to leverage multiple cores to speed up the solving process. The way I do this is to add this line of code set_param("parallel.enable", True) to enable parallelism. However, it seems that this does not provide any help. I want to ask whether this way to call the parallel mode is correct or not. Do you have any other suggestions for me to leverage multiple cores to speed this up?

As a motivating example, it takes me around 1.5 mins to get the output result for the following program (parallel.py) by running the command (time python3 parallel.py) using one core. People might need to install the z3 package in python through pip before running it.

from z3 import *

def long_running_z3_example():
    # Number of variables
    num_vars = 600  # Increase for longer runtime
    variables = [BitVec(f'v{i}', 32) for i in range(num_vars)]

    # Constraints
    constraints = []
    for i in range(num_vars - 1):
        # Create flexible XOR constraints
        constraints.append(Or(variables[i] ^ variables[i + 1] == 123456789, 
                              variables[i] ^ variables[i + 1] == 987654321))

    # Add a range constraint for each variable to avoid too-tight constraints
    for v in variables:
        constraints.append(And(v >= 100000, v <= 2000000000))

    # Add a less restrictive combined constraint
    combined = variables[0]
    for i in range(1, num_vars):
        combined = combined ^ variables[i]
    constraints.append(combined >= 5000000)  # Looser constraint to ensure satisfiability

    # Solver setup
    solver = Solver()
    solver.add(constraints)
    # Enable parallel mode and set the number of threads
    set_param("parallel.enable", True)
    # set_param("parallel.threads", 4)  # Adjust this number based on your CPU cores

    # Check satisfiability
    print("Solving...")
    result = solver.check()
    if result == sat:
        model = solver.model()
        print("Model:")
        for v in variables[:10]:  # Print the first 10 variables for brevity
            print(f"{v} = {model[v]}")
    elif result == unsat:
        print("Unsatisfiable!")
    else:
        print("Unknown result.")

if __name__ == "__main__":
    long_running_z3_example()

Thanks a lot for any feedback in advance.

[NikolajBjorner]

There isn't much in support of xor constraints (also not for bit-vectors).

[XiangyuG]

Thanks for your reply. Does it mean z3 cannot support parallelism for bit-vectors and some relatively advanced operations (e.g., bitwise or, bitwise and, bitwise xor)?