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].

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

Примечания

  1. ↑ SAT@Home. Дата обращения: 26 декабря 2012. Архивировано 21 декабря 2012 года.
  2. ↑ SAT@home detailed stats. Дата обращения: 5 сентября 2013. Архивировано 11 августа 2013 года.
  3. ↑ Архив новостей SAT@home. Дата обращения: 26 декабря 2012. Архивировано из оригинала 4 января 2013 года.
  4. ↑ 1 2 3 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.

Ссылки

Content Disclaimer

Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.

  1. The information displayed on this website is sourced in part or in whole from Wikipedia and has been adapted for the purpose of restating it. We strive to provide accurate and relevant information, however:
  2. There is no guarantee of absolute accuracy. Wikipedia is an open, collaborative project that can be edited by anyone, so information is subject to change.
  3. It is not intended to constitute professional advice. The content displayed is for informational and educational purposes only. For important decisions (e.g., medical, legal, or financial), please consult a professional.
  4. Content copyright. Wikipedia is licensed under the Creative Commons Attribution-ShareAlike License (CC BY-SA). This means that content may be reused with appropriate attribution and shared under a similar license.
  5. Responsible use. Any risk arising from the use of information from this website is entirely the responsibility of the user.