3 ms·
Z3 is such a brilliant piece of software - we've been using it for some small scheduling problems - such a godsend.
by shriphani 8y ago
Z3 is such a brilliant piece of software - we've been using it for some small scheduling problems - such a godsend.
- vitaminCPP 8y agoWhat's the difference between using the Z3 library and using [sympy](www.sympy.org) a symbolic solving library?
- jahewson 8y agoSymPy is somewhat like Mathematica where it presents a wrapper around lots of underlying solvers. Z3 is one particular solver for a category of problems.
- whazor 8y agoZ3 opt is like magic
- amelius 8y agoI imagine that for complicated inputs, the solver will just "hang". Is this an issue in practice? Can you bound its runtime?
- shriphani 8y agohmm so Z3 has a timeout option you can set. In our experience we haven't really seen it hang or do anything out of the ordinary - unsat problems on average seem to take longer than sat problems (it probably needs to scan a lot more). We've pushed it to about a million variables or so and it has handled it well thought we might only be a the lower end of workloads.