SAT@home

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

SAT@Home
Платформа BOINC
Объём загружаемого ПО 10 МБ
Объём загружаемых данных задания 2 КБ
Объём отправляемых данных задания 20 КБ
Объём места на диске 10 МБ
Используемый объём памяти 80 МБ
Графический интерфейс нет
Среднее время расчёта задания до 5 часов
Deadline 10 дней
Возможность использования GPU нет

История проекта

Вычисления в рамках проекта стартовали[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].

Судя по всему, проект прекратил своё существование в 2016 году.

Примечания
  1. SAT@Home
  2. SAT@home detailed stats
  3. Архив новостей SAT@home (недоступная ссылка). Дата обращения: 26 декабря 2012. Архивировано 4 января 2013 года.
  4. Найденные решения SAT@home (недоступная ссылка). Дата обращения: 26 декабря 2012. Архивировано 21 декабря 2012 года.
  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.

Ссылки
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.