  In this paper we describe how to modify GSAT so that it can be applied to
non-clausal formulas. The idea is to use a particular ``score'' function which
gives the number of clauses of the CNF conversion of a formula which are false
under a given truth assignment. Its value is computed in linear time, without
constructing the CNF conversion itself. The proposed methodology applies to
most of the variants of GSAT proposed so far.
