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

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




Алгоритм ResolveSat использует следующую процедуру, которая принимает на вход произвольное присваивание y, КНФ-формулу F и перестановку ж и выполняет присваивание u. Присваивание u получается путем рассмотрения переменных y в порядке, заданном ж, и изменении их значений в попытке обеспечить выполнимость формулы F.
Алгоритм ResolveSat использует следующую процедуру, которая принимает на вход произвольное присваивание y, КНФ-формулу F и перестановку <math>\pi \;</math> и выполняет присваивание u. Присваивание u получается путем рассмотрения переменных y в порядке, заданном <math>\pi \;</math>, и изменении их значений в попытке обеспечить выполнимость формулы F.




Функция Modify(КНФ-формула G(x1, x2, ... .  xn), перестановка ж = {1, 2, ..., n}, присваивание y) — ■> (присваивание u)
Функция Modify(КНФ-формула <math>G(x_1, x_2, ..., x_n) \;</math>, перестановка <math>\pi \;</math> = ({1, 2, ..., n}, присваивание y) <math>\to</math> (присваивание u)


G’ = G.
  <math>G_0 = G</math>.
for i = 1 to n
  '''for''' i = 1 '''to''' n
if Gj-i единичный дизъюнкт хлщ then ul(i) = 1
      '''if''' <math>G_{i - 1}</math> содержит единичный дизъюнкт <math>x_{\pi (i)}</math>
else if Gj-i единичный дизъюнкт %(,) then иж(,) = 0
        '''then''' <math>u_{\pi(i)} = 1</math>
else ul(i) = yn(i)
      '''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;
Источник — http://pco.iis.nsk.su/wega/index.php/K-КНФ-алгоритмы_на_основе_поиска_с_возвратом