Отзыв  профессора  Mate  Soos  о  проекте  SAT@home

 

 

Наша справка (от Nauchnik):  Mate Soos - один из крупнейших специалистов в области решения вычислительно трудных задач (в первую очередь криптографических) путем их сведения к SAT (задаче выполнимости булевых формул).  Mate Soos - автор SAT решателя cryptominisat . Этот решатель в 2011 году победил в крупнейшем специализированном соревновании SAT Competition в категории "параллельные SAT решатели". На этом соревновании cryptominisat показал себя хорошо при решении разнообразных задач, в частности криптографических. Сейчас в проекте SAT@home при помощи распределенных добровольных вычислений решаются именно криптографические задачи, сведенные к SAT, мнение о проекте такого специалиста весьма интересно. Mate предлагает много идей по улучшению процедур решения SAT задач в проекте.

 

"Размышления о SAT@home" были опубликованы на страничке Mate.   Автор перевода Alexone. Рецензор Nauchnik.

 


11 Декабря 2011        Размышления о SAT@Home

 

   Если вы когда-нибудь задумывались над тем, как ваша SAT задача, требующая многих месяцев решения, может быть решена, то ответ прост: SAT@Home от русских исследователей! Подобная идея назревала в моей голове, мы с дружественным исследователем из Америки даже запустили мини-проект, но у нас так и не получилось довести его до рабочего состояния :(. Здорово, что кто-то нашел время, чтобы это сделать. Создание подобных вещей имеет как простые так и сложные этапы. Настройка BOINC сервера несложная задача, но ведь требуется, чтобы он работал в режиме 24/7, а вот это уже сложно, если вы не директор университета или у вас нет своей компании.  Потом требуется написать скрипты, что относительно несложно сделать, но их тестирование и отладка занимает много времени. Действительно сложной задачей, на мой взгляд, является то, как осуществить распараллеливание. Много научных трудов может быть написано на эту тему,  но в данном проекте используется простейший метод, а именно разделение задания на части путем варьирование значений нескольких переменных. Я думаю это хороший старт, начинать надо с простых вещей – ведь первый автомобиль не пытался разогнаться до 300 км/ч, и здесь не стоит.

 

Предполагаю, что со временем подход будет становиться все более и более сложным и включать в себя все больше различных техник и алгоритмов, от варьирования значений переменных до обмена дизъюнктами с использованием множества эвристических  оценок их полезности, и до обмена статистикой полезности параметров. В конце концов и сами задания могут быть поделены на категории. Одни могут осуществлять «простой» поиск без накапливания ограничений, другие заниматься решением с использованием конфликтных дизъюнктов (и чисткой конфликтной базы?). Третьи могут заниматься только упрощением кодировки с использованием специфических алгоритмов, таких как поглощение или усиление, четвертые — производить анализ данных на текущем шаге решения задачи: оценивать достижимость решения, количество гейтов (функциональных элементов) или элементов другого рода при представлении проблемы на более высоком уровне, например, сумматоров и так далее. Другими словами есть много вариантов развития проекта. Возможно, даже имеет смысл создание общего интерфейса, при помощи которого различные SAT-солверы смогут объединяться в одну структуру и использоваться совместно.

 

Мой друг когда-то написал мне мэйл, в котором описана идея оплаты посещения веб страниц не через просмотр баннеров, а через запуск программы на javascript. Конечно возникла идея написать приложение решающее SAT задачи на javascript и получать решения от множества людей, разместив код на часто посещаемых страницах. Сервер будет распределять задания на javascript приложения, а потом собирать полученные результаты расчетов, в то время как человек занимается интернет серфингом. Это обеспечит дешевое (возможно даже бесплатное) и практически неограниченное процессорное время для сложных задач. Мы могли бы например использовать его, чтобы ответить на некоторые вопросы математики, или взломать некоторые криптографические алгоритмы… просто надо найти того безумца который бы смог написать SAT решатель на javascript! :)

 
 

Вернуться на BOINC.RU