Hacker News Reader

Comment by zero_k | Hacker News Reader

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.

View on HN

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

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/), 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 So I'm probably a bit biased towards BV. For counting (e.g. https://github.com/meelgroup/approxmc) and sampling (e.g. https://github.com/meelgroup/unigen) it's also 99% SAT solver runtime.

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.

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.

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.

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

The only 3 Lane i7 I know of is the Nehalem

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

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-mi...

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.

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

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

Reply on news.ycombinator.com