Une nouvelle borne pour 3-SAT : comprendre la remise en cause de l'ETH
SAT, le problème de satisfaisabilité booléenne, demande si une formule logique possède au moins une solution. Ses variables prennent les valeurs vrai ou faux, et ses clauses imposent des règles sur ces valeurs. Avec n variables binaires, il existe 2^n affectations possibles. Les tester une à une devient vite impraticable.
ETH signifie Exponential Time Hypothesis, l'hypothèse du temps exponentiel. Elle affirme qu'aucun algorithme déterministe ne peut résoudre toutes les instances de 3-SAT en temps sous-exponentiel par rapport à n, le nombre de variables. ETH sert de point de départ à de nombreuses preuves de complexité.
À la fin d'octobre 2026, OpenAI et Anthropic ont chacun publié une prépublication, un texte rendu public avant évaluation par les pairs. Les deux travaux revendiquent un algorithme déterministe sous-exponentiel pour compter les solutions de formules SAT dont la largeur des clauses est fixée. Si les preuves sont correctes et si les énoncés formels décrivent bien le 3-SAT dans un modèle de calcul usuel, le compte exact permet aussi de décider si une formule a une solution. Le résultat contredit alors ETH. Ces travaux restent théoriques et ne donnent pas encore de méthode pratique pour résoudre les formules rencontrées dans un projet.
D'abord, que demande 3-SAT ?
Une clause est un OU de littéraux. Un littéral est une variable ou sa négation. Par exemple, (x₁ ∨ ¬x₂ ∨ x₃) est vraie si x₁ vaut vrai, si x₂ vaut faux, ou si x₃ vaut vrai. Le symbole ∨ signifie OU et ¬ signifie NON.
Une formule est un ET de clauses : chacune doit être vraie pour que toute la formule le soit. Dans 3-SAT, chaque clause contient au plus trois littéraux. Une affectation fixe la valeur de toutes les variables, et le problème consiste à savoir si l'une d'elles satisfait l'ensemble des clauses.
Dans les bornes ci-dessous, n compte les variables et m les clauses. L'énumération directe teste jusqu'à 2^n affectations. Chaque variable supplémentaire double ce nombre. Des algorithmes spécialisés font mieux, parfois jusqu'à une base proche de 1,3, mais leur temps reste exponentiel en n.
Ce que signifie « sous-exponentiel »
Les temps 2^n et 1,3^n sont exponentiels. Réduire la base peut accélérer un programme, mais ne change pas ce classement. Une borne sous-exponentielle a la forme 2^{f(n)}, où f(n) / n tend vers zéro. Par exemple, 2^{n / sqrt(log n)} est sous-exponentiel parce que son exposant grandit moins vite que n. log n désigne le logarithme de n. Sa base ne change pas cette propriété asymptotique.
La notation 2^{o(n)} résume cette propriété. Elle ne promet pas un temps court pour les tailles d'entrée actuelles. Certaines fonctions sous-exponentielles dépassent encore toute puissance de n. Pour chaque constante fixe c > 0, elles finissent par être plus petites que 2^{cn} lorsque n grandit. ETH porte sur le pire cas et ne prédit pas le temps d'un solveur sur une formule particulière.
Cette hypothèse ne répond pas à la question P contre NP. P regroupe les problèmes qu'un algorithme peut résoudre en temps polynomial. Dans NP, une solution proposée se vérifie en temps polynomial. Un problème est NP-complet s'il appartient lui-même à NP et si tous les problèmes de NP peuvent être réduits à lui en temps polynomial. 3-SAT est NP-complet : un algorithme polynomial pour 3-SAT donnerait donc un algorithme polynomial pour tout problème de NP, ce qui établirait P = NP.
La borne annoncée reste super-polynomiale. Même si ETH est réfutée, elle ne donne donc pas d'algorithme polynomial et ne tranche pas P contre NP.
La SETH, ou hypothèse du temps exponentiel fort, affirme qu'on ne peut pas gagner une fraction fixe de l'exposant n pour toutes les tailles de clauses. Plus précisément, pour chaque ε > 0, il existe un k fixé tel qu'aucun algorithme déterministe ne résout k-SAT en 2^{(1-ε)n} multiplié par un facteur polynomial en la taille de l'entrée. k-SAT autorise jusqu'à k littéraux par clause, et k reste indépendant de n. SETH implique ETH. Une réfutation d'ETH réfute donc aussi SETH.
La complexité fine étudie les limites de temps propres à chaque problème. Les chercheurs utilisent souvent une réduction depuis 3-SAT : elle transforme une formule en instance du problème visé tout en préservant sa réponse. Pour transférer une borne sous-exponentielle, il faut aussi contrôler la taille produite. Si les n variables deviennent O(n) éléments, un algorithme en 2^{o(N)} sur cette instance, de taille N, donnerait une borne sous-exponentielle pour 3-SAT. Une réduction polynomiale qui produit une instance beaucoup plus grande ne suffit pas. Le manuscrit souligne ce point pour la distance d'édition, la plus longue sous-séquence commune et des problèmes de graphes. Si ETH est réfutée, il faudra examiner séparément les réductions et les hypothèses utilisées pour chaque borne. Certaines limites peuvent reposer sur une hypothèse plus faible ou une autre réduction.
Ce que les deux annonces affirment
SAT répond par oui ou non. #SAT renvoie le nombre exact d'affectations qui satisfont la formule. Si ce compte est positif, la réponse à SAT est oui. Le compte tient sur au plus n + 1 bits, car il ne peut pas dépasser 2^n, le nombre total d'affectations possibles.
Pour chaque largeur fixée k ≥ 2, c'est-à-dire au plus k littéraux par clause, le preprint d'OpenAI annonce un algorithme déterministe de complexité :
poly_k(n,m) × 2^{O_k(n log log n / sqrt(log n))}
Dans cette expression, poly_k(n,m) désigne un facteur polynomial en n et m. La constante cachée dans O_k peut dépendre de k. Le rapport log log n / sqrt(log n) tend vers zéro, donc l'exposant grandit moins vite que n. Les clauses répétées peuvent être retirées sans changer le compte. Pour un k fixe, il reste au plus O(n^k) clauses distinctes. Le facteur polynomial ne change donc pas la classification sous-exponentielle. Le théorème borne aussi l'espace de calcul par un polynôme en la taille de l'entrée. L'algorithme est déterministe : une même entrée suit toujours les mêmes étapes.
Le manuscrit donne aussi une borne pour les formules clairsemées, où m ≤ Dn. Cela signifie que le nombre de clauses reste proportionnel au nombre de variables, avec une constante D fixée indépendamment de la taille de la formule.
poly_{k,D}(n,m) × 2^{O_{k,D}(n / sqrt(log n))}
Les constantes cachées peuvent dépendre de k et de D. Les deux bornes supposent que k reste fixe quand n augmente. Elles ne s'appliquent donc pas automatiquement aux formules dont la largeur des clauses grandit avec l'entrée.
Anthropic a publié un résultat distinct sur le comptage sous-exponentiel et une formalisation Lean dans son dépôt, tandis qu'OpenAI attribue sa preuve à un modèle de recherche interne et qu'Anthropic crédite Claude. Les preuves restent distinctes.
Comment le comptage évite-t-il la simple énumération ?
Partons d'une formule F. Une affectation x est un choix de vrai ou faux pour chacune de ses n variables. Pour chaque clause j, C_j(x) vaut 1 si x la satisfait et 0 sinon. Le produit des C_j(x) vaut donc 1 quand toutes les clauses sont vraies :
#F = somme sur x dans {0,1}^n du produit des C_j(x)
Additionner ces produits sur les 2^n affectations donne le compte exact, mais oblige encore à examiner chaque choix. Le résultat annoncé vient d'une autre méthode.
Le manuscrit transforme le compte en un polynôme qui dépend d'un paramètre. L'algorithme le calcule en plusieurs points, choisis pour simplifier les interactions entre variables, puis retrouve le compte par interpolation. Cette méthode reconstruit un polynôme à partir de ses valeurs. Pour un polynôme en une variable de degré d, d + 1 valeurs en des points distincts suffisent. Garder d bas limite le nombre de calculs nécessaires.
Un test de parité creux est une équation modulo 2 qui relie un petit nombre de bits. Ici, ces bits indiquent quelles clauses une affectation viole. Un tenseur est un tableau de nombres indexé par plusieurs valeurs. Le réseau de tenseurs représente les fonctions locales des clauses et des tests par de tels tableaux, reliés quand ils partagent une variable. La contraction combine les tableaux en sommant sur leurs indices communs. Son ordre compte : une bonne séquence de contractions exploite la structure sans énumérer toutes les affectations globales.
L'analyse doit borner le degré du polynôme, le nombre d'évaluations et la taille des entiers calculés exactement. Le gain asymptotique dépend de ces bornes et de leur interaction.
Ce que Lean vérifie, et ce qui reste à relier
Lean est un assistant de preuve et un langage formel. Les chercheurs y écrivent un énoncé mathématique précis et une preuve sous une forme que la machine peut vérifier. Les tactiques de Lean aident à construire cette preuve. Son noyau, un petit vérificateur, contrôle qu'elle découle bien des définitions, des théorèmes et des axiomes importés. Un axiome est une règle admise comme point de départ. Cette vérification porte sur l'énoncé écrit en Lean. Elle ne compare pas automatiquement cet énoncé avec le texte d'un article.
Pour ce résultat, il faut examiner la preuve formelle et la traduction du manuscrit en Lean. Un « codage canonique » est une manière fixée et non ambiguë d'écrire une formule en entrée de la machine. Une formule en forme conjonctive normale, ou CNF, est un ET de clauses, chacune étant un OU de littéraux. La note de périmètre d'OpenAI décrit une machine qui compte exactement les affectations satisfaisantes de formules k-CNF, où chaque clause contient au plus k littéraux. Elle précise aussi un écart entre la borne du manuscrit et celle de la formalisation.
Le manuscrit annonce un exposant O_k(n log log n / sqrt(log n)). La formalisation établit O_k(n (log log n)^2 / sqrt(log n)), avec un facteur log log n supplémentaire. Son temps comprend aussi un facteur polynomial en L, la longueur en bits de la formule encodée. Pour k fixé, on peut retirer les clauses répétées et il reste au plus O(n^k) clauses distinctes. L reste alors polynomial en n. Le facteur supplémentaire ne change pas le caractère sous-exponentiel, car (log log n)^2 / sqrt(log n) tend vers zéro. Un modèle de calcul précise comment la machine reçoit une entrée et quelles opérations comptent dans son temps d'exécution. La borne formelle réfute ETH si l'encodage et ce modèle couvrent bien le 3-SAT usuel.
Le dépôt Anthropic fournit une formalisation distincte. Son fichier MainResults.lean expose les énoncés, tandis que les preuves sont vérifiées dans le projet Lean. Le dépôt décrit aussi un contrôle avec Comparator, qui compare les énoncés à un fichier de référence, et nanoda, un vérificateur de preuve écrit indépendamment de Lean. Ces outils contrôlent les énoncés encodés et leurs preuves. La lecture qui relie ces énoncés au manuscrit reste nécessaire.
Le 31 octobre, Carlos Toledo a publié un audit externe des deux développements Lean. Il indique avoir rejoué les preuves avec le noyau de Lean et nanoda, qui les acceptent chacune par rapport à l'énoncé de leur dépôt. Son audit formalise aussi le lien entre ces énoncés et ETH dans les modèles de calcul utilisés par les deux projets. La correspondance avec le modèle de machine usuel et avec les manuscrits reste expliquée en prose. Les organisateurs de l'examen communautaire précisent eux aussi que leur rôle est de faciliter la lecture publique, sans certifier le résultat.
Ce que cela change pour la pratique
Si ETH est réfutée, les bornes qui s'appuient dessus devront être vérifiées une par une. Leur solidité dépend de la réduction utilisée et de l'hypothèse exacte. Certaines peuvent rester valides sous une hypothèse plus faible ou grâce à une autre réduction.
Pour un développeur de solveur SAT, les prépublications ne donnent pas encore une méthode à intégrer. Une borne asymptotique décrit le comportement quand les entrées deviennent très grandes. Les facteurs polynomiaux et les constantes cachées peuvent dominer le calcul sur des formules réalistes.
Les solveurs SAT courants utilisent CDCL, l'apprentissage de clauses guidé par les conflits. Quand le solveur rencontre une contradiction, il apprend une clause qui bloque la combinaison de décisions à l'origine du conflit. Cette stratégie exploite la structure de chaque formule. Les prépublications ne comparent pas encore leur algorithme à ces solveurs sur des jeux de formules réelles. Une telle comparaison devrait aussi mesurer le coût de l'arithmétique exacte.
Pour aller plus loin
Le texte fondateur d'Impagliazzo et Paturi, publié en 2001, présente l'ETH dans le contexte de la complexité des problèmes satisfaisabilité. Les deux annonces sont disponibles dans le preprint OpenAI et le dépôt Anthropic. Pour suivre les vérifications, consulte la note de périmètre OpenAI, l'audit de Carlos Toledo et la lettre des organisateurs.
Article co-écrit avec l'IA · Images générées avec l'IA.