Nondeterministic SMT-LIB Output

[miladrabi]

Hi,
After building my complete formula in Rust, I’ve noticed that solve times vary drastically from around 0.3 s up to 78 s. That led me to dump the SMT‑LIB encoding with solver.to_smt2(), and I discovered that each run emits the exact same constraints and declarations, just in a different order. I’m beginning to suspect that this reordering sometimes helps the solve time and sometimes hurts it. Is there a way to disable this behavior so I get the identical output every time?

[Pat-Lafon]

Not just order the order of constraints. Changing variable names, performing simple transformations like a+b -> b+a, using different solver versions or supposedly even changes in whitespace can cause the solver to behave differently. https://www.cs.cmu.edu/~csd-phd-blog/2024/mariposa/ This blog post and corresponding paper talk a little about this but there is a lot of lore I think.

Some of the reordering comes from non-determinism in the solver itself perhaps? There are very few guarantees one can give unfortunately, though I haven't seen that as much myself. Any chance it is non-determinism on your side which would be the easiest thing one could fix?

If you are serious about this, the cvc5 people have a preprocessing normalization step you can run on your smt lib file. It will make the file completely unreadable, but it should help with getting a more consistent smtlib file. Note that this doesn't mean your queries will perform faster. It could easily normalize to the 78 second case. https://arxiv.org/abs/2410.22419

Alternatively, there may be certain features of your query that make it more fragile. Investigating different encodings or shrinking the query may help but that's a bit of an art.

[Pat-Lafon]

This is more of a discussion post than an issue imo. There really isn't anything the rust bindings can do about this.