The Walksat local search algorithm has been extended to handle quantification over variables. This greatly reduces model sizes, but in order to guide greedy moves the algorithm still maintains a set of violated clauses. For very large problems, or at the start of a search, this can cause memory problems. We design a new local search algorithm that does not maintain this set and is therefore applicable to larger SAT problems. We show that this algorithm is nevertheless greedy in a probabilistic sense, and that it has good performance on some SAT problems. We also describe a prototype lifted version of the algorithm, and show that advanced constraint programming techniques pay off when searching for violated clauses.