Has there been a study of the bottleneck of the performance of modern sat solvers? Some modern x86 CPUs have enormous cache sizes.
Note that (1) and (2) are much more important than (3). In particular, you can even arrange the data elements for (1) in an order that you _expect_ them to be dereferenced, and even if your "hit" ratio is only slightly better than zero, you can get a performance improvement. For this latter one, check out https://www.msoos.org/2016/03/memory-layout-of-clauses-in-mi...
Although I'm quite new to the SAT field I have to say I am quite impressed with the performance of cutting edge sat solvers. Looking at the source of some of them (like Glucose) I don’t see that much low-level trickery. I wonder how much down the stack one could go to try to get more out of their processors.