4511
правок
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
Строка 50: | Строка 50: | ||
ResolveSat получается в результате сочетания Search с шагом предварительной обработки, заключающейся в ограниченном разложении формулы. Между дизъюнктами | Алгоритм '''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-ограниченное разложение максимально возможное количество раз. | ||
правок