3 ms·
Yes. It turns out that squeezing more performance out _purely_ from the silicon has been mostly due to: (1) hand-rolled memory layouts that optimize placement,
by zero_k 6y ago
Yes. It turns out that squeezing more performance out _purely_ from the silicon has been mostly due to: (1) hand-rolled memory layouts that optimize placement, do bit-stuffing and the like to take the most advantage of the cache, (2) using clever data structures that cache certain elements of the pointed-to data in the data we read linearly, thereby allowing the cache to pre-fetch them and allow us not to (always) dereference the pointer, (3) prefetching.
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-minisat/ https://www.msoos.org/2016/03/memory-layout-of-clauses-in-mi...
- josalhor 6y agoThanks for that resource, that is really interesting! 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.