Поддержка структур данных для локального поиска SAT

Question

Walksat и GSAT являются известными и простыми локальными алгоритмами поиска для решения проблемы логической удовлетворенности. Псевдокод для алгоритма GSAT копируется из вопроса Реализация алгоритма GSAT - как выбрать, какой букваль переворачивается? и представлено ниже.

procedure GSAT(A,Max_Tries,Max_Flips)
  A: is a CNF formula
  for i:=1 to Max_Tries do
    S <- instantiation of variables
    for j:=1 to Max_Iter do
      if A satisfiable by S then
        return S
      endif
      V <- the variable whose flip yield the most important raise in the number of satisfied clauses;
      S <- S with V flipped;
    endfor
  endfor
  return the best instantiation found
end GSAT

Здесь мы переворачиваем переменную, которая максимизирует количество удовлетворенных положений. Как это делается эффективно? Наивный метод состоит в том, чтобы перевернуть каждую переменную, и для каждого шага через все предложения и рассчитать, сколько из них удовлетворяется. Даже если пункт может быть запрошен за удовлетворенность в постоянное время, наивный метод все равно будет работать во время $ O (VC) $, где $ V $ - это количество переменных и $ C $ количество пунктов. Я уверен, что мы можем добиться большего успеха, отсюда и вопрос:

Многие локальные алгоритмы поиска переворачивают назначение переменной, которая максимизирует количество удовлетворенных предложений. На практике, с какими структурами данных эффективно поддерживается?

Это то, что я чувствую, как учебники часто пропускают. Один пример даже знаменитый Книга Рассела и Норвига.

Answer 1

Необходимая структура данных является произойти список, список для каждой переменной, содержащей предложения, в которых происходит переменная. Эти списки строятся один раз, когда CNF сначала считывается. Они используются в шагах 3 и 5 ниже, чтобы избежать сканирования всей формулы CNF, чтобы считать удовлетворенные предложения.

Лучший алгоритм, чем перевернуть каждую переменную:

1. Составьте список только тех переменных, которые встречаются в неудовлетворенных положениях.
2. Выберите переменную $ x $ из этого списка.
3. Подсчитайте, сколько положений, содержащих $ x $, удовлетворено.
4. Flip $ x $.
5. Подсчитайте, сколько положений, содержащих $ x $, удовлетворено.
6. Untfip $ x $.
7. Вычтите результат шага 3 из шага 5 и запишите его за $ x $.
8. Повторите шаги 2-7 для остальных переменных, найденных на шаге 1.
9. Переверните переменную с наибольшим числом, записанным на шаге 7.

Например, ссылка на структуру данных (часто также известная как список смежности) Lynce и Marques-Silva, эффективные структуры данных для обратного перехода SAT решателей, 2004.