WalkSAT
Encyclopedia
GSAT and WalkSat are local search
algorithm
s to solve Boolean satisfiability problems
.
Both algorithms work on formulae that are in, or have been converted into, conjunctive normal form
. They start by assigning a random value to each variable. 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 generally picked at random among unsatisfied clauses. The variable is generally 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's considering fewer possibilities.
The algorithm 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.
Local search (optimization)
In computer science, local search is a metaheuristic method for solving computationally hard optimization problems. Local search can be used on problems that can be formulated as finding a solution maximizing a criterion among a number of candidate solutions...
algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
s to solve Boolean satisfiability problems
Boolean satisfiability problem
In computer science, satisfiability is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE...
.
Both algorithms work on formulae that are in, or have been converted into, conjunctive normal form
Conjunctive normal form
In Boolean logic, a formula is in conjunctive normal form if it is a conjunction of clauses, where a clause is a disjunction of literals.As a normal form, it is useful in automated theorem proving...
. They start by assigning a random value to each variable. If the assignment satisfies all clauses
Clause (logic)
In logic, a clause is a finite disjunction ofliterals. Clausesare usually written as follows, where the symbols l_i areliterals:l_1 \vee \cdots \vee l_nIn some cases, clauses are written as sets of literals, so that clause above...
, 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 generally picked at random among unsatisfied clauses. The variable is generally 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's considering fewer possibilities.
The algorithm 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
Satplan
Satplan is a method for automated planning. It converts the planning problem instance into an instance of the Boolean satisfiability problem, which is then solved using a method for establishing satisfiability such as the DPLL algorithm or WalkSAT.Given a problem instance in planning, with a given...
.
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.