1. Что такое SAT?
SAT (сокращенно от Satisfiability) - задача выполнимости булевых формул. В ней требуется найти выполняющий набор булевой формулы (если он существует), либо доказать факт его отсутствия. Выполняющий набор — это набор значений истинности булевых переменных, который при подстановки обращает булеву формулу в 1. Обычно в качестве булевой формулы используется конъюнктивная нормальная форма (КНФ), т. к. это удобный и унифицированный формат. Многие трудные комбинаторные задачи допускают эффективную сводимость к SAT.
2. Зачем понадобилось создание проекта SAT@home?
Основная причина в нехватке вычислительных мощностей. До проекта мы решали задачи на вычислительных кластерах. Но весьма проблематично получить большие ресурсы кластера на продолжительное время. К тому же на них естественнее решать задачи, требующие интенсивные обмены данными (на то там и мощный интерконнект), а у нас непосредственно при решении задач обменов почти нет, задачи идеально подходят для распределенных вычислений. Мы продолжаем использовать кластеры для нахождения параметров декомпозиции, эти вычисления как раз непродолжительные и требуют мощный интерконнект. Найденные же на кластерах параметры декомпозиции используются в SAT@home.
3. Какие задачи решаются в проекте сейчас?
Сейчас запущен эксперимент, направленный на решение 10 задач криптоанализа генератора A5/1, которые не решаются с помощью rainbow-таблицы, построенной специально для этих целей (см. A5/1 cracking project). С помощью rainbow-таблиц задачи криптоанализа генератора A5/1 решаются быстро, но успешное решение не гарантировано на 100%. В SAT-подходе эти задачи решаются долго, но их решение находится с вероятностью 100%. Сделали мы наши задачи так:
сгенерировали случайным образом 1000 задач криптоанализа генератора A5/1;
попробовали решить эти 1000 задач с помощью rainbow-таблицы. Не решились 125 из 1000.
из 125 случайно выбрали 10, по ним построили SAT-задачи, которые и решаются сейчас в проекте.
В каждой из этих 10 SAT-задач достаточно найти одно решение, чтобы проверить, что мы решили то, что нужно. В разделе Найденные решения размещена таблица с результатами.
4. Сколько решений может быть в задаче криптоанализа генератора A5/1
Мы экспериментально обнаружили, что выполняющих наборов у КНФ, кодирующих криптоанализ генератора A5/1, может быть несколько. Эти наборы соответствуют инициализирующим последовательностям, по которым генератор выдает одинаковый ключевой поток (по аналогии с хэш-функциями их можно назвать «коллизиями» ). Jovan Golic в своей статье 1997 г. теоретически обоснована возможность существования таких «коллизий» для A5/1. На практике у задач криптоанализа генератора A5/1 оказывается от 1 до 3 решений (не исключено, что бывает и больше). Ранее в SAT@home были решены 2 задачи, в которых были найдены все решения.
5. Что именно содержится в конкретном задании?
По задаче криптоанализа генератора A5/1 мы строим КНФ, которая содержит 10784 переменных и 49280 дизъюнктов. В каждой такой КНФ первые 64 переменные кодируют инициализирующую последовательность (вход генератора), последние 160 кодируют ключевой поток (выход генератора). Остальные 10560 переменные — дополнительные, она введены для того, чтобы закодировать в КНФ все «эволюции» генератора, по которым из входа получается выход. Задача по известному выходу (т.е. значения последних 160 переменных известны) найти вход. Это и есть задача обращения генератора, как дискретной функции. Первые 64 перменные самые важные (мы их называем ядровыми), от них «информационно» зависят все остальные перменные КНФ. Мы создаем 2^31 (2 миллиарда) задач, в каждой из которых известны значения 31 переменных из 64 ядровых. Мы создаем 2^16 (65536) заданий, в каждой нужно решить 2^15 (32768) таких подзадач. Почти на все подзадачи из 2 миллиардов будет ответ, «выполняющего набора нет», только в нескольких (двух или трех) будет найден выполняющий набор (набор значений переменных, который при подстановке обращает КНФ в 1), каждому из которых соответствует инициализирующая последовательность (по сути, двоичный вектор длины 64), которая и является ответом на исходную задачу. В разделе Найденные решения в 16-ричном виде приведены значения найденных инициализирующих последовательностей генератора A5/1.
6. Зачем вообще нужно решать криптографические задачи?
Есть большая разница между исследованиями в области криптографии, организуемыми
а) спец. службами б) хакерами в) научными коллективами.
Мы относим себя только к к категории в). То, что делается в категориях а) и б), как правило, закрыто для мировой общественности. И реально используемые системы шифрования в основном исследуют как раз научные коллективы. Если бы уязвимость в шифре нашли хакеры, они бы могли этим воспользоваться в корыстных целях, мы же публикуем результаты в научной печати, в том числе в англоязычных журналах. Тем самым мы даем возможность учесть найденные уязвимости при разработке следующего поколения шифров.
Кроме того, криптографические задачи — это база аргументированно трудных тестов, позволяющая развивать технологии решения крупномасштабных задач с использованием распределенных вычислений. А вообще наш проект не направлен на решение только криптографических задач.
7. Почему время решения заданий варьируется от 1 часа до 10 часов?
В теории сложности алгоритмов есть понятие числа шагов, которое совершает алгоритм, получая на входные данные некоторой фиксированной длины. Зачастую алгоритм может на различных входах одной и той же длины совершать различное число шагов. В некоторых алгоритмах эта разница может быть весьма существенной. Алгоритмы, используемые в SAT@home, относятся именно к этому типу алгоритмов.
8. Предполагается ли закрытие проекта после завершения текущего эксперимента?
В обозримом будущем закрывать проект не предполагается, т. к. имеется целый ряд задач, которые планируется в нем решать.
9. Какие задачи будут решаться в проекте после решения серии задач криптоанализа генератора A5/1?
Планируется решать задачу поиска тройки взаимно ортогональных латинских квадратов размерности 10. В дальнейшем предполагается использовать SAT@home для решения некоторых задач комбинаторной оптимизации (например квадратичной задачи о назначениях).
10. Зачем нужно решать задачу поиска тройки взаимно ортогональных латинских квадратов?
Данная задача интересна сама по себе, поскольку это своего рода вызов человеческому интеллекту. Впервые она сформулирована еще Л. Эйлером в XVIII веке. На текущий момент минимальная размерность, для которой неизвестно существование тройки попарно ортогональных латинских квадратов, равна 10. Несмотря на то, что данная размерность кажется маленькой, комбинаторная сложность этой задачи весьма высока. Предварительные эксперименты позволяют нам надеяться, что эти задачи удастся решить в проекте SAT@home. Кроме того, у нее есть практические приложения. Многие используемые на практике комбинаторные конструкции, например некоторые классы кодов, исправляющих ошибки при передаче информации, теснейшим образом связаны с латинскими квадратами. Имеется связь латинских квадратов с задачами планирования экспериментов, а также с различными головоломками, например Sudoku.
11. Предполагается ли сделать версию приложения для GPU?
В данный момент мы активно работаем над этой проблемой. Все осложняется ограничениями архитектуры GPU, препятствующими эффективной реализации в них нехронологоического варианта алгоритма DPLL (наиболее эффективного на данный момент алгоритма решения SAT задач). В ближайшее время предполагается изучение с помощью добровольных тестеров хронологической GPU версии алгоритма DPLL. Это поможет понять, реально ли получить ускорение на GPU по сравнению CPU в рамках SAT@home хотя бы для некоторых классов тестов.
12. Как можно помочь проекту?
Мы с большой благодарностью принимаем любую помощь. На данный момент особо актуальным является привлечение новых пользователей и разъяснение им базовых принципов добровольных вычислений, а также целей и особенностей проекта SAT@home.
Проект активно обсуждается на следующих ресурсах, где пользователи высказывают немало ценных предложений: