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 , S2CID 206559488 .
- Шёнинг, У. (1999), «Вероятностный алгоритм для k -SAT и проблемы удовлетворения ограничений», Труды 40-го ежегодного симпозиума по основам информатики , стр. 410–414, CiteSeerX 10.1.1.132.6306 , doi : 10.1109/ SFFCS.1999.814612 , ISBN 978-0-7695-0409-4 , S2CID 1230959 .
- Б. Селман и Генри Каутц (1993). Независимое от предметной области расширение GSAT: решение больших проблем структурированной выполнимости . В материалах тринадцатой Международной совместной конференции по искусственному интеллекту (IJCAI'93) , страницы 290–295.
- Барт Селман , Генри Каутц и Брэм Коэн . «Стратегии локального поиска для тестирования на выполнимость». Окончательная версия опубликована в журнале «Клик, раскраска и выполнимость: вторая задача внедрения DIMACS», 11–13 октября 1993 г. Дэвид С. Джонсон и Майкл А. Трик , ред. Серия DIMACS по дискретной математике и теоретической информатике, том. 26 лет, АМН, 1996 г.
- Б. Селман, Х. Левеск и Д. Митчелл (1992). Новый метод решения сложных задач выполнимости . В материалах Десятой национальной конференции по искусственному интеллекту (AAAI'92) , страницы 440–446.