[comfypotato]

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]

Z3 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