OpenAI propone una confutazione dell’ipotesi sui tempi minimi del 3-SAT

OpenAI sostiene che un suo modello interno abbia confutato l’Exponential Time Hypothesis, o ETH: una delle ipotesi usate per tracciare i limiti degli algoritmi. Riguarda il 3-SAT, un problema di logica in cui bisogna scegliere valori vero/falso che rispettino tutte le condizioni date, ciascuna composta da tre termini. ETH dice, in sostanza, che nel caso peggiore non si possa evitare un tempo che cresce esponenzialmente con il numero di variabili.

Il manoscritto reso pubblico il 26 ottobre propone invece un algoritmo deterministico che conta esattamente le soluzioni, anche per formule con un numero fisso di termini per condizione diverso da tre. Se si sa quante soluzioni ci sono, si sa anche se ne esiste almeno una. Il tempo dichiarato è subesponenziale: supera quindi il limite ipotizzato da ETH, senza diventare per questo polinomiale o già conveniente nell’uso pratico.

Centinaia di lavori hanno ricavato da ETH limiti condizionali alla velocità di algoritmi per grafi, banche dati, geometria e biologia computazionale. Confutarla significherebbe togliere la premessa a quei limiti, non rendere falsi i ragionamenti che dicevano «se ETH è vera». Il manoscritto presenta anche conseguenze più concrete, fra cui algoritmi subesponenziali per contare certe colorazioni dei grafi.

OpenAI ha pubblicato il testo e una formalizzazione Lean, il sistema che controlla le dimostrazioni. La pagina che ne descrive l’ambito precisa che Lean verifica un limite temporale leggermente meno stretto di quello del manoscritto, ma comunque subesponenziale: sufficiente per la confutazione dichiarata.

L’esame indipendente e la spiegazione del risultato saranno guidati da Russell Impagliazzo, Ramamohan Paturi e Ryan Williams. I primi due sono fra gli autori dell’ipotesi originale. Il gruppo ha chiesto che il materiale fosse pubblico per un esame aperto; partecipare non equivale ad avere già certificato la conclusione. Il risultato, se confermato, resterebbe distinto da una soluzione a P contro NP.