Алгоритмы GSAT и WalkSAT для решения задач выполнимости булевых формул.
WalkSAT
GSAT и WalkSAT: локальные алгоритмы поиска решений для задач выполнимости булевых формул. Работают с КНФ, случайным назначением переменных и перебором.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Введение
В информатике GSAT и WalkSAT — это локальные алгоритмы поиска для решения задач булевой выполнимости. Оба алгоритма работают с формулами булевой логики, представленными в конъюнктивной нормальной форме или преобразованными в неё. Они начинают с присвоения каждой переменной в формуле случайного значения. Если присвоение удовлетворяет всем дизъюнктам, алгоритм завершается, возвращая это присвоение. В противном случае, выбирается переменная и её значение меняется на противоположное, после чего процесс повторяется до тех пор, пока все дизъюнкты не будут удовлетворены. WalkSAT и GSAT различаются методами выбора переменной для изменения. GSAT вносит изменение, которое минимизирует количество неудовлетворенных дизъюнктов в новом присвоении, либо с некоторой вероятностью выбирает переменную случайным образом. WalkSAT сначала выбирает неудовлетворенный дизъюнкт текущим присвоением, а затем меняет значение переменной внутри этого дизъюнкта. Выбор дизъюнкта осуществляется случайным образом среди неудовлетворенных. Переменная выбирается так, чтобы изменение её значения привело к наименьшему числу ранее удовлетворенных дизъюнктов, ставших неудовлетворенными, с некоторой вероятностью случайного выбора одной из переменных. При случайном выборе WalkSAT гарантированно имеет хотя бы один шанс из числа переменных в дизъюнкте исправить текущее некорректное присвоение. При выборе переменной, предположительно оптимальной, WalkSAT требует меньше вычислений, чем GSAT, поскольку рассматривает меньше вариантов. Оба алгоритма могут перезапускаться с новым случайным присвоением, если решение не найдено за слишком долгое время, чтобы выйти из локальных минимумов числа неудовлетворенных дизъюнктов. Существует множество версий GSAT и WalkSAT. WalkSAT оказался особенно полезным при решении задач выполнимости, полученных в результате преобразования из задач автоматизированного планирования. Подход к планированию, преобразующий задачи планирования в задачи булевой выполнимости, называется satplan. MaxWalkSAT — это вариант WalkSAT, предназначенный для решения задачи взвешенной выполнимости, в которой каждому дизъюнкту соответствует вес, и цель состоит в том, чтобы найти такое присвоение (которое может удовлетворять или не удовлетворять всю формулу), которое максимизирует общий вес удовлетворенных дизъюнктов.
In computer science, GSAT and WalkSAT are local search algorithms to solve Boolean satisfiability problems. Both algorithms work on formulae in Boolean logic that are in, or have been converted into conjunctive normal form. They start by assigning a random value to each variable in the formula. If the assignment satisfies all clauses, the algorithm terminates, returning the assignment. Otherwise, a variable is flipped and the above is then repeated until all the clauses are satisfied. WalkSAT and GSAT differ in the methods used to select which variable to flip. GSAT makes the change which minimizes the number of unsatisfied clauses in the new assignment, or with some probability picks a variable at random. WalkSAT first picks a clause which is unsatisfied by the current assignment, then flips a variable within that clause. The clause is picked at random among unsatisfied clauses. The variable is picked that will result in the fewest previously satisfied clauses becoming unsatisfied, with some probability of picking one of the variables at random. When picking at random, WalkSAT is guaranteed at least a chance of one out of the number of variables in the clause of fixing a currently incorrect assignment. When picking a guessed to be optimal variable, WalkSAT has to do less calculation than GSAT because it is considering fewer possibilities. Both algorithms may restart with a new random assignment if no solution has been found for too long, as a way of getting out of local minima of numbers of unsatisfied clauses. Many versions of GSAT and WalkSAT exist. WalkSAT has been proven particularly useful in solving satisfiability problems produced by conversion from automated planning problems. The approach to planning that converts planning problems into Boolean satisfiability problems is called satplan. MaxWalkSAT is a variant of WalkSAT designed to solve the weighted satisfiability problem, in which each clause has associated with a weight, and the goal is to find an assignment—one which may or may not satisfy the entire formula—that maximizes the total weight of the clauses satisfied by that assignment.