4446
правок
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
Строка 57: | Строка 57: | ||
Алгоритм '''ResolveSat''' | Алгоритм '''ResolveSat''' | ||
Алгоритм '''ResolveSat''' по сути очень прост. Получив на вход формулу в k-КНФ, он вначале генерирует дизъюнкты, которые могут быть получены путем разложения, длина которых не превышает некоторой величины. Затем он | Алгоритм '''ResolveSat''' по сути очень прост. Получив на вход формулу в k-КНФ, он вначале генерирует дизъюнкты, которые могут быть получены путем разложения, длина которых не превышает некоторой величины. Затем он берет некоторый случайный порядок переменных и последовательно присваивает им значения согласно этому порядку. Если рассматриваемая в текущий момент переменная встречается в виде единичного дизъюнкта, ей присваивается единственное значение, при котором этот дизъюнкт выполним. Если она встречается в двух противоречащих друг другу единичных дизъюнктах, алгоритм начинает работу заново. На каждом этапе алгоритм также проверяет, выполнима ли формула. Если выполнима, то входной набор принимается. Процедура повторяется до тех пор, пока не будет найдено присваивание, приводящее к выполнимости формулы, либо пока не истечет выделенное время. | ||
'''ResolveSat''' использует следующую процедуру, которая принимает на вход произвольное присваивание y, КНФ-формулу F и перестановку <math>\pi \;</math> и выполняет присваивание u. Присваивание u получается путем рассмотрения переменных y в порядке, заданном <math>\pi \;</math>, и | '''ResolveSat''' использует следующую процедуру, которая принимает на вход произвольное присваивание y, КНФ-формулу F и перестановку <math>\pi \;</math> и выполняет присваивание u. Присваивание u получается путем рассмотрения переменных y в порядке, заданном <math>\pi \;</math>, и изменения их значений в попытке обеспечить выполнимость формулы F. | ||
Строка 77: | Строка 77: | ||
Алгоритм '''Search''' получается в результате выполнения | Алгоритм '''Search''' получается в результате выполнения процедуры '''Modify'''<math>(G, \pi, y) \;</math> на нескольких парах <math>(\pi, y) \;</math>, где <math>\pi \;</math> – случайная перестановка, а y – случайное присваивание. | ||
правок