Things are heating up for the SAT competition 2016. I will of course compete. However, I would publicly like to ask the organisers to please for the love of whatever you believe in, please randomise the benchmarks. Just a tiny, little bit. It’s ridiculous that people are tuning their solvers so they can solve some randomly solveable instance like the vmpc* series. It’s laughable and it’s making the whole community look bad. Really, it’s time to stop this madness. I wrote that article with a bunch of ideas in 2013. It’s time. Not even the largest of organisations move this slowly, and this is a research group of about 50 people max.

Nobody on the face of the Earth will believe that if you swap the first 2 clauses of a CNF instance that typically contains at least 100 thousand clauses, you have somehow substantially altered the problem. Please, it’s crazy what is going on. I don’t care what method you choose. Swap the literals, swap the clauses, rename some variables, propagate some of them (really, all sane solvers propagate variables, I cannot possibly see how that could in any way change the results). You are a creative crowd, I’m sure you’ll find a way that even the most nit-picking industry expert (and there are not too many of those, let’s be honest) can show that it makes a difference. It’s time to take our heads out of the sand and fix things up.

Thank you.