Les contraintes du premier ordre (toute quantification, tout symbole logique) jouent un rôle fondamental en informatique et mathématiques. D'un côté théorique la conception d'un solveur de contraintes du premier ordre dans une théorie T est la preuve formelle de la complétude de T.D'un point de vue pratique, les contraintes du premier ordre offrent une grande expressivité qui permet de modéliser d'une manière naturelle plusieurs problèmes complexes de différents domaines de l'intelligence artificielle. Un des derniers résultats publiés autour de la logique du premier ordre est “la décomposabilité” : une propriété partagée par plusieurs théories du premier ordre qui permet de dégager une procédure de décision générale qui pour toute proposition (formule sans variables libres) produit soit vrai soit faux dans toute théorie décomposable. Malheureusement, cette procédure de décision ne permet pas de résoudre des contraintes du premier ordre contenant des variables libres. Ce genre de problème est connu sous le nom de first-order constraint satisfaction problems. Nous présentons donc dans ce papier, le premier solveur complet de contraintes du premier ordre dans toute théorie décomposable T. L'idée principale est de combiner une propagation de sous-formules logiques avec des propriétés subtiles de la décomposabilité. Notre solveur est composé de neuf règles de réécriture qui transforme toute contrainte du premier ordre φ (qui peut évidement contenir des variables libres) en une formule équivalente Φ qui est : soit la formule vrai, soit la formule faux, soit une formule simple ayant au moins une variable libre et n'étant équivalente ni à vrai ni à faux. Nous montrons l'efficacité de notre solveur en résolvant des contraintes du premier ordre sur des arbres finis ou infinis contenant un grand nombre de quantificateurs imbriqués et comparons les performances obtenues avec ceux de notre tout dernier solveur de contraintes du premier ordre dédié aux arbres finis ou infinis. Ceci est le premier solveur de contraintes du premier ordre pour toute théorie décomposable T.