WalkSAT - WalkSAT
В информатике , GSAT и WalkSAT являются локальные поисковые алгоритмы для решения логических задач выполнимости .
Оба алгоритма работает по формулам в булевой логике , которые находятся в, или были преобразованы в КНФ . Они начинают с присвоения случайного значения каждой переменной в формуле. Если присвоение удовлетворяет всем предложениям , алгоритм завершается, возвращая присвоение. В противном случае переменная переворачивается, а затем повторяется вышеупомянутое до тех пор, пока все предложения не будут удовлетворены. WalkSAT и GSAT различаются методами, используемыми для выбора переменной для преобразования.
GSAT вносит изменение, которое сводит к минимуму количество невыполненных предложений в новом назначении или с некоторой вероятностью выбирает переменную случайным образом.
WalkSAT сначала выбирает предложение, которое не удовлетворяется текущим назначением, затем меняет значение переменной в этом предложении. Предложение выбирается случайным образом среди неудовлетворенных предложений. Выбирается переменная, что приведет к тому, что наименьшее количество ранее удовлетворенных предложений станет неудовлетворенным, с некоторой вероятностью случайного выбора одной из переменных. При случайном выборе WalkSAT гарантирует, по крайней мере, шанс одной из переменных, указанных в предложении, исправить некорректное присвоение. При выборе предполагаемой оптимальной переменной WalkSAT должен производить меньше вычислений, чем GSAT, потому что он рассматривает меньше возможностей.
Алгоритм может перезапуститься с новым случайным назначением, если решение не было найдено слишком долго, в качестве способа выхода из локальных минимумов количества невыполненных предложений.
Существует множество версий GSAT и WalkSAT. WalkSAT оказался особенно полезным в решении проблем выполнимости, возникающих при преобразовании из задач автоматического планирования . Подход к планированию, который преобразует проблемы планирования в проблемы булевой выполнимости, называется сатпланом .
MaxWalkSAT - это вариант WalkSAT, предназначенный для решения задачи взвешенной выполнимости , в которой каждое предложение связано с весом, а цель состоит в том, чтобы найти назначение - такое, которое может или не может удовлетворять всей формуле - которое максимизирует общий вес пункты, удовлетворяемые этим назначением.
Ссылки
- Генри Каутц и Б. Селман (1996). Расширяя границы: планирование, логика высказываний и стохастический поиск . В материалах тринадцатой национальной конференции по искусственному интеллекту (AAAI'96) , страницы 1194–1201.
- Пападимитриу, Христос Х. (1991), «О выборе удовлетворительного задания истины», Труды 32-го ежегодного симпозиума по основам компьютерных наук , стр. 163–169, doi : 10.1109 / SFCS.1991.185365 , ISBN 978-0-8186-2445-2.
- Шёнинг, У. (1999), «Вероятностный алгоритм для k -SAT и задач удовлетворения ограничений», Труды 40-го ежегодного симпозиума по основам компьютерных наук , стр. 410–414, CiteSeerX 10.1.1.132.6306 , doi : 10.1109 / SFFCS.1999.814612 , ISBN 978-0-7695-0409-4.
- Б. Селман и Генри Каутц (1993). Доменно-независимое расширение GSAT: решение больших проблем структурированной выполнимости . В материалах тринадцатой международной совместной конференции по искусственному интеллекту (IJCAI'93) , страницы 290–295.
- Барт Селман , Генри Каутц и Брэм Коэн . «Стратегии местного поиска для проверки выполнимости». Окончательная версия опубликована в книге «Клики, раскраска и соответствие: вторая задача внедрения DIMACS», 11–13 октября 1993 г. Дэвид С. Джонсон и Майкл А. Трик , ред. Серия DIMACS по дискретной математике и теоретической информатике, т. 26, AMS, 1996.
- Б. Селман, Х. Левеск и Д. Митчелл (1992). Новый метод решения сложных проблем выполнимости . В материалах Десятой национальной конференции по искусственному интеллекту (AAAI'92) , страницы 440–446.