如果您的iPhone更快地解决SMT，为什么还要购买昂贵的PC？考虑到逻辑公式的基础理论，可满足性模理论（SMT）公式是逻辑公式的可解性问题。 - 维基百科几天前，我
发了一条
推文 ：“一个有趣的实验：在新iPhone上，Z3证明器的工作速度比我（相当昂贵）的台式机英特尔更快。 现在该将所有正式的研究方法转移到手机上了。”
我读到有关
苹果处理器开发人员取得的令人难以置信的进步，并且Mac很快就会转移到
苹果自己的ARM处理器上 。 这些报告通常引用一些跨平台测试，例如
Geekbench，以证明Apple的移动处理器不逊于Intel的移动处理器和台式机处理器。 但是，我对这些跨平台测试（以及
其他跨平台测试）始终持怀疑态度-它们是否真的反映了我使用Mac进行实际任务的速度？
作为正式方法的研究人员，我经常必须运行SMT求解器，通常是
Z3证明器 。 我花了很多时间研究Z3的性能特征。 它具有一些测试未考虑的功能（Z3通常是单线程的）。 我最近购买了配备最新Apple
A12处理器的新
iPhone XS 。 而且，不知何故，我决定不做任何事情，决定在iOS中编译Z3，然后看看新手机（或假设的未来Mac）的运行速度如何。
第一次测试
事实证明，交叉编译Z3非常简单，您只需要更改几行代码即可。 我发布了
在您自己的iOS设备上启动Z3的资源。 为了进行测试，我从最近有关
分析符号计算的工作中提出了一些疑问：对于每种情况，
都提取了
Rosette生成的SMT。
在第一次测试中，我将iPhone XS与运行在Intel Core i7-7700K上的台式机进行了比较，这是我18个月前造车时面向消费者市场的最佳Intel芯片。 英特尔本应毫无问题地获胜，但结果却不同：
在这23秒的测试中，iPhone XS的速度提高了约11％！ 我在Twitter上报告了此信息，但Twitter并没有太多细节余地，因此我将在此处介绍：
- 该基准是SMT的
QF_BV一部分，因此Z3使用位爆和SAT求解器解决了这一部分。 - 即使运行10次，结果也非常稳定：iPhone支持此性能，并且似乎不会因过热而开始变慢。 1个 。 尽管如此，基准仍然相当短暂。
- 几个人问这是否是由于不确定性造成的。 也许在不同的平台上，由于使用随机数或其他原因，求解器的运行方式有所不同？ 但是我相当仔细地检查了Z3的详细发布，结果很难由此解释。
- 这两个系统都运行Z3 4.8.1，我使用Clang在相同的优化设置下进行了编译。 我还使用预构建的Z3二进制文件（由GCC编译）在i7-7700K上进行了测试，但它们的速度甚至更慢。
这是怎么回事？
这怎么可能？ Core i7-7700K是相同的台式机处理器。 在单线程任务中，它的功耗约为45瓦，工作频率为4.5 GHz。 另一方面，拔掉iPhone。 它可能甚至不会消耗掉10％的这种功率，并且（我们希望）在2 GHz频段的某个地方工作。 此外，在进行了对比测试之后，我查看了有关iPhone电池使用情况的报告：它说Slack的能耗是Z3应用程序的4倍，尽管屏幕上的时间更少。
苹果公司没有提供足够的信息来了解iPhone上Z3的性能，但是幸运的是，英特尔为其处理器提供了此信息。 我在
VTune上闲逛
了一段时间，以在台式机上启动Z3时发现性能瓶颈。 正如
Mat Soos所指出的那样，SAT求解器
大部分时间都在分发上 ，这
对缓存非常敏感 。 VTune表示同意，并说Z3在迭代观察到的文字时会花费大量时间在内存中等待。 因此，性能的关键似乎是缓存大小和内存延迟。 这种效果可以解释为什么iPhone在此测试中如此强大：A12芯片具有
巨大的L2高速缓存，具有低延迟 ，并且与7700K相比，高速缓存未命中后似乎还具有更好的内存延迟。
苹果处理器的飞速发展
为了确认结果，我进行了更广泛的实验，收集了我可以获得的所有Apple设备。 我还选择了大约10倍长的基准测试（即在台式机上运行4分钟），以减轻对移动CPU性能突增的担忧。
以下是苹果首款64位用户处理器A7的这些设备（发布日期）的结果：
应当立即注意到，在更长的测试中，i7-7700K台式机处理器优于iPhone XS。 但是iPhone的竞争力令人难以置信，显示出i7-7700K和它的前身i7-6700K之间的成绩，i7-6700K是不到两年前最快的消费型台式机处理器。
为了娱乐，我在我的2016 MacBook中添加了另一个酷睿m7-6Y75处理器。 在Z3测试中，我的手机比笔记本电脑快50％。
真正值得注意的是趋势：这种Z3基准每年持续稳定地提高30％。 显然，您不应从一个愚蠢的测试中得出深远的结论，但似乎经过几次迭代，Apple处理器将变得非常适合工作负载。
2 。 老实说，我没想到我们会如此接近：智能手机的现代架构简直令人难以置信！
感谢Megan Cowan ， Max Willsy和Eddie Ian在其他设备上运行测试的帮助。
1 。
麦克斯注意到iPhone是防水的，因此可以将其浸入冰浴中进行检验。 但是我为电话花了很多钱，所以我不想自愿进行这种体验。
↑2 。 我敢打赌，新款
iPad Pro的A12X速度更快，这要归功于平板电脑具有更大的
散热范围 。
↑