DPLL алгоритм с вероятностным отсечением: оценка времени работы

DPLL алгоритмы (алгоритмы расщепления) — один из основных подходов к решению задачи выполнимости пропозициональных формул (задачи SAT). На вход алгоритм получает формулу, на выход выдает выполняющий набор либо сообщение о том, что формула невыполнима. Он действует рекурсивно, выбирая переменную и присваиваемое ей значение и вызывая себя на формуле, получившейся при подстановке. Если выполняющий набор не найден, переменной присваивается другое значение и происходит еще один рекурсивный вызов. Работу такого алгоритма можно представить как дерево ("дерево расщепления"). DPLL алгоритм характеризуется двумя процедурами (эвристиками): A, выбирающей переменную для расщепления, и B, выбирающей первое присваиваемое этой переменной значение. Можно рассмотреть такую модификацию, как DPLL алгоритм с отсечением, т.е., добавить эвристику C, ''обрезающую ветви'' дерева расщепления: если C возвращает 0, то алгоритм вместо рекурсивных вызовов сразу выдает, что формула невыполнима. В таком случае, алгоритм может ошибаться на выполнимых формулах. В докладе будет рассмотрен случай, когда B и C — вероятностные процедуры. Будет показано, что если для выполнимой формулы, построенной по матрице смежности граничного экспандера, вероятность ошибки мала, то велика вероятность того, что алгоритм будет работать экспоненциально долго.

Описание лекции на сайте Computer Science клуба