улучшение производительности алгоритма dpll
Я реализую DPLL алгоритм в C ++, как описано в википедия:
function DPLL(Φ)
if Φ is a consistent set of literals
then return true;
if Φ contains an empty clause
then return false;
for every unit clause l in Φ
Φ ← unit-propagate(l, Φ);
for every literal l that occurs pure in Φ
Φ ← pure-literal-assign(l, Φ);
l ← choose-literal(Φ);
return DPLL(Φ ∧ l) or DPLL(Φ ∧ not(l));
но иметь ужасную производительность. На этом этапе:
return DPLL(Φ ∧ l) or DPLL(Φ ∧ not(l));
В настоящее время я пытаюсь избежать создания копий Φ но вместо добавления l или же not(l) к единственной копии Φ и удалите их, когда / если DPLL()возвращение false, Это, кажется, нарушает алгоритм, дающий неправильные результаты (UNSATISFIABLE хотя набор SATISFIABLE).
Любые предложения о том, как избежать явных копий на этом этапе?
Решение
Менее наивный подход к DPLL позволяет избежать копирования формулы путем записи назначений переменных и изменений, внесенных в предложения в шагах распространения единиц и чисто литеральных назначений, а затем отменяет изменения (возвратные пути) при создании пустого предложения. Так что, когда переменная Икс присвоено значение true, вы бы отметили все предложения, содержащие положительный литерал Икс как неактивные (и игнорировать их после этого, так как они удовлетворены) и удалить -Икс из всех пунктов, которые его содержат. Запишите, какие пункты -Икс в них, чтобы вы могли вернуться позже. Также запишите, какие пункты вы отметили как неактивные по той же причине.
Другой подход заключается в отслеживании количества неназначенных переменных в каждом неудовлетворенном предложении. Запишите, когда число уменьшится, чтобы вы могли вернуться позже. Распространение юнитов, если число достигает 1, возврат в обратном направлении, если число достигает 0 и все литералы ложны.
Я написал «менее наивно» выше, потому что есть еще лучшие подходы. Современные SAT-решатели типа DPLL используют схему обновления ленивых предложений, называемую «двумя наблюдаемыми литералами», которая имеет то преимущество, что нет необходимости удалять литералы из предложений и, следовательно, не нужно восстанавливать их при обнаружении неверного назначения. Присвоение переменных все еще должно быть записано и отслежено, но отсутствие необходимости обновления структур, связанных с предложениями, делает два наблюдаемых литерала быстрее, чем любая другая известная схема обратного отслеживания для решателей SAT. Вы, без сомнения, узнаете об этом позже в своем классе.
Другие решения
Других решений пока нет …