Planted-solution SAT and Ising benchmarks from integer factorization

Il paper presenta una famiglia di istanze di benchmark con soluzione piantata per risolutori SAT e ottimizzazione Ising, derivate dalla fattorizzazione di interi, che permettono di verificare l'output dei solutori grazie a una verità nota e mostrano un tempo di esecuzione mediano che cresce esponenzialmente con la lunghezza in bit dei fattori.

L'essenziale

🧩 L'Enigma dei Numeri: Un Nuovo Gioco per i Computer

Immagina di avere due numeri primi (numeri speciali che non si possono dividere, come 11 e 13) e di moltiplicarli tra loro per ottenere un risultato, diciamo 143.
Fino a qui, è facile: 11 × 13 = 143.

Ora, immagina il problema al contrario: ti do il numero 143 e ti chiedo: "Quali due numeri primi ho moltiplicato per ottenere questo?"
Per un umano è facile. Per un computer, se i numeri sono enormi (come quelli usati per proteggere le password su internet), diventa un incubo. È come cercare di ricostruire due pezzi di un puzzle gigante sapendo solo l'immagine finale, ma senza avere la scatola con la foto di riferimento.

Gli scienziati Itay Hen e il suo team hanno creato un nuovo tipo di "puzzle" per testare quanto sono bravi i computer a risolvere questi indovinelli.

🏗️ Come hanno costruito il puzzle?

Invece di creare numeri a caso, hanno usato la matematica della moltiplicazione stessa per costruire il puzzle. Ecco come funziona, passo dopo passo:

1. La Fabbrica di Bit: Immagina che i numeri non siano scritti con le cifre (1, 2, 3...), ma con interruttori accesi e spenti (0 e 1), come in un computer.
2. La Catena di Montaggio: Quando moltiplichi due numeri, il computer fa una serie di calcoli simili a una catena di montaggio. Ogni passaggio produce un risultato parziale e, cosa molto importante, genera dei "rimanenti" (chiamati riporti) che passano al passaggio successivo, proprio come quando fai una somma a mano e porti l'1 in alto.
3. Il Puzzle Logico: Hanno trasformato questa catena di montaggio in un'enorme lista di regole logiche (un "codice" che il computer deve seguire).
   • Se l'interruttore A è acceso E l'interruttore B è acceso, allora C deve essere acceso.
   • Se C è acceso, allora D deve essere spento.
   • E così via...

Il risultato è un documento lunghissimo (chiamato CNF) che contiene migliaia di queste regole.

🔍 La "Trucco" del Maestro (La Soluzione Piantata)

Qui arriva la parte geniale. Di solito, quando si crea un puzzle per testare un computer, non si sa se esiste una soluzione o quanto è difficile.
In questo caso, gli scienziati hanno detto: "Noi sappiamo già la risposta!".
Hanno creato il puzzle partendo da due numeri che conoscevano già (i "numeri primi nascosti"). Quindi, quando danno il puzzle a un computer, sanno esattamente qual è la soluzione corretta. È come avere la chiave di una serratura mentre si testa quanto è difficile aprirla.

🚀 Cosa hanno scoperto?

Hanno fatto fare questo puzzle a due dei computer più veloci al mondo (i "solutori SAT") e hanno osservato cosa succede man mano che i numeri diventano più grandi.

• L'Effetto Valanga: Hanno scoperto che ogni volta che aumentano di poco la lunghezza dei numeri (aggiungendo un solo "bit", cioè un interruttore in più), il lavoro del computer raddoppia. È come se ogni nuovo interruttore attivasse una valanga di calcoli che si propaga attraverso tutto il sistema.
• La Crescita Esplosiva: Se raddoppi la difficoltà del puzzle, il tempo che il computer impiega non raddoppia, ma cresce in modo esponenziale. È come se il puzzle diventasse un labirinto dove ogni passo in più ti costringe a esplorare un numero di strade che si moltiplica all'infinito.
• Il Colpo di Stato: Anche se i computer moderni sono bravissimi, per numeri un po' più grandi di quelli testati (circa 35-40 bit), il tempo necessario per risolvere il puzzle diventerebbe così lungo da essere praticamente impossibile per i computer attuali.

