Yes, of course there's some variance to be expected, but typically I've seen a fairly constant rate of results generation. The "proving completion" effect at the end of a calculation is very startling and easy to notice because the time lag can be orders of magnitude larger than anything else seen in the computation thus far. An annoying drawback of trying to use this method for larger searches...

I think this is just a property of DPLL. Just because it found one solution quickly, doesn't mean that it will find the next one quickly because it may have to do significant backtracking. It probably depends a lot on your usage though.

Thanks for sharing! Looks very nice and performant! I was wondering: how do these SAT solvers work under-the-hood? Is this also not similar to some recursive backtracking algorithm? Or do these fundamentally work differently? by leveraging some matrix algebra or polynomial solving or …?

Btw: The images show up a bit strange on this website:

but they show up fine on your own website.

I see, that's what I thought. I was actually thinking of doing the branching also a bit smarter; basically rank the cells by their 'influence/importance' such that the pruning is faster. But it can't beat any compiled sat solver likely :-)