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.
All posts by msoos
Texas Executed Offenders’ Last Words
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 released
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
Eight Pro Tips on Creating Better Software
I have been writing software for more than 20 years now. I thought it’s about time to gather my experiences and write some advice on building better software.
1. Solve the right problem
It is all too often that one tries solving something before understanding the problem at hand. We have a certain understanding of what the issue is, write something to solve it, but it turns out that we wrote the wrong solution because we misunderstood the problem. Do some research, read some articles, talk to people and read some books before attempting to solve a problem.
Continue reading Eight Pro Tips on Creating Better Software
Memory layout of clauses in MiniSat
I have been trying to debug why some MiniSat-based solvers perform better at unit propagation than CryptoMiniSat. It took me exactly 3 full days to find out and I’d like to share this tidbit of information with everyone, as I think it might be of interest and I hardly believe many understand it.
The mystery of the faster unit propagation was that I tried my best to make my solver behave exactly as MiniSat to debug the issue, but even though it was behaving almost identically, it was still slower. It made no sense and I had to dig deeper. You have to understand that both solvers use their own memory managers. In fact, CryptoMiniSat had a memory manager before MiniSat. Memory managers are used so that the clauses are put close to one another so there is a chance that they are in the same memory page, or even better, close enough for them not to waste memory in the cache. This means that a contiguous memory space is reserved where the clauses are placed.