z3 Производительность решателя SMT на разных платформах

У меня есть логические проблемы, написанные с использованием z3py. Я запускаю их на обоих компьютерах (ядро i5 + 8GB RAM) и кластер (32 AMD Operaton 6320 cpus + 500GB RAM). В среде исполнения нет большой разницы, и иногда удаленный сервер занимает больше времени, что меня смущает. Кто-нибудь знает, эффективнее ли решение z3 на многоядерном компьютере?z3 Производительность решателя SMT на разных платформах

источник

2015-05-26 Zhongjun ' Mark' Jin

По умолчанию Z3 не использует несколько ядер или процессоров.

Он, однако, поставляется с партитурной и партикой и тактикой, которые могут использоваться для создания пользовательской тактики, использующей параллелизм.

источник

2015-05-26 19:34:37

Спасибо, Кристоф. Это действительно полезно. Но можно ли использовать эти две тактики в Z3 python api? –

Да, они называются ParAndThen и ParOr, см. Здесь: http://z3prover.github.io/api/html/namespacez3py.html#ab3f56f42a92f895a293dd106ce88076d –

Спасибо. Ценить это! –

z3 Производительность решателя SMT на разных платформах

ответ

Смежные вопросы