4501
правка
Алгоритмы локального поиска для k-КНФ: различия между версиями
Перейти к навигации
Перейти к поиску
Алгоритмы локального поиска для k-КНФ (посмотреть исходный код)
Версия от 11:50, 6 апреля 2018
, 6 апреля 2018→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 3: | Строка 3: | ||
== Основные результаты == | == Основные результаты == | ||
В длинном списке алгоритмов для k-SAT алгоритм Шонинга [11] стал революционным прорывом. Это стандартный подход с использованием локального поиска, и сам по себе алгоритм не был новинкой (см., например, [7]). Предположим, что y – текущее присваивание (его начальное значение равномерно выбирается случайным образом). Если присваивание y обеспечивает выполнимость формулы, алгоритм выдает ответ «Да» и завершает работу. В противном случае имеется по меньшей мере один дизъюнкт, литералы которого на присваивании y имеют значение «ложь». Выберем такой произвольный дизъюнкт и выберем случайным образом один из трех литералов. Затем изменим значение этой переменной на противоположное («истина» на «ложь» и наоборот), заменим y этим новым присваиванием и повторим ту же процедуру. | |||
Более формально алгоритм выглядит следующим образом: | |||
'''SCH'''(КНФ-формула F, целое I) | |||
'''repeat''' I раз | |||
y = равномерно выбранный случайный вектор <math>\in \{ 0, 1 \}^n \;</math> | |||
z = '''RandomWalk'''(F, y); | |||
'''if''' z приводит к выполнимости F | |||
'''then''' output(z); exit; | |||
'''end''' | |||
output(«Невыполнима»); | |||
'''RandomWalk'''(КНФ-формула <math>G(x_1, x_2, ..., x_n) \;</math>, присваивание y); | |||
y' = y; | |||
'''for''' 3n раза | |||
'''if''' y' приводит к выполнимости G | |||
'''then return''' y'; exit; | |||
C <math>\to</math> an arbitrary clause of G that is not satisfied | |||
by y0 ; | |||
Modify y0 as follows: | |||
select one literal of C uniformly at random and | |||
flip the assignment to this literal; | |||
end | |||
return y0 | |||