Определение алгоритма DPLL

Question

У меня возникли некоторые проблемы с пониманием алгоритма DPLL, и мне было интересно, может ли кто-нибудь объяснить мне это, потому что я думаю, что мое понимание неверно.

Насколько я понимаю, я беру некоторый набор литералови если какое-то каждое условие истинно, то модель истинно, но если какое-то условие ложно, то модель ложна.

Я рекурсивно проверяю модель, ища предложение единицы, если есть одно, я устанавливаю значение дляэто предложение модуля, чтобы сделать его истинным, а затем обновить модель.Удаление всех предложений, которые теперь являются истинными, и удаление всех литералов, которые теперь являются ложными.

Когда не осталось ни одного предложения блока, я выбрал любой другой литерал и назначил значения для этого литерала, которые делают его истинным и делают его ложным,затем снова удалите все предложения, которые теперь являются истинными, и все литералы, которые теперь являются ложными.

Answer 1

DPLL требует, чтобы проблема была изложена в дизъюнктивной нормальной форме, то есть в виде набора положений, каждое из которых должно быть удовлетворено.

Каждое предложение представляет собой набор литералов {l1, l2, ..., ln}, представляющих дизъюнкцию этих литералов (т. Е. По крайней мере один литерал должен быть истинным, чтобы условие было выполнено).

Каждый литерал l утверждает, что некоторая переменная истинна (x) или ложна (~x).

Если какой-либо литерал является истинным в предложении, то условие удовлетворяется.

Если все литералы в предложении являются ложными, то предложение является неудовлетворительным и, следовательно, проблема неудовлетворительной.

Решением является присвоение значений true / false переменным таким образом, чтобы выполнялось каждое предложение. Алгоритм DPLL - это оптимизированный поиск такого решения.

DPLL - это поиск в глубину, который чередуется между тремя тактиками. На любом этапе поиска есть частичное присваивание (то есть присваивание значений некоторому подмножеству переменных) и набор неопределенных предложений (то есть тех предложений, которые еще не были выполнены).

(1) Первой тактикой является «Чистое литеральное исключение»: если неназначенная переменная x появляется только в положительном виде в наборе неопределенных предложений (т. Е. Литерал ~x нигде не появляется), тогда мы можем просто добавьте x = true к нашему назначению и удовлетворите все пункты, содержащие литерал x (аналогично, если x появляется только в его отрицательной форме, ~x, мы можем просто добавить x = false к нашему назначению).

(2) Вторая тактика - «Распространение юнитов»: если все, кроме одного из литералов в неопределенном предложении, ложны, то оставшийся должен быть верным. Если оставшийся литерал равен x, мы добавляем x = true к нашему назначению; если оставшийся литерал равен ~x, мы добавляем x = false к нашему назначению. Это назначение может привести к дальнейшим возможностям распространения юнита.

(3) Третья тактика - просто выбрать неназначенную переменную x и продолжить поиск: одна сторона пытается x = true, другая - x = false.

Если в какой-то момент мы получим неудовлетворительное предложение, то мы зашли в тупик и должны вернуться назад.

Существует множество других хитроумных оптимизаций, но это является ядром почти всех решателей SAT.

Надеюсь, это поможет.

Answer 2

Алгоритм Дэвиса – Путнэма – Логемана – Лавленда (DPLL) - это алгоритм поиска на основе обратного отслеживания для определения выполнимости логических формул высказываний в конъюнктивной нормальной форме, также известный как проблема выполнимости или SAT.

Любая логическая формула может быть выражена в конъюнктивной нормальной форме (CNF), что означает соединение предложений, т. Е. (…) ^ (…) ^ (…)

где предложение является дизъюнкцией булевых переменных, т. Е. (A v B v C ’v D)

пример булевой формулы, выраженной в CNF:

(A v B v C) ^ (C ’v D) ^ (D’ v A)

и решение проблемы SAT означает поиск комбинации значений для переменных в формуле, которые удовлетворяют ей, например, A = 1, B = 0, C = 0, D = 0

Это проблема NP-Complete. На самом деле это первая проблема, доказанная NP-Complete Стивеном Куком и Леонидом Левиным

Конкретным типом проблемы SAT является 3-SAT, который представляет собой SAT, в котором все предложения имеют три переменные.

Алгоритм DPLL является способом решения проблемы SAT (которая практически зависит от твердости ввода), которая рекурсивно создает дерево потенциального решения

Предположим, вы хотите решить проблему 3-SAT следующим образом

(A v B v C) ^ (C ’v D v B) ^ (B v A’ v C) ^ (C ’v A’ v B ’)

если мы перечислим такие переменные, как A = 1 B = 2 C = 3 D = 4 и найдем отрицательные числа для отрицательных переменных, таких как A ’= -1, то такую ​​же формулу можно написать на Python, например, так:

[[1,2,3], [- 3,4,2], [2, -1,3], [- 3, -1, -2]]

Теперь представьте, что вы создали дерево, в котором каждый узел состоит из частичного решения. В нашем примере мы также изобразили вектор предложений, удовлетворяемых решением

корневым узлом является [-1, -1, -1, -1], что означает, что никакие значения еще не были присвоены переменным ни 0, ни 1

на каждой итерации:

1. мы берем первое неудовлетворенное предложение, затем

2. если больше нет неназначенных переменных, которые мы можем использовать для удовлетворения этого условия, тогда в этой ветви дерева поиска не может быть допустимых решений, и алгоритм должен вернуть None

3. в противном случае мы берем первую неназначенную переменную и устанавливаем ее так, чтобы она удовлетворяла условию, и начинаем рекурсивно с шага 1. Если внутренний вызов алгоритма возвращает None, мы переворачиваем значение переменной так, чтобы она не удовлетворяла предложение и установите следующую неназначенную переменную, чтобы удовлетворить предложение. Если все три переменные были опробованы или для этого предложения больше нет неназначенной переменной, это означает, что в этой ветви нет допустимых решений, и алгоритм должен вернуть None

См. Следующий пример:

из корневого узла мы выбираем первую переменную (A) первого предложения (A v B v C) и устанавливаем ее так, чтобы она удовлетворяла предложению, тогда A = 1 (второй узел дерева поиска)

продолжить со вторым предложением, и мы выбираем первую неназначенную переменную (C) и устанавливаем ее так, чтобы она удовлетворяла предложению, что означает C = 0 (третий узел слева)

мы делаем то же самое для четвертого предложения (B v A ’v C) и устанавливаем B в 1

мы пытаемся сделать то же самое для последнего предложения, которое мы понимаем, что у нас больше нет неназначенных переменных, и предложение всегда ложно. Затем мы должны вернуться к предыдущей позиции в дереве поиска. Мы изменяем значение, которое мы присвоили B, и устанавливаем B на 0. Затем мы ищем другое неназначенное значение, которое может удовлетворить третье предложение, но его нет. Затем мы должны вернуться обратно ко второму узлу

Оказавшись там, мы должны перевернуть присвоение первой переменной (C), чтобы оно не удовлетворяло предложению, и установить следующую неназначенную переменную (D), чтобы удовлетворить ее (то есть C = 1 и D = 1 ). Это также удовлетворяет третьему пункту, который содержит C.

Последний пункт для удовлетворения (C ’v A ’v B’) имеет одну неназначенную переменную B, которую затем можно установить в 0 для удовлетворения условия.

В этой ссылке http://lowcoupling.com/post/72424308422/a-simple-3-sat-solver-using-dpll вы также можете найти код Python, реализующий его