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

Question

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.

Answer 1

Isn't the maximum number of satisfied clauses what we're looking for?

Yes, we're looking for an assignment that satisfies the maximum number of clauses (that is all of them, preferably). And to that end we ask ourselves "Which single variable will bring us closest to this goal when flipping it?" and then flip it.

It seems to me that we're trying to use the solution or approximations to it to find the solution.

Using the solution would be if we asked "Which combination of multiple flips would give the best result?" or simply "Which assignment would be the best?". However that's not what we're doing, we're only looking one step ahead. Using an approximation of the solution seems like an accurate description. However there's nothing wrong with that. That's how greedy strategies work.

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.

Right.