The GSAT algorithm is, for the most part, straight forward: You get a formula in conjunctive normal form and flip the literals of the clauses until you find a solution that satisfies the formula or you reach the max_tries/max_flips limit and find no solution.
I'm implementing the following algorithm:
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
I'm having trouble interpreting the following line:
V <- the variable whose flip yield the most important raise in the number of satisfied clauses;
Isn't the maximum number of satisfied clauses what we're looking for? It seems to me that we're trying to use the solution or approximations to it to find the solution.
I've thought of some ways to do this but It'd be good to hear other points of view (The assumption is that once the variable is flipped once it is selected.):
- Generate a state space with all possible flips and search the space for a literal that results in the best approximation to the goal state.
- Randomly select the variable that I will flip starting with the literals that are more common.
- Pick a random literal.