Le problème SAT est central en théorie de la complexité non seulement du point de vue théorique mais également pour ses applications dans de nombreux domaines, le plus souvent obtenues par codage. Ce problème est de décider si une formule du calcul propositionnel (une conjonction de clauses) admet oui ou non un modèle. Par ailleurs, dans ses applications, obtenir le cas échéant un modèle est très souvent bienvenu. Bien que ce problème soit bien connu pour être NP-Complet, on peut toutefois attendre d'un algorithme de décision que sa complexité soit indépendante de l'ordre des variables et des clauses mais aussi des conditions inutiles dans une formule non satisfiable.
Dans cet exposé, nous proposons une approche de ces objectifs par une méthode basée sur des "compteurs à sauts" et qui fournit au moins un modèle lorsque la formule est satisfiable. Il est notable que les opérations centrales de cette méthode sont combinatoirement assez simples. Récemment, Véronique Cortier est parvenue à améliorer la complexité du calcul de l'une d'elles, passant du quadratique au linéaire. Par contre, la complexité de la méthode dans sa globalité reste encore un mystère....