Citation authentique :

« Sa mère les diamants ça chauffe. Je passe aux pigeons. » « Lol. J'ai poussé les pigeons. » « Alors ils te vont mes pigeons ? » « Tout va bien pour les pigeons partiels. » « Je suis dégoûtée des pigeons. »

Devinette : Qui a dit cela ? Dans quel contexte ?

Solution :

Le pigeonhole principle (= en français je crois le principe des tiroirs) désigne en SAT une famille de formules insatisfiables dont les preuves par résolution sont de taille exponentielle donc tout solveur DPLL ou CDCL aura un comportement exponentiel sur elles.

Les diamond formulas sont une famille de formules pour lesquelles toute preuve DPLL(T) (squelette propositionnel + lemmes de théorie sur les propositions atomiques de la formule d'origine) est de taille exponentielle, donc tous les solveurs DPLL(T) ont un comportement exponentiel.