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

[Waterfall]

SAT@Home (Parallel and Distrubuted SAT Solver)

А чого все на English подаєте, якщо проект чисто російський?

Що пишуть про проект його автори:" SAT@Home - совместный российский проект Института системного анализа РАН и Института динамики систем и теории управления Сибирского отделения РАН.
Цели проекта - поиск решения проблем инверсии дискретных функций, дискретной оптимизации, биоинформационных технологий и др. SAT-проблем.
Мы сводим различные задачи к SAT - задаче решения уравнений вида ''КНФ=1'', где КНФ - это конъюнктивная нормальная форма. Задача в такой постановке NP-трудная, но для некоторых важных на практике областей существуют SAT решатели, способные работать с реальными большими задачами.
В основе данных решателей лежит алгоритм DPLL.
Из доступных в интернете статей нашего коллектива можно посмотреть эту статью http://num-meth.srcc.msu.su/zhurnal/tom_2008/v9r115.html
Сейчас в проекте запущена задача анализа свойств криптографических дискретных функций, используемых в генераторах ключевого потока. В частности, скоро запустим SAT-задачи для генератора A5/1, который используется в стандарте GSM.
Открытые научные исследования в этой области способствуют улучшению широко используемых поточных систем шифрования. Текущие наши результаты в этой области можно посмотреть здесь http://arxiv.org/abs/1102.3563.
Скоро планируем перейти к задаче Quadratic Assignment Problem (про полезность см. англ. Википедию).
Первый опыт ее решения у нас есть http://num-meth.srcc.msu.su/zhurnal/tom_2011/v12r125.html, надо перенести на desktop grid. Есть результаты по решению задач биоинформатики, поставленные НИИ Цитологии и Генетики (Новосибирск). Речь идет об исследованию поведения дискретных моделей генных сетей, эти задачи мы тоже собираемся решать в проекте. Возможно также что-то получится с задачей поиска ортогональных латинских квадратов определенной размерности.... Имеются приложения для x86-совместимых ЦП на платформах Windows и Linux..."