Привіт Гість ( Вхід | Реєстрація )

> SAT@Home (Parallel and Distrubuted SAT Solver), http://sat.isa.ru/pdsat/
nikelong
Oct 10 2011, 17:34
Пост #1


Тера ранчер
**********

Група: Trusted Members
Повідомлень: 12 443
З нами з: 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
http://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
User is offlineProfile CardPM
Go to the top of the page
+Quote Post
 
Reply to this topicStart new topic
Відповідей(1 - 12)
Rilian
Oct 10 2011, 17:41
Пост #2


interstellar
**********

Група: Team member
Повідомлень: 17 344
З нами з: 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.


--------------------
(Show/Hide)

Миссия проекта Help Fight Childhood Cancer (Помоги Победить Детский Рак) - подобрать белки, блокирующие некоторые виды рака. Подключайтесь!
IPB Image
IPB Image

IPB Image

IPB Image
IPB Image

общая статистика: BOINCstats * FreeDC команда: BOINC команда Ukraine

IPB Image
User is offlineProfile CardPM
Go to the top of the page
+Quote Post
Death
Oct 13 2011, 09:35
Пост #3


<script ///>
**********

Група: Moderators
Повідомлень: 6 429
З нами з: 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


--------------------
wbr, Me. Dead J. Dona OGR-27
User is offlineProfile CardPM
Go to the top of the page
+Quote Post
Rilian
Oct 14 2011, 17:57
Пост #4


interstellar
**********

Група: Team member
Повідомлень: 17 344
З нами з: 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


--------------------
(Show/Hide)

Миссия проекта Help Fight Childhood Cancer (Помоги Победить Детский Рак) - подобрать белки, блокирующие некоторые виды рака. Подключайтесь!
IPB Image
IPB Image

IPB Image

IPB Image
IPB Image

общая статистика: BOINCstats * FreeDC команда: BOINC команда Ukraine

IPB Image
User is offlineProfile CardPM
Go to the top of the page
+Quote Post
Waterfall
Oct 15 2011, 22:40
Пост #5


Эрудит
********

Група: Trusted Members
Повідомлень: 1 617
З нами з: 24-May 10
З: Україна,Одеса(Odessa)
Користувач №: 1 401
Стать: Чол
Парк машин:
ПК: Pentium, 2.80 GHz Ноут:DELL Studio, 2.26 GHz



(nikelong @ Oct 10 2011, 18:34) *

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..."
User is offlineProfile CardPM
Go to the top of the page
+Quote Post
Rilian
Oct 28 2011, 13:34
Пост #6


interstellar
**********

Група: Team member
Повідомлень: 17 344
З нами з: 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'.


--------------------
(Show/Hide)

Миссия проекта Help Fight Childhood Cancer (Помоги Победить Детский Рак) - подобрать белки, блокирующие некоторые виды рака. Подключайтесь!
IPB Image
IPB Image

IPB Image

IPB Image
IPB Image

общая статистика: BOINCstats * FreeDC команда: BOINC команда Ukraine

IPB Image
User is offlineProfile CardPM
Go to the top of the page
+Quote Post
Rilian
Nov 1 2011, 11:57
Пост #7


interstellar
**********

Група: Team member
Повідомлень: 17 344
З нами з: 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 с целью найти остальные выполняющие наборы, т.н. 'коллизии'.


--------------------
(Show/Hide)

Миссия проекта Help Fight Childhood Cancer (Помоги Победить Детский Рак) - подобрать белки, блокирующие некоторые виды рака. Подключайтесь!
IPB Image
IPB Image

IPB Image

IPB Image
IPB Image

общая статистика: BOINCstats * FreeDC команда: BOINC команда Ukraine

IPB Image
User is offlineProfile CardPM
Go to the top of the page
+Quote Post
nikelong
Nov 26 2011, 11:41
Пост #8


Тера ранчер
**********

Група: Trusted Members
Повідомлень: 12 443
З нами з: 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


--------------------
User is offlineProfile CardPM
Go to the top of the page
+Quote Post
Rilian
Dec 10 2011, 09:23
Пост #9


interstellar
**********

Група: Team member
Повідомлень: 17 344
З нами з: 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.


--------------------
(Show/Hide)

Миссия проекта Help Fight Childhood Cancer (Помоги Победить Детский Рак) - подобрать белки, блокирующие некоторые виды рака. Подключайтесь!
IPB Image
IPB Image

IPB Image

IPB Image
IPB Image

общая статистика: BOINCstats * FreeDC команда: BOINC команда Ukraine

IPB Image
User is offlineProfile CardPM
Go to the top of the page
+Quote Post
Rilian
Feb 3 2012, 23:24
Пост #10


interstellar
**********

Група: Team member
Повідомлень: 17 344
З нами з: 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


--------------------
(Show/Hide)

Миссия проекта Help Fight Childhood Cancer (Помоги Победить Детский Рак) - подобрать белки, блокирующие некоторые виды рака. Подключайтесь!
IPB Image
IPB Image

IPB Image

IPB Image
IPB Image

общая статистика: BOINCstats * FreeDC команда: BOINC команда Ukraine

IPB Image
User is offlineProfile CardPM
Go to the top of the page
+Quote Post
Rilian
Feb 19 2012, 19:45
Пост #11


interstellar
**********

Група: Team member
Повідомлень: 17 344
З нами з: 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


--------------------
(Show/Hide)

Миссия проекта Help Fight Childhood Cancer (Помоги Победить Детский Рак) - подобрать белки, блокирующие некоторые виды рака. Подключайтесь!
IPB Image
IPB Image

IPB Image

IPB Image
IPB Image

общая статистика: BOINCstats * FreeDC команда: BOINC команда Ukraine

IPB Image
User is offlineProfile CardPM
Go to the top of the page
+Quote Post
Rilian
Apr 16 2012, 17:19
Пост #12


interstellar
**********

Група: Team member
Повідомлень: 17 344
З нами з: 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


--------------------
(Show/Hide)

Миссия проекта Help Fight Childhood Cancer (Помоги Победить Детский Рак) - подобрать белки, блокирующие некоторые виды рака. Подключайтесь!
IPB Image
IPB Image

IPB Image

IPB Image
IPB Image

общая статистика: BOINCstats * FreeDC команда: BOINC команда Ukraine

IPB Image
User is offlineProfile CardPM
Go to the top of the page
+Quote Post
Arbalet
Apr 1 2015, 13:10
Пост #13


Штандартенкранчер
*********

Група: Moderators
Повідомлень: 2 764
З нами з: 16-August 05
Користувач №: 119
Стать: Чол
Парк машин:
FX-8320 + 1070Ti



В текущем эксперименте были сгенерированы все WU. Примерно 10 дней новых WU не будет, а потом будет запущен новый эксперимент по поиску систем латинских квадратов.


--------------------
(Show/Hide)


My asteroids: 1150 Achaia, 1643 Brown, 3286 Anatoliya

User is offlineProfile CardPM
Go to the top of the page
+Quote Post

Reply to this topicStart new topic
1 Користувачів переглядають дану тему (1 Гостей і 0 Прихованих Користувачів)
0 Користувачів:

 



- Lo-Fi Версія Поточний час: 28th March 2024 - 15:03

Invision Power Board v1.3.3 © 1996 IPS, Inc.