SAT@Home (Parallel and Distrubuted SAT Solver), http://sat.isa.ru/pdsat/ |
Привіт Гість ( Вхід | Реєстрація )
SAT@Home (Parallel and Distrubuted SAT Solver), http://sat.isa.ru/pdsat/ |
nikelong |
Oct 10 2011, 17:34
Пост
#1
|
Тера ранчер Група: Trusted Members Повідомлень: 11 909 З нами з: 19-March 05 Користувач №: 92 Стать: Чол |
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 |
Oct 10 2011, 17:41
Пост
#2
|
interstellar Група: Team member Повідомлень: 17 049 З нами з: 22-February 06 З: Торонто Користувач №: 184 Стать: НеСкажу Free-DC_CPID Парк машин: ноут и кусок сервера |
News
New work is submitted October 1, 2011, 20:45 GMT Experiment with 10240 WUs started. The goal is to solve 10 problems of inversion of a function that is used to generate keystream in summation generator (4 LFSRs, initialization sequence of length 63 bits). The estimated run time was set to approximately 2 hours and the deadline was set to 1 day. Start September 29, 2011, 15:57 GMT Project has started! Thanks to all users who helped in testing. Special thanks to user brmn - our permanent user of the day. -------------------- |
Death |
Oct 13 2011, 09:35
Пост
#3
|
<script ///> Група: Moderators Повідомлень: 6 371 З нами з: 5-November 03 З: Kyiv Користувач №: 26 Стать: НеСкажу Free-DC_CPID Парк машин: гидропарк jabber:deadjdona@gmail.com |
Rank Name Members Recent average credit Total credit Country Type
1 Rule The World 4 4,379 71,928 Russia Social/political/religious 2 SETI.USA 14 4,697 51,708 None None 3 BOINC@Poland 16 1,472 17,221 Poland National 4 L'Alliance Francophone 15 1,086 12,941 International None 5 AMD Users 2 1,066 12,460 International None 6 Free-DC 1 535 6,608 International None 7 XtremeSystems 1 528 5,696 International None 8 Team 2ch 3 344 4,106 Japan None 9 IRNOK 2 265 3,060 Russia University or department 10 Crunchers@Freiburg 1 185 2,042 Germany None 11 SETI.Germany 12 146 1,751 Germany None 12 Ukraine 3 135 1,582 Ukraine National -------------------- |
Rilian |
Oct 14 2011, 17:57
Пост
#4
|
interstellar Група: Team member Повідомлень: 17 049 З нами з: 22-February 06 З: Торонто Користувач №: 184 Стать: НеСкажу Free-DC_CPID Парк машин: ноут и кусок сервера |
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 -------------------- |
Waterfall |
Oct 15 2011, 22:40
Пост
#5
|
Эрудит Група: Trusted Members Повідомлень: 1 607 З нами з: 24-May 10 З: Україна,Одеса(Odessa) Користувач №: 1 401 Стать: Чол Парк машин: ПК: Pentium, 2.80 GHz Ноут:DELL Studio, 2.26 GHz |
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..." |
Rilian |
Oct 28 2011, 13:34
Пост
#6
|
interstellar Група: Team member Повідомлень: 17 049 З нами з: 22-February 06 З: Торонто Користувач №: 184 Стать: НеСкажу Free-DC_CPID Парк машин: ноут и кусок сервера |
2011-10-28: SAT@home - First satisfying assignment was finded
First satisfying assignment for current SAT problem was successfully finded. In this experiment we will process all WUs in order to find other satisfying assignments, so called 'collisions'. -------------------- |
Rilian |
Nov 1 2011, 11:57
Пост
#7
|
interstellar Група: Team member Повідомлень: 17 049 З нами з: 22-February 06 З: Торонто Користувач №: 184 Стать: НеСкажу Free-DC_CPID Парк машин: ноут и кусок сервера |
First satisfying assignment was found
October 28, 2011, 4:41 GMT First satisfying assignment for current SAT problem was successfully found. In this experiment we will process all WUs in order to find other satisfying assignments, so called 'collisions'. Первый выполняющий набор для текущей SAT задачи был найден. В данном эксперименте будут обработаны все WU с целью найти остальные выполняющие наборы, т.н. 'коллизии'. -------------------- |
nikelong |
Nov 26 2011, 11:41
Пост
#8
|
Тера ранчер Група: Trusted Members Повідомлень: 11 909 З нами з: 19-March 05 Користувач №: 92 Стать: Чол |
Первые успехи российского проекта SAT@home
16 ноября 2011 г. AlexA В ходе работы проекта SAT@home была решена SAT-задача №1 для генератора A5/1. Это заняло 29 дней, первые 23 в активном режиме (65207 результатов), последние 6 - в неактивном (329 результатов). Найдены два выполняющих набора. Получен интересный опыт одновременной работы проекта по двум экспериментам. В текущем эксперименте успешно найден первый выполняющий набор для второй SAT-задачи по генератору A5/1. http://www.boinc.ru/news/news.aspx?id=865 -------------------- |
Rilian |
Dec 10 2011, 09:23
Пост
#9
|
interstellar Група: Team member Повідомлень: 17 049 З нами з: 22-February 06 З: Торонто Користувач №: 184 Стать: НеСкажу Free-DC_CPID Парк машин: ноут и кусок сервера |
2011-12-08: In new experiment 10 new SAT problems for A5/1 generator are to be solved. These problems cannot be solved using avaliable rainbow-tables. Version 1.14 for linux x64 client application was released. Compatibility with old versions added. During BOINCStats challenge real performance of SAT@home has reached 4.3 TFlops.
-------------------- |
Rilian |
Feb 3 2012, 23:24
Пост
#10
|
interstellar Група: Team member Повідомлень: 17 049 З нами з: 22-February 06 З: Торонто Користувач №: 184 Стать: НеСкажу Free-DC_CPID Парк машин: ноут и кусок сервера |
New solution December 16, 2011, 15:06 GMT SAT problem # 2 for the generator A5/1 was solved. It took 31 days, first 20 in active mode last 11 days in inert mode. One satisfying assignment was found New server application December 26, 2011, 15:41 GMT In the current experimet 2 SAT problems (from 10) were solved Solution of SAT problem # 2 was found in WU 272110 by zombie67 [MM] from SETI.USA. New vertion of server application released. Generation of tasks now is performed gradually New section, new solution January 6, 2011, 15:41 GMT In current experiment solution of SAT problem # 3 was found by T.H.@jisaku from Team 2ch and joeyraj from BOINCstats New section Found solutions is ready ISDCT SB RAS - member of IDGF January 20, 2011, 9:20 GMT ISDCT SB RAS has received status Organisational member of International Desktop Grid Federation Mate Soos published his Thoughts on SAT@home Deadline increased from 10 to 14 days New solution February 3, 2011, 15:05 GMT In current experiment solution of SAT problem # 4 was found by Traviss from UK BOINC Team and [SG-SPEG]Jeeper74 from SETI.Germany -------------------- |
Rilian |
Feb 19 2012, 19:45
Пост
#11
|
interstellar Група: Team member Повідомлень: 17 049 З нами з: 22-February 06 З: Торонто Користувач №: 184 Стать: НеСкажу Free-DC_CPID Парк машин: ноут и кусок сервера |
2012-02-19: During BOINCStats challenge real performance of SAT@home has reached 3.5 TFlops
After problems with overloading server and database were reconfigured In current experiment solution of SAT problem # 5 was found by verstapp from Sicituradastra. and [SG-SPEG] Nullinger from SETI.Germany -------------------- |
Rilian |
Apr 16 2012, 17:19
Пост
#12
|
interstellar Група: Team member Повідомлень: 17 049 З нами з: 22-February 06 З: Торонто Користувач №: 184 Стать: НеСкажу Free-DC_CPID Парк машин: ноут и кусок сервера |
SAT@home: New solution
2012-04-16: In current experiment solution of SAT problem # 8 was found by eLPeCKo and koll from Czech National Team On March 28, 2012 we presented a report about SAT@Home at the conference Parallel Computational Technologies, Novosibirsk, Section C SAT@home: New solution 2012-04-11: In current experiment solution of SAT problem # 7 was found by Jeff17 from BOINCstats and Bigred from Free-DC -------------------- |
Arbalet |
Apr 1 2015, 13:10
Пост
#13
|
Штандартенкранчер Група: Trusted Members Повідомлень: 2 647 З нами з: 16-August 05 Користувач №: 119 Стать: Чол Парк машин: FX-8320 + 1070Ti |
В текущем эксперименте были сгенерированы все WU. Примерно 10 дней новых WU не будет, а потом будет запущен новый эксперимент по поиску систем латинских квадратов. -------------------- (Show/Hide) |
Lo-Fi Версія | Поточний час: 26th September 2024 - 13:32 |