Na ciência da computação, GSAT e WalkSat são algoritmos de busca local para resolver Problemas de Satisfatibilidade Booleana. Ambos os algoritmos trabalham com fórmulas da lógica booleana que estão na, ou foram convertidas para a, forma normal conjuntiva. Começa-se pela atribuição de um valor aleatório para cada variável na fórmula. Se a atribuição satisfaz todas as cláusulas, o algoritmo termina, retornando a atribuição. Caso contrário, uma variável é substituída e repete-se o passo anterior até que todas as cláusulas sejam satisfeitas. WalkSAT e GSAT diferem-se nos métodos utilizados para selecionar quais variáveis serão substituidas.