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

 

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.

Continue reading Memory layout of clauses in MiniSat

Benchmark randomisation for SAT Comp’16

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.

Continue reading Benchmark randomisation for SAT Comp’16