I’ve been reading through the source code of the 2016 SAT Competition Main Track winner, MapleCOMSPS_DRUP, and I found that it has an important piece of code, regulating its behaviour that depends on timing:
static bool switch_mode = false;
static void SIGALRM_switch(int signum) { switch_mode = true; }
lbool Solver::solve_()
{
signal(SIGALRM, SIGALRM_switch);
alarm(2500);
I read this paper about most research findings being false. Given that most research papers in SAT take a sample size that is incredibly small (especially considering that it’s cheap to have large sample sizes relative to, e.g. medical trials), and the samples are very often hand-picked, it’s easy to see why this could be the case. But that article lists a number of other factors, too, and they are interesting to consider as well. Only few true innovations stick around in SAT (glues, VSIDS, UIP, restarts, etc). Most are forgotten because, frankly, they didn’t show the promise they purported to have. It’d be interesting to force authors to e.g. run their systems on much larger sample sizes (e.g. 2-3000 instances from SAT competitions) with much longer timeouts (e.g. 5000s). Then those implementing SAT solvers wouldn’t have to wade through piles of articles to get to something worth implementing. One is allowed to dream.
A new version of CryptoMiniSat, 5.0.1 has been released. It is essentially only a release to mark the move to a much more permissive, MIT license. I am changing the license so that everyone can use the system as they wish, however they wish. I want to give back to the community I have been part of for so long, and so I am making this change. Thank you all for using the solver, it makes me happy that I have been able to help some with my hobby work.
An artist friend of mine gave me this idea, so here is the list of the most used words of those executed in Texas, from their last statement:
word frequency
-----------------------
you 4.670330
and 3.945360
the 3.670635
for 2.701465
love 2.419109 **
that 2.190171
all 2.113858
have 1.663614
this 1.297314
thank 1.030220 **
know 1.014957
family 0.969170 **
your 0.908120
not 0.839438
will 0.808913
god 0.801282 **
want 0.801282
would 0.778388
with 0.755495
i'm 0.755495
sorry 0.747863 **
like 0.740232
say 0.679182
but 0.641026
life 0.595238 **
what 0.579976
there 0.549451
ya'll 0.534188
hope 0.488400 **
them 0.488400
CryptoMiniSat 5.0.0, after winning the incremental track at SAT Competition 2016 and getting 3rd place at the parallel track, has been released. The new solver contains a number of important additions. The most important are that the solver can now be used as a preprocessor and Gauss-Jordan Elimination is back.
Continue reading CryptoMiniSat 5.0.0 released