K-КНФ-алгоритмы на основе поиска с возвратом: различия между версиями

   output("Невыполнимо");

Алгоритм '''ResolveSat''' получается в результате сочетания '''Search''' с шагом предварительной обработки, заключающейся в ''ограниченном разложении'' формулы. Между дизъюнктами <math>C_1 \;</math> и <math>C_2 \;</math> возникает ''конфликт'' на переменной v, если один из них содержит v, а другой – <math>\bar{v}</math>. <math>C_1 \;</math> и <math>C_2 \;</math> представляют собой ''разложимую пару'', если они конфликтуют точно на одной переменной v. Для таких пар их ''резольвентой'', обозначаемой <math>R(C_1, C_2) \;</math>, будет являться дизъюнкт <math>C = D_1 \vee D_2 \;</math>, где <math>D_1 \;</math> и <math>D_2 \;</math> получаются удалением v и <math>\bar{v}</math> из <math>C_1 \;</math> и <math>C_2 \;</math>, соответственно. Легко заметить, что любое присваивание, при котором <math>C_1 \;</math> и <math>C_2 \;</math> выполнимы, влечет также и выполнимость C. Следовательно, если F является выполнимой КНФ-формулой, содержащей разложимую пару <math>C_1 \;</math>, <math>C_2 \;</math>, то формула <math>F' = F \wedge R(C_1, C_2)</math> будет иметь те же удовлетворяющие условию выполнимости присваивания, что и F. Разложимая пара <math>C_1, C_2 \;</math> является ''s-ограниченной'', если  <math>|C_1|, |C_2| \le s</math> и <math>|R(C_1, C_2)| \le s</math>. Следующая процедура расширяет формулу F до формулы <math>F_s \;</math>, применяя s-ограниченное разложение максимально возможное количество раз.

Resolve(КНФ-формула F, целое число s)

while Fs содержит s-ограниченную разложимую пару C1, C2

 

ResolveSat(КНФ-формула F, целое число s, целое положительное число I)

 

Fs =Resolve(F, s).

 

Search(Fs, I).

Время выполнения ResolveSat(F, s, I) можно ограничить следующим образом. Resolve(F, s) добавляет не более O(ns) дизъюнктов к F за счет сравнения пар дизъюнктов, так что прямолинейная реализация будет выполняться за время n3spoly(n) (эту границу можно улучшить, однако ее улучшение не повлияет на асимптотику основного результата). Search(Fs, I) требует I(jFj + ns)poly(n) времени. Следовательно, полное время выполнения ResolveSat(F, s, I) можно грубо ограничить сверху значением (n3s + I(jFj + ns))poly(n). If s = O(n/log n), общее время выполнения можно ограничить значением IjFj2O(n), поскольку ns = 2O(n). Для этого нужно взять в качестве s некоторую константу достаточно большой величины или медленно растущую функцию от n. Таким образом, s(n) будет стремиться к бесконечности с n, но будет оставаться в пределах O(log n).

В случае, если функция F оказывается невыполнимой, алгоритм Search(F, I) всегда выдает результат «невыполнима». Таким образом, единственной проблемой остается нахождение верхней границы в случае, когда F выполнима. Обозначим за x(F) вероятность того, что Modify(F it,y) найдет некоторое присваивание, обеспечивающее выполнимость. Тогда для выполнимой функции F вероятность ошибки Search(F, I) равна (1 - r(F))1 < e~It(F\, что не превышает e~" при условии I > nlx{F). Следовательно, достаточно получить хорошую верхнюю границу для T(F).