September 9th, 2021

with Cat The Cat

Случайный поиск.

Вот пример решателя SAT, основанного на случайном поиске вокруг текущего присваивания: http://fmv.jku.at/yalsat/

Основной алгоритм у него таков:
  1. если нет неудовлетворённых ограничений, остановиться
  2. если есть неудовлетворённые ограничения, взять первое (или второе - или какое-то, там шесть эвристик) из очереди добавленных неудовлетворённых ограничений
  3. выбрать случайным образом литерал ограничения для изменения значения на противоположное
  4. изменить значение выбранного литерала на противоположное и пересчитать неудовлетворённые ограничения
Как легко заметить, мы не отмечаем путь и если мы два раза (четное количество раз) выбрали литерал одной и той же переменной, то мы будем крутиться на одном месте.

Типичный способ ведения пути это табу-список: мы ведём список нескольких последних переменных и запрещаем изменение значения переменной, если она в запрещённом списке. Для такого метода легко понять ограничения: если "окружность" задачи больше размера запрещённого списка, то мы не выйдем из локального минимума. Или мы можем сделать ненужные действия, если наш глобальный минимум (решение) ближе, чем размер запрещённого списка. Обычно, запрещённый список имеет размер в пару десятков переменных, а в задаче у нас пара сотен переменных.

Если же мы будем отмечать несколько сотен (тысяч, десятков, сотен тысяч или даже миллионов) конфигураций присваиваний (a ∧ b отличается от a ∧ -b - две разные конфигурации), то мы можем вести запрещённый список конфигураций в виде фильтра Блюма или хэша кукушки - очень близко к теоретическому минимуму и позволяя перещёлкивать переменные, если они приводят к действительно новому состоянию.

Таким образом мы приближаем локальный поиск к систематическому (DPLL). Мы вынуждены искать наиболее выгодные изменения состояния, которые мы ещё не посещали, что близко к DPLL.