Skip Navigation Links
Проекты
Биолого-медицинские
Skip Navigation Links
Естественнонаучные
Skip Navigation Links
Математические
Skip Navigation Links
Прочие проекты
Skip Navigation Links
Завершённые
Skip Navigation Links

SAT@home

 

Задачи проекта
  • Решение комбинаторных задач, сведенных к задачам о булевой выполнимости (SAT)

  • Изучение применимости SAT-похода к решению различных прикладных задач

  • Опробирование SAT-алгоритмов в криптоанализе

  • Решение задачи о диагональных квадратах с помощью SAT-решателя
  • Обработка решений полученных на кластерах

  • Задачи криптоанализа не являются самоцелью проекта, а выступают в роли аргументированно трудных тестов. Успешная апробация вычислительной технологии на криптографических тестах означает её принципиальную применимость для решения задач, вычислительная трудность в которые не заложена искусственно.
                                                                                                            

 

Источники данных  для проекта

  • Комбинаторные, криптографические задачи для которых возможно применить SAT-подход 
Приложения проекта
  • ParallelAndDistributedSATsolver (Intel/AMD)
  • PD-SAT for cryptology (Intel/AMD)
  • Все приложения Win/Mac/Linux
Особенности приложения
Что считают наши компьтеры?
Результаты проекта
  • Показана применимость SAT-подхода для криптоанализа поточных шифров на примере генератора A5/1
  • Показана применимость SAT-подхода для криптоанализа на примере шифра Bivium
  • Показана применимость SAT-подхода для нахождения ортогональных пар диагональных латинских квадратов.
  • Найдено 46 ортогональных пар диагональных латинских квадратов порядка 10
  • Найдено 17 псевдотроек взаимно ортогональных латинских квадратов порядка 10
  • Найденные дополнительные решения проблемы диагональных квадратов
 

Дополнительная информация

 
  • Проект SAT@home был запущен 29 сентября 2011 года двумя российскими институтами – ИДСТУ СО РАН (Иркутск) и ИСА РАН (Москва). У центра грид-технологий и распределенных вычислений ИСА РАН была необходимая материальная база (сервер, хостинг сайта), а у сотрудников накопился большой опыт создания и администрирования подобных проектов (в июне 2011 года ИСА РАН запустили проект Optima@home, направленный на решение некоторых трудных задач оптимизации). В лаборатории ИДСТУ СО РАН были созданы программные комплексы, предназначенные для сведения к задаче выполнимости булевых формул (SAT) задач из различных областей (биоинформатика, поиск комбинаторных структур, криптография). Получаемые SAT-задачи допускают очень естественные формы распараллеливания, позволяющие использовать для их решения не только суперкомпьютеры, но и распределенные вычислительные среды. В лаборатории были разработаны и успешно использованы на суперкомпьютерах параллельные SAT-решатели, но для обработки некоторых классов задач не хватало вычислительных ресурсов. Именно для решения этих задач и был создан проект SAT@home.
  • В мае 2012 года в проекте был успешно завершен полугодовой эксперимент, направленный на решение 10 задач исследования стойкости системы шифрования A5/1, которые не решаются стандартными способами (с помощью rainbow-таблиц). В ближайшем будущем предполагается использовать проект SAT@home для решения задачи поиска тройки взаимно ортогональных латинских квадратов порядка 10. На текущий момент 10 - это минимальный порядок, для которого неизвестно существование такой тройки. Данная задача очень трудна, поэтому сейчас в проекте SAT@home запущен эксперимент, направленный на поиск пар ортогональных латинских квадратов порядка 9 и 10 с дополнительным условием «диагональности». Данные задачи проще, чем задача поиска троек попарно ортогональных латинских квадратов порядка 10. Тем не менее представляет интерес нахождение новых ортогональных диагональных пар. Кроме этого, исследуя данные задачи, мы пытаемся найти возможные направления для улучшения производительности используемых нами алгоритмов. В настоящий момент в проекте уже найдены более 100 пар диагональных латинских квадратов порядка 9.
  • По состоянию на 22 августа 2012 года в проекте 2578 участников из 80 стран, 1044 из них активны. Средняя производительность за год составляет 2,2 терафлопса (пиковая – 4.7 терафлопс).