[Question] Is it possible to add randomness to generated solutions?

[jonathan-dilorenzo]

Currently (at least in my use of Z3), if I pass Z3 the same formula, it will generate the same solution deterministically every time, which is generally great.

However, I have a use-case (as part of a Fuzzer) where it would be amazing if I could somehow tell Z3 to randomize the solutions more (ideally w.r.t. a seed). Is there any setting that allows for this or do I need to perturb the formula externally to achieve my goal?

[NikolajBjorner]

use options smt.random_seed=NNN and sat.random_seed=NNN to ensure either SMT or SAT core uses randomization.

[jonathan-dilorenzo]

Amazing! Thanks Nikolaj! We'll give it a shot.

[verios-google]

@NikolajBjorner, we gave it a shot and it appears that the solver produces the same result after several iterations.

For more context, our constraint is on an IPv4 address. The constraints are:
- address value >= 224.0.0.0
- address value <= 239.255.255.255
Values are treated as numerical

The solver keeps producing 224.0.0.0, even after changing the seed repeatedly. That is a valid solutions, was just hoping to generate other valid solutions as well

Why does this happen? Is the constraint just too simple that randomness does not impact the result?

[verios-google]

@NikolajBjorner any follow up?

[NikolajBjorner]

from z3 import *

ip = BitVec("ip", 32)

set_param("sat.phase", "random")
count = 0
while True:
    count += 1
    set_param("sat.random_seed", count)
    s = Solver()
    s.add(ULE(0 + 256*(0 + 256*(0 + 256*224)), ip))
    s.add(ULE(ip, ((255*256 + 255)*256 + 255)*256 + 239))
    print(s.check())
    print(s.model())