Tag: Parallel SAT Solving
-
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.
-
On the New Watchlist Scheme
All right, so I am not so cool because I work on weekends, but I got this new watchlist scheme implemented. First off, let me say it was relatively easy to implement, which is a testament to the extensibility of CryptoMiniSat: it only took me ~4 hours to get it done. Secondly, I realised that […]
-
Changing the Watchlist Scheme
Okay, what if we changed the watchlist scheme… a bit? The way the watchlist scheme operates in SAT solvers is the following. We have a set of literals lit1, lit2, lit3, lit4 that defines the clause we want to be watched for propagation and conflict. We take two literals from this set of literals, and […]