About convergence of a hybrid SAT+ROBDD-derivation.pdf Проблема обращения дискретных функций возникает во многих теоретических иприкладных областях современной кибернетики. Пусть / : {0,1}* ^ {0,1}* - вычис-лимая детерминированным образом за полиномиальное от длины входа время дискрет-ная функция. Если А ( / ) - некоторый полиномиальный алгоритм, вычисляющий /,то А ( / ) задает семейство функций вида /п : { 0 , 1 } n ^ {0,1}* , n Е N. Задача обраще-ния произвольной функции /п из данного семейства состоит в следующем: известноy Е Range / n , требуется, зная текст программы А ( / ) , найти произвольный x Е { 0 , 1 } n,такой, что / n ( x ) = y. Описанная задача является вычислительно трудной в общейпостановке - она не может быть решена за полиномиальное время в предположении,что P = NP. Поскольку различные практические задачи могут рассматриваться какчастные случаи сформулированной, разработка вычислительных алгоритмов для еёрешения является актуальной областью.Описанную проблему можно сводить к SAT-задачам [1], используя эффективныеалгоритмы трансляции программ в булевы уравнения (см., например, [2]). Для реше-ния получаемых SAT-задач можно использовать различные методы, лучшие из ко-торых базируются на алгоритме DPLL. В КНФ, получаемой в процессе трансляцииалгоритма A ( / n ) , можно выделить множество X n , состоящее из n так называемых «пе-ременных входа» рассматриваемой функции. Мощность данного множества равна n.В [3] говорится о том, что Xn является «сильной формой» множества-лазейки для ал-горитма DPLL, который применяется к КНФ C ( / n ) , кодирующей задачу обращения /п1 Работа выполнена при поддержке гранта РФФИ № 11-07-00377-a.в произвольной точке (в [3] используется термин «strong unit propagation backdoor set»,SUPBS). Данный факт в [3] полагается «интуитивно ясным» и приводится без дока-зательства. В работе [4] дано понятие ядра DPLL-вывода, которое является по сутианалогом понятия SUPBS, а также доказано, что множество переменных, кодирую-щих вход рассматриваемой функции /n , образует ядро DPLL-вывода в применениик КНФ C(/n ) . Это означает, что ограниченный вариант нехронологического DPLL, ко-торый выбирает переменные только из Xn , является полным и может использоватьсядля решения задачи обращения рассматриваемой функции. Такой алгоритм получилназвание core-DPLL. В [4] отмечено, что core-DPLL должен порождать избыточныеограничения. Данный тезис целиком подтвердился вычислительными эксперимента-ми. В связи с этим в работе [5] описан гибридный SAT+ROBDD-логический вывод,в котором core-DPLL используется для накопления баз конфликтных дизъюнктов, со-ставленных из литералов только над переменными ядра. Каждая такая конфликтнаябаза имеет вид КНФ и задает тем самым булеву функцию, для которой строится еёROBDD-представление. В дальнейшем вывод работает как на исходной КНФ, так и наконфликтной части, но представленной в форме ROBDD. Для этой цели в [5] введеныаналоги основных механизмов вывода, используемых в современных SAT-решателях,основанных на DPLL. В [5] описан также новый SAT-решатель с параллельной архи-тектурой, в котором реализован гибридный SAT+ROBDD-вывод. Данный решательсущественно превзошёл по эффективности известные решатели на SAT-задачах, ко-дирующих обращение некоторых криптографических функций.В докладе представлено новое свойство гибридного SAT+ROBDD-вывода, а именноего сходимость относительно числа путей в терминальную единицу в ROBDD, пред-ставляющей базу конфликтных ограничений.Гибридная SAT+ROBDD-стратегия логического вывода в применении к C(/n)представляет собой процесс, разделенный на итерации [5]. На начальной итерации core-DPLL накапливает некоторое множество конфликтных дизъюнктов - D , . . . , D . Да-лее строится ROBDD B1, представляющая булеву функцию, заданную КНФ Dj.. . - D .Дальнейший вывод является гибридным - задействуется как КНФ-часть (собствен-но C(/n ) ) , так и ROBDD-часть. Если Br - ROBDD-представление конфликтной базы,построенной на итерации с номером r, а на итерации с номером r + 1 гибридный выводпорождает дизъюнкты D ^ 1 , . . . , D[+1, то ROBDD Br+1 естьBr+1 = Apply (Br DT+1 ... D + i )(используется алгоритм Apply [6]).Через B(g) обозначим число наборов значений истинности, на которых булевафункция g над множеством переменных X, представляемая ROBDD B(g), принимаетзначение 1. Справедлив следующий результат.Теорема 1. Пусть C - произвольная КНФ над множеством X. Предположим,что на C осуществляется s итераций гибридного SAT+ROBDD-вывода и B1 , . . . , Bs -ROBDD-представления баз конфликтных дизъюнктов, построенные на соответствую-щих итерациях. Если для некоторого k Е { 1 , . . . , s } множество вершин B& исчерпыва-ется терминальным нулем, то C невыполнима. В противном случае для произвольногоk Е { 2 , . . . , s} имеет место Bk < Bk-1.

Скачать электронную версию публикации