У меня есть логические проблемы, написанные с использованием z3py. Я запускаю их как на своем ПК (intel core i5 + 8 ГБ ОЗУ), так и на кластере (32 процессора AMD Operaton 6320 + 500 ГБ ОЗУ). Нет большой разницы во времени выполнения, и иногда удаленный сервер занимает больше времени, что меня смущает. Кто-нибудь знает, является ли решатель z3 более эффективным на многоядерной машине?
Производительность решателя z3 SMT на разных платформах
Ответы (1)
По умолчанию Z3 не использует несколько ядер или процессоров.
Однако он поставляется с тактиками пар-или и пар-и, которые можно использовать для создания пользовательских тактик, использующих параллелизм.
person
Christoph Wintersteiger
schedule
26.05.2015
Спасибо, Кристоф. Это действительно полезно. Но можно ли использовать эти две тактики в Z3 Python API?
- person Zhongjun 'Mark' Jin; 26.05.2015
Да, они называются ParAndThen и ParOr, см. здесь: z3prover.github.io/ API/html/
- person Christoph Wintersteiger; 27.05.2015
Спасибо. Ценить это!
- person Zhongjun 'Mark' Jin; 27.05.2015
