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

Перейти к навигации Перейти к поиску
Строка 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
4501

правка

Навигация