What is the best hardware to run z3solver on in cloud?

[javafanboy]

I am looking at runing z3solver in public cloud and would like some sugestions on what type of VM to start experimenting with:

1. Does z3 user more than a single core?
2. I read somewhere that X86 is prefered over ARM - is this still the case 2022 or can more cost efficinet ARM now be used?
3. Are there and parameters of the problem I can use to get some idea about how much memory that efficiently can be utelized?

[NikolajBjorner]

Parallel solving is only applied if you configure z3 to use it.
There is a description here: https://z3prover.github.io/papers/programmingz3.html

The release has ARM support for Apple M series. The CI builds do build and test ARM on other platforms.
Our own perf testing is for x64 and I have no visibility into performance on ARM. Architectures with better
cache performance should have an advantage.

Memory: depends on workload. Many problems in SMTLIB require less than 50MB. Some larger problems easily use perhaps 8GB. This is still peanuts, but for VMs you may cap the memory to 16GB to be reasonably within bounds. Z3 is not set up to be inherently memory hungry. A proxy for memory usage is whether your instance involves quantifiers (can increase memory size), or number of atomic formulas + clauses. Use -st from the command-line on canaries to get an idea of memory footprint compared to instance characteristics.

[nunoplopes]

Just to complement what Nikolaj said: the big issue is CPU cache. Most (all?) cloud offerings don't give you a good cache because that's expensive. Plus, CPUs are shared with other tenants, so performance will vary widely depending on your neighbors.
Ideally you want a CPU with a lot of cache and few (beefy) cores.