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

I tried a1.medium and a1.4xlarge instances on AWS. More info They say it runs on AWS Graviton

• a1.medium: "All 568 test jobs succeeded in 5.72 seconds."
• a1.4xlarge: "All 568 test jobs succeeded in 5.56 seconds."

Also:

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