Рассматривается низкоресурсный блочный шифр Simon32/64 из семейства Simon. Полная версия этого шифра состоит из 32 раундов. Задачи криптоанализа для 8 раундов Simon32/64 были неоднократно решены с помощвю SAT-подхода, т. е. путём сведения к проблеме булевой выполнимости и исполвзования SAT-решателей. Для 9 раундов задача все ещё является сложной для SAT-подхода. Построена SAT-кодировка криптоанализа 9-раундовой версии Simon32/64. Сформированы три класса тестов в зависимости от способа выбора открытого текста. С помощвю параллелвного SAT-решателя во всех случаях удалосв успешно решитв задачи криптоанализа при условии, что 16 из 64 битов секретного ключа известны.