<story><title>SMT Solving on an iPhone (2018)</title><url>https://www.cs.utexas.edu/~bornholt/post/z3-iphone.html</url></story><parent_chain></parent_chain><comment><author>zero_k</author><text>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&amp;#x27;s at.&lt;p&gt;I once had an old, but &amp;quot;enthusiast&amp;quot; i7 that had a 3-lane mem setup, and &amp;quot;upgraded&amp;quot; to a consumer dual-lane i7 that was 2-3 gens ahead. It had the same performance(!) for SAT solving. Was pretty eye-opening.</text></comment>
<story><title>SMT Solving on an iPhone (2018)</title><url>https://www.cs.utexas.edu/~bornholt/post/z3-iphone.html</url></story><parent_chain></parent_chain><comment><author>panpanna</author><text>Note that this sort of software can be extremely sensitive to cache arrangement.&lt;p&gt;Not only actual performance but also small details such as data arrangement, line size, replacement model and coherency model.&lt;p&gt;Source: I worked on performance improvement for a related piece of software.</text></comment>