La difficulté de SAT ne tient pas à la vérification, qui est immédiate, mais à la recherche. Cette asymétrie est le cœur de la question.
Les deux tâches
Vérifier : une affectation complète est donnée, il faut dire si elle satisfait la formule. Il suffit de parcourir les clauses une fois.
Trouver : rien n'est donné, il faut produire une affectation satisfaisante ou prouver qu'il n'en existe aucune.
Objectif
Compter les affectations possibles pour deux tailles de formule, donner le facteur d'une variable supplémentaire, et dire de quoi dépend le coût d'une vérification.
Rappels
Chaque variable prend deux valeurs, et les choix sont indépendants : le nombre d'affectations est donc deux élevé à la puissance du nombre de variables.
Pièges
Passer de dix à vingt variables ne double pas le travail, il le multiplie par mille vingt-quatre. C'est cette croissance, et non la taille du texte de la formule, qui rend la recherche exhaustive inutilisable.