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

Перейти к навигации Перейти к поиску
Строка 50: Строка 50:




ResolveSat получается в результате сочетания Search с шагом предварительной обработки, заключающейся в ограниченном разложении формулы. Между дизъюнктами Q и C2, Q и C2 возникает конфликт на переменной v, если один из них содержит v, а другой – v. C1 и C2 представляют собой разложимую пару, если они конфликтуют точно на одной переменной v. Для таких пар их резольвентой, обозначаемой R(C1, C2), будет являться дизъюнкт C = D1 _ D2, где D1 и D2 получаются удалением v и v из C1 и C2, соответственно. Легко заметить, что любое присваивание, при котором C1 и C2 выполнимы, приводит также и к выполнимости C. Следовательно, если F выполнимой КНФ-формулой, содержащей разложимую пару C1, C2, то формула F0 = F Л R(C1 ; C2) будет иметь те же удовлетворяющие условию выполнимости присваивания, что и F. Разложимая пара C1, C2 является s-ограниченной, если  j C1 j ; j C2j < s и jR(C1 ; C2)j < s. Следующая процедура расширяет формулу F до формулы Fs, применяя s-ограниченное разложение максимально возможное количество раз.
Алгоритм '''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-ограниченное разложение максимально возможное количество раз.




Источник — http://pco.iis.nsk.su/wega/index.php/K-КНФ-алгоритмы_на_основе_поиска_с_возвратом