[SAT] Running Kissat SAT-solver on ARM CPU
Regarding that old story about running Z3 SMT-solver on iPhone....
I tried various server-grade ARM CPUs I could access.
Latest Kissat from github.
I run "tissat -j1" (to limit it on single thread).
Some x86 CPUs for comparison:
My relic Intel(R) Core(TM)2 Duo CPU T9400 @ 2.53GHz:
"All 568 test jobs succeeded in 4.13 seconds."
My relic Intel(R) Xeon(R) CPU E31220 @ 3.10GHz (8MiB L3 cache)
"All 568 test jobs succeeded in 3.02 seconds."
AMD Ryzen 5 3600 6-Core Processor (32MiB L3 cache):
"All 568 test jobs succeeded in 2.05 seconds."
AMD EPYC Processor (something from Hetzner with 16MiB L3 cache):
"All 568 test jobs succeeded in 1.84 seconds."
instances on AWS.
They say it runs on AWS Graviton
"All 568 test jobs succeeded in 5.72 seconds."
"All 568 test jobs succeeded in 5.56 seconds."
CAX11 instance from Hetzner. "Ampere" ARM64 CPU, as they say.
lscpu: "Model name: Neoverse-N1"
"All 568 test jobs succeeded in 2.65 seconds."
Didn't try Z3 SMT-solver yet...
(the post first published at 20230425.)
List of my other blog posts.
Subscribe to my news feed
Yes, I know about these lousy Disqus ads.
Please use adblocker.
I would consider to subscribe to 'pro' version of Disqus if the signal/noise ratio in comments would be good enough.