Dreaming up a parallel SAT architecture
Parallel SAT solving is difficult for two main reasons: conflict clauses should be shared even though they are generated at an extreme pace, and secondly, creating a scalable architecture given the inherent algorithmic difficulties is hard. In this blogpost I share with you some of my thoughts about the architecture I thought up that could scale to large number of threads with relative ease, retaining some of the performance of single-threaded solvers.
Hyper-binary resolution: I was wrong, again
I am not perfect, so I make mistakes. One of the more memorable mistakes I have made has been regarding hyper-binary resolution. More specifically, in this post I wrote that I cannot add as many binary clauses using hyper-binary resolution as Armin Biere, one of the leading SAT solver experts, and I proposed a reason […]
Wasting cluster time
Today marked the 100th cluster experiment I have conducted on the Grid’5000 cluster in Grenoble. The computers in this cluster are very powerful beasts, equipped with two Xeon Core i7-based processors, each with 4 cores for 8 cores in total with some impressive memory size and connectivity. The sad part is that since CryptoMiniSat is […]
Documenting code is not always so much fun. However, in order for the code to be extended by others, documentation needs to exist. Since I conceived CryptoMiniSat as a program to be extended by others, documentation was a must. So now, after investing about 2 weeks into documentation, it is finally ready. All major classes […]