Розподілені обчислення в Україні -> Відповідь у SAT@Home (Parallel and Distrubuted SAT Solver)

Останні 10 повідомлень [ в зворотному порядку ]

Arbalet	Дата Apr 1 2015, 13:10
	В текущем эксперименте были сгенерированы все WU. Примерно 10 дней новых WU не будет, а потом будет запущен новый эксперимент по поиску систем латинских квадратов.
Rilian	Дата Apr 16 2012, 17:19
	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
Rilian	Дата Feb 19 2012, 19:45
	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	Дата Feb 3 2012, 23:24
	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	Дата Dec 10 2011, 09:23
	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.
nikelong	Дата Nov 26 2011, 11:41
	Первые успехи российского проекта 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	Дата Nov 1 2011, 11:57
	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 с целью найти остальные выполняющие наборы, т.н. 'коллизии'.
Rilian	Дата Oct 28 2011, 13:34
	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'.
Waterfall	Дата Oct 15 2011, 22:40
	(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..."
Rilian	Дата Oct 14 2011, 17:57
	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
Перегляд теми повністю (відкриється у новому вікні)

Українська команда з розподілених обчислень