Рубрика «прувер»

Зачем покупать дорогой ПК, если ваш iPhone быстрее решает SMT?

Задача выполнимости формул в теориях (satisfiability modulo theories, SMT) — это задача разрешимости для логических формул с учётом лежащих в их основе теорий. — Википедия

Несколько дней назад я написал в твиттере: «Любопытный эксперимент: на новом iPhone прувер Z3 работает быстрее, чем на моём (довольно дорогом) десктопном Intel. Пора перевести все формальные методы исследований на телефон».

Я читал о невероятном прогрессе, которого добились разработчики процессоров Apple, и что скоро маки переведут на собственные ARM-процессоры от Apple. Эти отчёты обычно ссылаются на некоторые кросс-платформенные тесты, такие как Geekbench для демонстрации, что мобильные процессоры Apple не уступают мобильным и настольным процессорам Intel. Но я всегда немного скептически относился к этим кросс-платформенным тестам (как и к другим) — действительно ли они отражают скорость выполнения реальных задач, для которых я использую свои Mac?
Читать полностью »


https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js