Les solveurs SAT sont utilisés avec succès dans de nombreuses applications combinatoires et du monde réel. Il n'est maintenant pas rare de lire qu'une preuve mathé-matique implique des centaines de gigaoctets de traces de solveur SAT. L'ampleur de la preuve commence à consti-tuer une véritable limite à l'approche globale. Dans ce travail, nous proposons de rechercher des contraintes de haut niveau dans les preuves UNSAT. Un travail similaire a été proposé il y a quelques annéespour les contraintes de cardinalité les plus simples. Nous étendons cette idée à un cas plus général (sans limitation sur les bornes des contraintes de cardinalité) en généralisant l'algorithme de Bron & Kerbosh (pour l'énumération de cliques dans les graphes) aux hypergraphes. Nous démontrons expéri-mentalement la capacité de notre approche à trouver des contraintes de cardinalité dans les grandes preuves, ou-vrant ainsi un nouveau moyen de générer des preuves plus courtes et compréhensibles pour les problèmes di ciles. Abstract SAT solvers are successfully used in many real-world and combinatoric applications. It is now not uncommon to read that a mathematical proof implied hundreds of gigabytes of SAT solver traces. The size of the proof by itself begins to be a real limit to the whole approach. In this work, we propose to search for higher-level constraints in UNSAT proofs. A similar work was proposed a few years ago, but only on the original formulafor the most simple cardinality constraints. We extend this idea to a more general case (with no limitations on the bounds of the cardinality constraints) by generalizing the Bron & Kerbosh algorithm (for clique enumeration in graphs) to hypergraphs. We experimentaly demonstrate the ability of our approach to find for cardinality constraints in large proofs, opening a new way of generating more shorter and human-understandable UNSAT proofs of hard problems.