Just a short note: this Easter holiday I got a bit bored and did a mini-threading system for CryptoMiniSatv4. It will now be able to compete in the multi-threading track after quite a number of years of absence. Last time I did this, CryptoMiniSat won the UNSAT multi-threaded track, which was a bit funny because all I shared were unitary and binary clauses. For the simplicity and the fun, I’m doing the same this time around. Let’s hope all the super-complicated and extra-theoretical stuff will get won over.

Non-blocking datastructs

Some authors implement a non-blocking data-sharing construct to gain more performance out of the system. I think/hope that what is shared is more important than how. I use one global lock for the shared unit and one for the shared binary clauses. Since there won’t be more than 8 threads under normal circumstances and I have to lock about once per 10sec per thread for about 0.01s, there won’t be any contention. Under these circumstances, simplicity wins over the complexity of using non-locking datastructures. Also, these fancy datastructs probably don’t have an implementation that is C++11 (i.e. portable) and is already implemented in gcc 4.7.1 (which doesn’t support a number of the threading constructs), the compiler used in the competition.

Library usage

This time around I didn’t mess it up: multi-threading can be used from the library interface. The system completely hides the fact that multiple threads are competing in the background to solve the problem. The threads are cleanly and safely stopped and then re-started when the user asks for another solve() operation, optionally with assumptions. In other words, the user doesn’t see and doesn’t have to bother with the complexity of threads. All of that is abstracted away behind a neat and clean API. This means that e.g. the different threads can have radically different variable numbers. They could have renumbered the variables differently, added new and different BVA variables, etc. All of this is hidden away and the user is presented with and always communicates using his/her own variable numbers.

Final notes

This simple multi-threading system means that I can now port my old MPI code to use the new CryptoMiniSat. Maybe, once again, CryptoMiniSat will run on a cluster. Fun times ahead!