SAT@home

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск
SAT@Home
Платформа

BOINC

Объём загружаемого ПО

10 МБ

Объём загружаемых данных задания

2 КБ

Объём отправляемых данных задания

20 КБ

Объём места на диске

10 МБ

Используемый объём памяти

80 МБ

Графический интерфейс

нет

Среднее время расчёта задания

до 5 часов

Deadline

10 дней

Возможность использования GPU

нет

SAT@home — российский проект добровольных вычислений на платформе BOINC, запущенный в сентябре 2011 года[1]. Научной целью проекта является решение дискретных задач путём сведения их к задаче о выполнимости булевых формул (SAT, от англ. Satisfiability — выполнимость) в конъюнктивной нормальной форме (КНФ). Отыскание решения выбранной задачи производится с использованием одного из известных SAT-решателей, реализующего алгоритм DPLL. Проект поддерживается лабораторией Дискретного анализа и прикладной логики Института динамики систем и теории управления Сибирского отделения РАН и Центром распределённых вычислений Института проблем передачи информации. По состоянию на 19 сентября 2014 года в проекте приняли участие 18394 компьютеров 7239 пользователей из 124 стран, обеспечивая производительность порядка 3,1 терафлопс[2]. Участвовать в проекте может любой желающий, обладающий компьютером с выходом в Интернет, установив на него программу BOINC.

История проекта[править | править вики-текст]

Вычисления в рамках проекта стартовали[3] в сентябре 2011 года с решения задачи криптоанализа генератора A5/1, применяющегося в GSM-связи. По известному фрагменту ключевого потока требовалось определить инициализирующую последовательность, то есть начальное заполнение регистров генератора. Целью проводимых вычислений являлось доказательство применимости SAT-подхода к решению данной задачи для тех случаев, когда другими методами (например, с использованием радужных таблиц) отыскание решения невозможно. В результате расчетов к маю 2012 года были решены 10 тестовых задач криптоанализа A5/1[4].

Первая пара ортогональных диагональных латинских квадратов порядка 10, найденная в проекте SAT@Home пользователями tanos и notnA

В июне 2012 года был запущен новый эксперимент, целью которого являлся поиск ортогональных пар диагональных латинских квадратов порядка 9. К августу 2012 года было найдено 134 пары, что доказало применимость данного подхода к поставленной задаче. Следом за этим был запущен эксперимент по поиску ортогональных пар диагональных латинских квадратов порядка 10. В результате вычислений на данный момент найдены 13 пар латинских квадратов[4], которые не совпадают с известными парами, приведенными в статье[5].

Научные достижения[править | править вики-текст]

2012 год
  • Показана применимость SAT-подхода для криптоанализа поточных шифров на примере генератора A5/1.
  • Показана применимость SAT-подхода для нахождения ортогональных пар диагональных латинских квадратов. Найдено 5 ортогональных пар порядка 10[4].
2013 год
  • Найдено 12 ортогональных пар диагональных латинских квадратов порядка 10[4].

Примечания[править | править вики-текст]

  1. SAT@Home
  2. SAT@home detailed stats
  3. Архив новостей SAT@home
  4. 1 2 3 4 Найденные решения SAT@home
  5. Brown et al. Completion of the Spectrum of Orthogonal Diagonal Latin Squares. Lecture notes in pure and applied mathematics. 1992. Vol. 139. Pp 43–49.

Ссылки[править | править вики-текст]