Sur des instances 3-SAT tirées au hasard, le comportement ne dépend presque pas de la taille : il dépend du rapport entre le nombre de clauses et le nombre de variables.
Les trois régimes
Rapport petit, sous 4. Peu de clauses pour beaucoup de variables : les solutions abondent, et un solveur en trouve une presque sans revenir en arrière.
Rapport grand, au-dessus de 5. Tant de clauses que la contradiction apparaît vite, et la réfutation est courte.
Rapport voisin de 4,26. Les solutions sont rares mais pas absentes, et rien ne se décide localement. Le solveur doit explorer.
Objectif
Calculer le nombre de clauses de deux instances prises au seuil, donner le nombre de littéraux par clause en 3-SAT, et situer une instance de rapport 2.
Pièges
Le seuil est aussi le point où le coût de résolution est maximal, et cela vaut pour les deux réponses. Une instance difficile ne l'est pas parce qu'elle est grande, mais parce qu'elle est prise au mauvais endroit.