4511
правок
K-КНФ-алгоритмы на основе поиска с возвратом: различия между версиями
Перейти к навигации
Перейти к поиску
K-КНФ-алгоритмы на основе поиска с возвратом (посмотреть исходный код)
Версия от 23:20, 24 февраля 2018
, 24 февраля 2018→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 19: | Строка 19: | ||
Алгоритм ResolveSat использует следующую процедуру, которая принимает на вход произвольное присваивание y, КНФ-формулу F и перестановку | Алгоритм ResolveSat использует следующую процедуру, которая принимает на вход произвольное присваивание y, КНФ-формулу F и перестановку <math>\pi \;</math> и выполняет присваивание u. Присваивание u получается путем рассмотрения переменных y в порядке, заданном <math>\pi \;</math>, и изменении их значений в попытке обеспечить выполнимость формулы F. | ||
Функция Modify(КНФ-формула G( | Функция Modify(КНФ-формула <math>G(x_1, x_2, ..., x_n) \;</math>, перестановка <math>\pi \;</math> = ({1, 2, ..., n}, присваивание y) <math>\to</math> (присваивание u) | ||
<math>G_0 = G</math>. | |||
for i = 1 to n | '''for''' i = 1 '''to''' n | ||
if | '''if''' <math>G_{i - 1}</math> содержит единичный дизъюнкт <math>x_{\pi (i)}</math> | ||
else if | '''then''' <math>u_{\pi(i)} = 1</math> | ||
else | '''else''' '''if''' <math>G_{i - 1}</math> содержит единичный дизъюнкт <math>\bar{x}_{\pi (i)}</math> | ||
'''then''' <math>u_{\pi(i)} = 0</math> | |||
'''else''' <math>u_{\pi(i)} = y_{\pi(i)}</math> | |||
Gi = G;_i Ujr(i)=Kjr(i) | Gi = G;_i Ujr(i)=Kjr(i) | ||
end /* end for loop */ return U; | end /* end for loop */ return U; | ||