Cet algorithme, en java, est une première étape vers la recherche d'algorithmes incomplets et efficaces pour la réfutation, dans le cadre de la logique booléenne (SAT).