SAT@Home (Parallel and Distrubuted SAT Solver), http://sat.isa.ru/pdsat/ Налаштування

[nikelong]

URL: http://sat.isa.ru/pdsat/

Команда Украины: http://sat.isa.ru/pdsat/team_display.php?teamid=9

Найденные решения: http://sat.isa.ru/pdsat/solutions.php

SAT@home - исследовательский проект, использующий соединяемые через сеть Интернет компьютеры для решения трудных и практически важных задач (обращения дискретных функций, дискретной оптимизации, биоинформатики и т.д.), которые могут быть эффективно сведены к задаче о выполнимости булевых формул. В настоящее время в проекте решаются задачи обращения некоторых криптографических функций, используемых в поточных шифрах. Все исследуемые криптографические алгоритмы опубликованы в общедоступных источниках, соответствующие задания представляют собой случайным образом сгенерированные тесты и не содержат какой-либо конфиденциальной информации. В ближайшем будущем предполагается решать в проекте квадратичную задачу о назначениях. Проект был реализован с использванием библиотеки DC-API.
Основатели SAT@home:

Институт системного анализа РАН, лаборатория Распределенных вычислений - участник Международной федерации гридов из персональных компьютеров
Институт динамики систем и теории управления Сибирского отделения РАН, лаборатория Дискретного анализа и прикладной логики

Научная цель проекта

Проект предполагает решение разнообразных комбинаторных задач. Известно множество важных в практическом отношении задач, для решения которых на данный момент не доказано наличие эффективных (полиномиальных) алгоритмов. Большинство таких задач являются NP-трудными. Это означает, что при некоторых разумных (хоть и не доказанных) предположениях данные задачи вообще не могут быть решены за полиномиальное время. Однако решать частные случаи таких задач все равно приходится, так как это востребовано практикой: это и различные задачи дискретной оптимизации (например, задачи планирования производств), и задачи верификации дискретных устройств (возникающие, например, при разработке микросхем или доказательстве корректности программ). Поэтому крайне важно иметь для их решения методы, которые являются «эффективными» если и не в строгом понимании (то есть не обладают полиномиальной сложностью), то хотя бы на практике. Такие методы могут успешно справляться с многочисленными частными случаями NP-трудных задач огромных размерностей. Одним из наиболее простых в своей основе, и поэтому наиболее эффективным в плане программных реализаций является SAT-подход. Данный подход предполагает сводимость рассматриваемой исходной задачи к некоторой SAT-задаче, то есть к задаче о выполнимости конъюнктивной нормальной формы (КНФ). SAT-задачи допускают очень естественные формы распараллеливания, позволяющие использовать для их решения распределенные вычислительные среды (в том числе Grid). Собственно сводимость к SAT осуществляется эффективно (по сути, это содержание знаменитой теоремы Кука-Левина).

Крайне привлекательным классом задач, для решения которых можно использовать SAT-подход, являются задачи криптоанализа. Сразу оговоримся, что мы не решаем задачи дешифровки реальных конфиденциальных данных. Все рассматриваемые нами тесты сгенерированы случайным образом. В этом плане наша работа направлена на исследование стойкости современных систем шифрования и подразумевает реальную помощь в создании новых систем шифрования. Наиболее сильным достигнутым нами практическим результатом является успешный логический криптоанализ (то есть в форме SAT-задачи) генератора ключевого потока широко известного шифра A5/1. Данный результат был получен в 2009 году с использованием системы BNB-Grid (статья в Трудах ИСА РАН, статья на Arxiv, статья в Lecture Notes in Computer Science). В 2010-2011 годах появились исследования (см., например, эту работу), в которых также был осуществлен реальный криптоанализ A5/1, но с использованием совершенно других методов (по сути, использовалась продвинутая техника rainbow таблиц). Однако даже самые хорошие rainbow-таблицы не покрывают все ключевое пространство на 100%. Поэтому в ближайшей перспективе в рамках SAT@home предполагается решение задач поиска инициализирующих последовательностей для A5/1, не покрываемых лучшими известными rainbow таблицами.

В дальнейшем предполагается использовать SAT@home для исследования других криптографических функций, для решения некоторых «крайне трудных» задач дискретной оптимизации, в частности, квадратичной задачи о назначениях (QAP), а также для решения задач из области биоинформатики (исследование поведения дискретных моделей генных сетей).

 

Полезные сслыки:
http://ru.wikipedia.org/wiki/%D0%97%D0%B0%...%BC%D1%83%D0%BB
https://distributed.ru/forum/?t=1184
http://www.bc-team.org/viewtopic.php?p=3546
http://forum.boinc.ru/yaf_postst819_Proiekt-SAT-home.aspx

Це повідомлення відредагував x3mEn: Feb 22 2012, 10:22

[Rilian]

New work is submitted

October 13, 2011, 17:00 GMT
New experiment with 16384 WUs has started. The goal is to solve 1 SAT problem for summation generator (4 LFSRs, 66 bits). There are no publicly available results for solving inversion problems for this type of generator. In new version of server application problem with credits was fixed.

Experiment #2 finished
October 13, 2011, 16:55 GMT
All 10 problems were solved. SAT problems for summation generator in configuration (4 LFSR, 63 bit) are simple enough. SAT problems for (4 LFSR, 66 bits) are about 10 times harder.

New work is submitted
October 13, 2011, 5:02 GMT
New experiment with 81920 WUs has started. The goal is to solve another 10 SAT problems (8192 WUs for every problem) for summation generator (4 LFSRs, 63 bits). Aborting of WUs by server has caused problems with credits (thanks to users for reports and sorry for inconvenience). The estimated run time was set to approximately 20 min. (it will decrease effect of credit losing) and the deadline increased to 2 days. New version of server application now is being implemented, problem with credits will be fixed.

Experiment #1 finished
October 13, 2011, 3:01 GMT
Experiment #1 successfully finished. All 10 problems were solved. Thanks everybody! New experiment is coming soon. It looks like eight time more WUs are needed to load the system adequatly.

Message boards enabled
October 12, 2011, 13:45 GMT
Message boards were added. There are already some topics with discussion