MapleCOMSPS taking the cake

I’ve been reading through the source code of the 2016 SAT Competition winner, MapleCOMSPS_DRUP, and this piece of beauty hit me:

Goodbye reproducibility. If you are unfamiliar with SAT solvers, they are notoriously difficult to understand and debug because their behaviour is randomised by the heuristic algorithmic choices which are influenced by essentially every solving parameter and every line of the input. But, at least with the same parameters and the same input file, they run the same exact way. Not this solver. The winning solver. This makes it incredibly hard to publish any results with it — I can simply claim my instance got solved and if it doesn’t get solved by anybody else, bad luck, the timing for that alert() must have been off! Better luck next time.

Usability issues

I am wondering where the SAT community is headed with a non-deterministic solver winning the competition. Is this really where we ought to be going? Which industrial system designer in their right mind would choose to use this solver? How would they debug their system? Note that this means that in case there are multiple solutions, the solver will, with high probability, return different solutions on different runs, with different running times. Imagine you needing to debug a million-line codebase and not having any idea why the bug is non-reproducible. After a day of tearing my hair out and realising that the underlying SAT solver is non-deterministic, I’d be ready to use absolutely anything but.


I thought there was a requirement that the solving must be reproducible? There was such a requirement at one point, I think. If not, maybe it’d be a good idea to add it. Microsoft spent a non-negligible amount of time and effort to make parallel SAT solving reproducible. Imagine the pressure they must have had from their industrial use-cases if they made that reproducible. Would Intel use a non-deterministic SAT solver? Would a start-up? Would IBM? Would you?