Question about Z3's Parallel Mode Trigger Conditions for Floating-Point Problems

[Lqs66]

When using the Z3 solver, I've noticed that despite enabling parallel mode (set_param("parallel.enable", True)), the actual solving process doesn't seem to fully utilize multi-threading. I've observed only one thread being active, while others remain idle.

I've consulted the Z3 documentation, including parallel, which describes parallel processing. The documentation states that parallel mode affects tactics like qfbv that use the SAT solver for sub-goals, introducing a "cube-and-conquer" approach.

My code deals with two independent floating-point expressions, p1(x) and p2(y), connected by an AND operation: p1 > 0.5 && p2 < 0.2. Intuitively, this could be seen as two independent sub-problems that could potentially be solved in parallel. However, even with the parallel parameter set, I haven't observed multi-threading activity during execution.

Here's the code I'm using:

from z3 import *

set_param("parallel.enable", True)

# 1. Use BitVec to represent the underlying bit pattern, then convert back to Double with fpBVToFP
x_bv = BitVec('x_bv', 64)
y_bv = BitVec('y_bv', 64)

# 2. Rounding mode
rm = RNE()

# 3. Convert to FP variables
x = fpBVToFP(x_bv, Float64())
y = fpBVToFP(y_bv, Float64())

# 4. Helper for constructing Double constants
def D(v):
    return FPVal(v, Float64())

# 5. Compute the polynomial p(x) = x - x^3/6 + x^5/120
# First construct x^2, x^3, x^4, x^5
x2 = fpMul(rm, x, x)
x3 = fpMul(rm, x2, x)
x4 = fpMul(rm, x2, x2)
x5 = fpMul(rm, x4, x)
p1 = fpAdd(rm,
    fpSub(rm,
      x,
      fpDiv(rm, x3, D(6.0))
    ),
    fpDiv(rm, x5, D(120.0))
)

# Similarly for p2
y2 = fpMul(rm, y, y)
y3 = fpMul(rm, y2, y)
y4 = fpMul(rm, y2, y2)
y5 = fpMul(rm, y4, y)
p2 = fpAdd(rm,
    fpSub(rm,
      y,
      fpDiv(rm, y3, D(6.0))
    ),
    fpDiv(rm, y5, D(120.0))
)

# 6. Add constraints: p1 > 0.5  &&  p2 < 0.2
s = Solver()
s.add(fpGT(p1, D(0.5)))
s.add(fpLT(p2, D(0.2)))

if s.check() == sat:
    m = s.model()
    # Directly extract BitVec and FP values from the model (without converting FP values using float())
    xv = m[x_bv].as_long()
    yv = m[y_bv].as_long()
    x_fp = m.evaluate(x)
    y_fp = m.evaluate(y)
    print("BitVector method solution: \nx_bv =", hex(xv),
          "\ny_bv =", hex(yv),
          "\nx_fp =", x_fp,
          "\ny_fp =", y_fp)
else:
    print("unsat")

1. Under what specific conditions does Z3's parallel.enable parameter actually trigger parallel processing?

2. For this type of floating-point constraint with seemingly independent sub-problems, does Z3 consider it a suitable scenario for parallel solving? If so, why am I not observing multi-threading activity with my code?

3. Are there specific tactics or parameter configurations I need to explicitly use or adjust to ensure full utilization of Z3's parallel capabilities in this kind of floating-point problem?

[NikolajBjorner]

It builds a search tree. THe root of the tree is sequential. So if all time is spent at the root there is no parallel effect.
You can also try to smt.threads, sat.threads respectively, option, which runs multiple concurrent cores.
Z3 does not detect indepedendent sub-problems
You can also enable parallel tactics https://microsoft.github.io/z3guide/docs/strategies/summary