Dans cet article, nous présentons une nouvelle technique de prétraitement d'une formule booléenne mise sous forme normale conjonctive (CNF). A la différence de la plupart des approches actuelles, notre procédure vise à améliorer la capacité de propagation des clauses de la formule tout en produisant un nombre limité de clauses utiles. Plus précisément, un test incomplet de redondance est effectué sur chaque clause d'une formule. Celui-ci est basé sur la propagation unitaire, et peut conduire soit à la production d'une sous-clause ou à la génération d'une nouvelle clause, via les techniques d'apprentissage implémenté dans les solveurs modernes. Cette nouvelle approche est comparée empiriquement au meilleur préprocesseur actuel, en terme de réduction de la formule considérée et d'amélioration pratique de sa résolution par l'un des meilleurs solveurs SAT.