🎯 Perché è importante?

Questo lavoro è come un banco di prova perfetto per i futuri computer quantistici e per i supercomputer classici.

• È controllato: Puoi rendere il puzzle più difficile o più facile semplicemente cambiando un numero (la lunghezza dei bit).
• È verificabile: Sai sempre se il computer ha indovinato o meno, perché hai la soluzione.
• È strutturato: A differenza dei puzzle casuali, questo ha una struttura logica precisa (come un edificio), che aiuta a capire dove i computer si bloccano e perché.

In sintesi

Gli scienziati hanno costruito una macchina per creare enigmi matematici basati sulla moltiplicazione. Hanno scoperto che questi enigmi diventano incredibilmente difficili molto velocemente, proprio come ci si aspetta che sia la crittografia moderna. Ora, chiunque può usare questo "generatore di enigmi" per vedere se il proprio computer è abbastanza potente da risolvere il mistero dei numeri, o se ha bisogno di una tecnologia completamente nuova (come i computer quantistici) per riuscirci.

È come avere un tapis roulant che puoi regolare a velocità diverse per testare la resistenza di un atleta: prima che l'atleta si stanchi, sai esattamente quanto è forte.

Sommario tecnico

Titolo: Benchmark SAT e Ising a soluzione piantata derivati dalla fattorizzazione intera

1. Il Problema

La valutazione delle prestazioni dei risolutori per la soddisfacibilità booleana (SAT) e per l'ottimizzazione Ising richiede famiglie di istanze che soddisfino contemporaneamente tre criteri difficili da conciliare:

1. Struttura realistica: Devono riflettere la complessità di problemi computazionali reali, non solo disordine casuale.
2. Scalabilità sistematica: La difficoltà deve poter essere controllata e aumentata in modo prevedibile.
3. Verificabilità della verità fondamentale (Ground Truth): Deve esistere una soluzione nota per validare l'output del solver.

Le istanze casuali (come k-SAT uniforme) mancano di una soluzione piantata nota, mentre le istanze "costruite" (crafted) spesso non offrono una scalabilità controllata tramite un singolo parametro. Inoltre, la maggior parte delle costruzioni esistenti si basa su disordine casuale o piantagione algebrica, non catturando la struttura deterministica a lungo raggio tipica di molti problemi computazionali reali.

2. Metodologia

L'autore propone una nuova famiglia di istanze di benchmark derivata dalla fattorizzazione intera. L'idea centrale è codificare i vincoli aritmetici del prodotto $N = p \times q$ (dove $p$ e $q$ sono primi noti) in una formula logica.

Il processo di costruzione segue una pipeline a tre stadi:

1. Generazione delle clausole dalla moltiplicazione binaria:

   • Si considerano due numeri primi $p$ e $q$ di lunghezza in bit $d$.
   • Il prodotto $N$ viene calcolato e i suoi bit sono trattati come costanti note.
   • I bit sconosciuti di $p$ e $q$ sono variabili booleane.
   • L'algoritmo di moltiplicazione binaria (shift-and-add) viene tradotto in un circuito logico. Ogni prodotto parziale ($p_i \land q_j$) e ogni operazione di somma con riporto viene decomposta in operazioni logiche (AND e XOR).
   • Questo genera un sistema di vincoli dove le assegnazioni soddisfacenti corrispondono alle fattorizzazioni valide di $N$. La coppia $(p, q)$ funge da soluzione "piantata" (ground truth).

2. Pre-elaborazione booleana:

   • Prima della conversione in CNF (Conjunctive Normal Form), il sistema subisce una semplificazione logica iterativa.
   • Vengono applicate operazioni come la propagazione dei vincoli (pinning), la semplificazione di AND/XOR (folding costante, identificazione di variabili) e l'inferenza incrociata tra clausole.
   • Le variabili equivalenti vengono fuse, riducendo drasticamente il numero di variabili e clausole, specialmente per istanze piccole.

