4 ms·
But what do you mean “fast”? If your problem ends up on the steep side of the exponential curve, it’s going to take a while to solve. I had a lot of fun making
by comfypotato 3y ago
But what do you mean “fast”? If your problem ends up on the steep side of the exponential curve, it’s going to take a while to solve.
I had a lot of fun making my own CDCL solver in Rust, and I’ve really enjoyed messing with Z3 for some theoretical computer science. On all of my explorations, there was a very tangible problem size beyond which the solve time was unusable.
In the case of Z3 with most real world problems, the typical problem size is beyond this limit.
- xavxav 3y agoZ3 is actually not a particularly good SAT solver, you really want to use a dedicated tool for pure SAT problems. On the other hand if your problem is in a richer class like QBF or SMT then z3 shines and often you can use encoding tricks to scale problems significantly