What: | Lecture |
When: | Sunday, 17 March 2013, 15:35–17:10 |
Where: | ПОМИ РАН |
Slides: | csseminar_lecture_170313.pdf |
DPLL алгоритмы (алгоритмы расщепления) — один из основных подходов к решению задачи выполнимости пропозициональных формул (задачи SAT). На вход алгоритм получает формулу, на выход выдает выполняющий набор либо сообщение о том, что формула невыполнима. Он действует рекурсивно, выбирая переменную и присваиваемое ей значение и вызывая себя на формуле, получившейся при подстановке. Если выполняющий набор не найден, переменной присваивается другое значение и происходит еще один рекурсивный вызов. Работу такого алгоритма можно представить как дерево (дерево расщепления
). DPLL алгоритм характеризуется двумя процедурами (эвристиками): A, выбирающей переменную для расщепления, и B, выбирающей первое присваиваемое этой переменной значение. Можно рассмотреть такую модификацию, как DPLL алгоритм с отсечением, т.е., добавить эвристику C, обрезающую ветви
дерева расщепления: если C возвращает 0, то алгоритм вместо рекурсивных вызовов сразу выдает, что формула невыполнима. В таком случае, алгоритм может ошибаться на выполнимых формулах. В докладе будет рассмотрен случай, когда B и C — вероятностные процедуры. Будет показано, что если для выполнимой формулы, построенной по матрице смежности граничного экспандера, вероятность ошибки мала, то велика вероятность того, что алгоритм будет работать экспоненциально долго.