Reset solver state but keep constraints

[egolf-cs]

If I query the solver for a model x, add a constraint forbidding x, and then ask for a new model y I’m finding that x and y are “close” to one another. Is this because the solver is reusing work it did when it found x? How can I stop this from happening? Ideally, I’d like y to be a random satisfying assignment, completely independent of x. Thanks!

[NikolajBjorner]

Here is a short discussion around controlling model outputs: https://z3prover.github.io/papers/z3internals.html#sec-there-are-no-deep-knobs-to-control-model-values

[egolf-cs]

Thank you for the quick reply! My constraints are quantifier free formulas over only boolean variables, so I think that

Ensuring diverse model values for Booleans is partially possible by controlling options on the SAT solver

this sentence might be applicable. Do you have advice on which options I should be controlling so that x and y are different?

[NikolajBjorner]

https://www.msoos.org/2021/09/cmsgen-a-fast-uniform-like-sampler/
and papers by Meel group.