Figure 3: GSAT algorithm of Selman, Levesque, and Mitchell.
algorithm GSAT(S, MAX_TRIES, MAX_FLIPS)
for (i = 0; i < MAX_TRIES; i++)
T := randomly generate an interpretation for the variables that appear in S
for (j = 0; j < MAX_FLIPS; j++)
if (T satisfies S) then return(T);
p := a proposition such that a change to its truth-assignment in T gives the
largest increase in the total number of clauses of S that are satisfied by T
if there are more than 1 such propositions, choose p randomly from them
T := T with truth-assignment for p "flipped"
end for
end for
return "no satisfying assignment found"