3. Conversione e Output:

   • I vincoli residui vengono convertiti in formato DIMACS CNF per i solver SAT.
   • Per l'ottimizzazione Ising, i vincoli residui vengono mappati in un Hamiltoniano quadratico utilizzando "gadget" energetici (penalità) che valutano a zero per le assegnazioni soddisfacenti e a un valore positivo per quelle violanti.

3. Contributi Chiave

• Struttura deterministica a lungo raggio: A differenza dei benchmark casuali, queste istanze possiedono correlazioni a lungo raggio indotte dalla propagazione dei riporti (carry) nel circuito di moltiplicazione. Un singolo bit di basso ordine può influenzare i riporti fino alla colonna più alta, creando una struttura di interazione complessa.
• Scalabilità quartica ($d^4$): L'analisi teorica dimostra che il numero totale di contrazioni (e quindi di clausole e variabili) scala come $\Theta(d^4)$, dove $d$ è la lunghezza in bit dei fattori. Questo deriva dal fatto che il numero di voci in una colonna del circuito di moltiplicazione cresce quadraticamente ($d^2$) e la somma su tutte le colonne porta alla crescita quartica.
• Verificabilità assoluta: La soluzione $(p, q)$ è nota a priori, permettendo una verifica univoca e senza ambiguità dell'output del solver.
• Dualità CNF/Ising: La stessa istanza può essere risolta sia come problema SAT (tramite file DIMACS) che come problema di ottimizzazione Ising (classico o quantistico), offrendo un terreno di prova unificato.
• Software open-source: Viene fornito un software per generare queste istanze in modo controllato da un singolo parametro ($d$).

4. Risultati Sperimentali

L'autore ha condotto benchmark sistematici utilizzando due solver SAT moderni basati su CDCL (Conflict-Driven Clause Learning): Kissat 3.0 e CaDiCaL 1.5.

• Scalabilità esponenziale: Per lunghezze dei fattori $d$ comprese tra 8 e 27 bit, il tempo di esecuzione mediano dei solver cresce esponenzialmente con $d$.
• Raddoppio per bit: L'analisi dei dati mostra che il tempo di esecuzione raddoppia approssimativamente per ogni bit aggiuntivo ($T \sim 2^d$). I coefficienti di pendenza ottenuti dall'adattamento log-lineare sono molto vicini a 1 (circa 0.98 per Kissat e 1.02 per CaDiCaL).
• Difficoltà crescente: Anche se le istanze testate ($N \lesssim 10^{16}$) sono ancora gestibili, la crescita rapida suggerisce che istanze con $d \geq 35-40$ costituiranno una sfida significativa per i solver attuali.
• Robustezza: La stretta correlazione tra le prestazioni dei due solver indica che la difficoltà è intrinseca alla struttura del problema (le correlazioni dei riporti) e non dipende da euristiche specifiche del solver.

5. Significato e Implicazioni

Questo lavoro introduce una classe di benchmark qualitativamente diversa rispetto agli ensemble esistenti:

• Complementarità: Riempie il vuoto tra le istanze casuali (senza soluzione nota) e quelle costruite (senza scalabilità controllata), offrendo problemi strutturati, deterministici e verificabili.
• Testbed per solver strutturati: È ideale per studiare il comportamento dei solver su problemi con dipendenze a lungo raggio, un aspetto spesso assente nei benchmark standard.
• Validazione per l'ottimizzazione quantistica: La capacità di compilare le istanze in forma Ising le rende adatte per testare computer quantistici adiabatici (come D-Wave) e algoritmi di ottimizzazione classica su problemi con una struttura di interazione non banale (grafi di interazione eterogenei con connessioni a lungo raggio).
• Impatto sulla complessità: Sebbene la fattorizzazione sia ritenuta computazionalmente difficile, non è scontato che una specifica codifica SAT lo sia. Tuttavia, i risultati empirici confermano che questa costruzione genera istanze di difficoltà crescente e controllabile, rendendole uno strumento prezioso per la ricerca futura sulla complessità computazionale e sull'ottimizzazione.

In sintesi, il paper fornisce un framework rigoroso e scalabile per generare problemi di ottimizzazione e soddisfacibilità con una "verità fondamentale" nota, sfruttando la struttura matematica della moltiplicazione binaria per creare sfide computazionali realistiche e strutturate.