SAT@home — российский проект добровольных вычислений на платформе BOINC, запущенный в сентябре 2011 года. Научной целью проекта является решение дискретных задач путём сведения их к задаче о выполнимости булевых формул (SAT, от — выполнимость) в конъюнктивной нормальной форме (КНФ). Отыскание решения выбранной задачи производится с использованием одного из известных SAT-решателей, реализующего алгоритм DPLL. Проект поддерживается лабораторией Дискретного анализа и прикладной логики Института динамики систем и теории управления Сибирского отделения РАН и Центром распределённых вычислений Института проблем передачи информации. По состоянию на 19 сентября 2014 года в проекте приняли участие 18394 компьютеров 7239 пользователей из 124 стран, обеспечивая производительность порядка 3,1 терафлопс. Участвовать в проекте может любой желающий, обладающий компьютером с выходом в Интернет, установив на него программу BOINC.
История проекта Вычисления в рамках проекта стартовали в сентябре 2011 года с решения задачи криптоанализа генератора A5/1, применяющегося в GSM-связи. По известному фрагменту ключевого потока требовалось определить инициализирующую последовательность, то есть начальное заполнение регистров генератора. Целью проводимых вычислений являлось доказательство применимости SAT-подхода к решению данной задачи для тех случаев, когда другими методами (например, с использованием радужных таблиц) отыскание решения невозможно. В результате расчетов к маю 2012 года были решены 10 тестовых задач криптоанализа A5/1.
В июне 2012 года был запущен новый эксперимент, целью которого являлся поиск ортогональных пар диагональных латинских квадратов порядка 9. К августу 2012 года было найдено 134 пары, что доказало применимость данного подхода к поставленной задаче. Следом за этим был запущен эксперимент по поиску ортогональных пар диагональных латинских квадратов порядка 10. В результате вычислений на данный момент найдены 13 пар латинских квадратов, которые не совпадают с известными парами, приведенными в статье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..
Научные достижения 2012 год Показана применимость SAT-подхода для криптоанализа поточных шифров на примере генератора A5/1. Показана применимость SAT-подхода для нахождения ортогональных пар диагональных латинских квадратов. Найдено 5 ортогональных пар порядка 10. 2013 год Найдено 12 ортогональных пар диагональных латинских квадратов порядка 10.
Судя по всему, проект прекратил своё существование в 2016 году.
Примечания
Ссылки Официальный сайт проекта Научные публикации Заикин О., Андреев А. Охотники за квадратами // Троицкий вариант — Наука. № 24 (118) от 11 декабря 2012. С. 6.
Категория:Математические проекты распределённых вычислений