# Implementing the GSAT algorithm - How to select which literal to flip?

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.