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
Здесь мы перевернем переменную, которая максимизирует количество удовлетворенных предложений. Как это сделать эффективно? Наивный метод состоит в том, чтобы перевернуть каждую переменную, и для каждого шага через все пункты и вычислить, сколько из них будет удовлетворено. Даже если предложение может быть запрошено на соответствие в постоянное время, простой метод все равно будет выполняться за время , где V - количество переменных, а C - количество предложений. Я уверен, что мы можем сделать лучше, поэтому вопрос:
Многие алгоритмы локального поиска переворачивают присвоение переменной, которое максимизирует количество удовлетворенных предложений. На практике, с какими структурами данных эта операция поддерживается эффективно?
Это то, что я чувствую, что учебники часто опускаются. Одним из примеров является даже знаменитая книга Рассела и Норвиг .
Ответы:
Необходимая структура данных - это список событий , список для каждой переменной, содержащий предложения, в которых эта переменная встречается. Эти списки создаются один раз, когда CNF впервые читается. Они используются в шагах 3 и 5 ниже, чтобы избежать сканирования всей формулы CNF для подсчета удовлетворенных предложений.
Лучший алгоритм, чем переключение каждой переменной:
Ссылкой на структуру данных (часто также называемой списком смежности) являются, например, Lynce и Marques-Silva, Efficient Data Structures for Backtracking SAT solvers, 2004.
источник