[zero_k]

For smaller problems, the fancier solvers are actually worse than MiniSat/Picosat. That's because of the overhead of creating and maintaining datastructures and the fancy preprocessing. The larger, more complex solvers are meant to have a better chance to solve more complex problems and will use hybrid strategies to make sure they don't accidentally go down into some rabbit hole. So I would expect them to have better consistency.

Note that winning in the competition, until 2017, meant you solved the most instances, each with a ~5000s timeout. So if you solved every single one within 4999s you won, you were the best... This obviously encouraged incredibly long startup times that are gained back over the overall 5000s timeout. It clearly does not mimic normal use-cases.

[keenerd]

Thanks. That makes sense. Most of my stuff has (at most) a few million clauses and usually takes between 1-600 seconds.