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.

[miladrabi]

Thank you for the response. The reason I asked this is that we have written the exact same pipeline in Python and with consecutive runs, we get the same output. This could also be interpreted as an issue because if the generated SMT-LIB file is suboptimal in terms of solver performance, the solve time won't change. we are particularly interested in this behavior because we are creating a benchmark and this gives us a huge time range in terms of performance. I'll investigate our pipeline in more details to see if we can fix this issue.

[toolCHAINZ]

Would you be able to share an example of your python source? Like @Pat-Lafon said, this should be completely independent of Z3.rs, which is just a thin API over the same C API that Python uses.

Without knowing more, my best guess as to what's going on here is that your python code is linked against a different version of Z3 than your rust code is (the python bindings distribute their own z3 shared object in the wheel) and that that's where the difference is.

You're exporting SMTLIB from both and evaluating that, correct? Could you share which python api you're using to get the SMTLIB and which you're using in Rust? That could maybe also account for the difference if the benchmark creation is being done differently.

[miladrabi]

Yes I can definitely provide an example. But let me know which part are you interested in, because we have an environment on top of Z3.rs where variables and other informations (system transitions) can be registered and this environment then uses this information to generate the final encoding.

In our environment we are also using Rust's standard hash map std::collections::HashMap and this structure doesn't preserve the order. However, Python uses a different implementation for their hash maps (dict) which preserves the order of insertion on iterations (as explained here in the Background). I believe this is why we don't have the same issue with the Python's implementation, as the order of retrieving information is always the same.

Yes, we export the SMT-LIB from both and use the native z3 executable on our system to obtain statistics. However, this is only for debugging purposes. We are using the official API in here and installed it using the pip install z3-solver command. The Python version is 3.13.3.

Actually, the encoding generated in the Python version is larger than the one created by Z3.rs (~17000 lines vs ~10000 in SMT file), which is a good sign in our case, since it helps solve time substantially if the ordering is (near-)optimal.

[Pat-Lafon]

Yeah, an unordered map would make a lot of sense as the issue.

I'm not totally sure why the encoding generated would be of different sizes unless the python wrapper is doing more work behind the scene. I would assume that is again a difference in your implementation but could totally be wrong on that.

I would be careful saying stuff like "ordering is (near-)optimal". You may be able to find an ordering that works well for one particular instance of your problem(such as for this specific smtlib file you are looking at) but you will have no guarantee that such an ordering performs well even under slight perturbation. SMT solvers are truly fickle beasts.

Sadly I'm not sure there are great solutions for this(unless you have a nicer way to split up, simplify or change the encoding of the problem). Sometimes people create "portfolios" of solvers which you run in parallel with either different settings or different orderings/mutations to their query. Then you just take the result of the first solver that gets back to you if all you care about is wall-clock time.

I sometimes use https://github.com/viperproject/smt-scope to get a better understanding of why the solver may be taking a long time. It doesn't always help but it's sometimes more useful in debugging solver performance.

[miladrabi]

Thank you for the suggested repo. I'll look into it. Your suggestions, especially the CMU blog, were really helpful.

[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.