6 ms·

Hah, funny to see my blog referenced. Yeah, cache misses are a huge part of SAT solving (modern solvers have prefetch code specifically for this loop, some seem

by zero_k 6y ago

Hah, funny to see my blog referenced. Yeah, cache misses are a huge part of SAT solving (modern solvers have prefetch code specifically for this loop, some seemingly following the code I wrote). And SAT solving is about 95+% of SMT solving. So, yeah, cache is where it's at. I once had an old, but "enthusiast" i7 that had a 3-lane mem setup, and "upgraded" to a consumer dual-lane i7 that was 2-3 gens ahead. It had the same performance(!) for SAT solving. Was pretty eye-opening.

HALtheWise 6y ago
At the end of the day, cache miss latency should be bounded by the speed of light and the distance to memory. It's entirely unsurprising to me that by putting main memory on the same board as the CPU, as well as the optimizations that come from allowing a custom communication protocol between them, better performance is possible. I wonder what a desktop machine designed for cache and memory latency would look like.
- janekm 6y ago
  Not just same board... the RAM is literally stacked right on top of the SoC. It’ll be interesting to see what Apple will do on desktop... maybe some stacked RAM plus more on the board? Having full control over memory / bus architecture (and the OS) creates lots of opportunities for optimization.
- vvanders 6y ago
  It's SRAM vs DRAM not the speed of light. Go take a look a DRAM CAS values as clock speeds have increased. The ns/fetch has stayed pretty static(~10ns) since DDR first showed up. There's been slight improvements but nothing like the order of magnitudes you seen in other areas. If you want to pay the power and cost of SRAM it can be done but it doesn't usually pencil out beyond what you see in caches today.
josalhor 6y ago
Has there been a study of the bottleneck of the performance of modern sat solvers? Some modern x86 CPUs have enormous cache sizes.
- 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 ago
    Thanks 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.
dtech 6y ago
Which 3 gens? Intel CPU performance has been flat-ish for 5 years or so, so that might not be super-suprising
- williadc 6y ago
  The only 3 Lane i7 I know of is the Nehalem
OxO4 6y ago
> SAT solving is about 95+% of SMT solving This is theory-dependent, I would say. It is certainly true for bit-vector solvers that bit-blast for example. For other theories, however, this is not necessarily the case. Consider a simplex-based linear integer arithmetic solver for example. If there is a problem that is simple at the Boolean level, you may end up spending more time in the simplex solver.
- zero_k 6y ago
  Ah, good point. Still, the most used theories are mostly SAT-bound. BV (bitvector) especially. And the translation to SAT can play a huge part, so even in BV logics, the SMT solver's abilities are super-important. But runtime in these logics are dominated by the SAT solver. I should play with more SMT solvers. I work on the STP SMT solver along with a team of very dedicated people (https://github.com/stp/stp/ https://github.com/stp/stp/), it's QF_BV (Quantifier Free BV) solver and it tends to do well in the competitions: https://smt-comp.github.io/2020/results.html https://smt-comp.github.io/2020/results.html So I'm probably a bit biased towards BV. For counting (e.g. https://github.com/meelgroup/approxmc https://github.com/meelgroup/approxmc) and sampling (e.g. https://github.com/meelgroup/unigen https://github.com/meelgroup/unigen) it's also 99% SAT solver runtime.
zitterbewegung 6y ago
To be honest can you redo it when the a14 chips come out in a device?
rurban 6y ago
So getting rid of ptrs and using roaring bitmap indices would make them fly.

by zero_k 6y ago

HALtheWise 6y ago

At the end of the day, cache miss latency should be bounded by the speed of light and the distance to memory. It's entirely unsurprising to me that by putting main memory on the same board as the CPU, as well as the optimizations that come from allowing a custom communication protocol between them, better performance is possible. I wonder what a desktop machine designed for cache and memory latency would look like.

janekm 6y ago
Not just same board... the RAM is literally stacked right on top of the SoC. It’ll be interesting to see what Apple will do on desktop... maybe some stacked RAM plus more on the board? Having full control over memory / bus architecture (and the OS) creates lots of opportunities for optimization.
vvanders 6y ago
It's SRAM vs DRAM not the speed of light. Go take a look a DRAM CAS values as clock speeds have increased. The ns/fetch has stayed pretty static(~10ns) since DDR first showed up. There's been slight improvements but nothing like the order of magnitudes you seen in other areas. If you want to pay the power and cost of SRAM it can be done but it doesn't usually pencil out beyond what you see in caches today.

josalhor 6y ago

Has there been a study of the bottleneck of the performance of modern sat solvers? Some modern x86 CPUs have enormous cache sizes.

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 ago
  Thanks 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.

dtech 6y ago

Which 3 gens? Intel CPU performance has been flat-ish for 5 years or so, so that might not be super-suprising

williadc 6y ago
The only 3 Lane i7 I know of is the Nehalem

OxO4 6y ago

> SAT solving is about 95+% of SMT solving This is theory-dependent, I would say. It is certainly true for bit-vector solvers that bit-blast for example. For other theories, however, this is not necessarily the case. Consider a simplex-based linear integer arithmetic solver for example. If there is a problem that is simple at the Boolean level, you may end up spending more time in the simplex solver.

zero_k 6y ago
Ah, good point. Still, the most used theories are mostly SAT-bound. BV (bitvector) especially. And the translation to SAT can play a huge part, so even in BV logics, the SMT solver's abilities are super-important. But runtime in these logics are dominated by the SAT solver. I should play with more SMT solvers. I work on the STP SMT solver along with a team of very dedicated people (https://github.com/stp/stp/ https://github.com/stp/stp/), it's QF_BV (Quantifier Free BV) solver and it tends to do well in the competitions: https://smt-comp.github.io/2020/results.html https://smt-comp.github.io/2020/results.html So I'm probably a bit biased towards BV. For counting (e.g. https://github.com/meelgroup/approxmc https://github.com/meelgroup/approxmc) and sampling (e.g. https://github.com/meelgroup/unigen https://github.com/meelgroup/unigen) it's also 99% SAT solver runtime.

zitterbewegung 6y ago

To be honest can you redo it when the a14 chips come out in a device?

rurban 6y ago

So getting rid of ptrs and using roaring bitmap indices would make them fly.