Riepilogo Tecnico: Calcolo di Implicanti SAT Brevi tramite Codifiche Ising/QUBO

1. Enunciato del Problema

Molti compiti di ragionamento, inclusa la spiegazione, la diagnosi e la compressione dei modelli, richiedono assegnazioni parziali soddisfacenti brevi (implicanti) piuttosto che assegnazioni totali. In questi contesti, le variabili non assegnate agiscono come vere "indifferenti" (don't-cares), e spesso solo un sottoinsieme di variabili (variabili visibili) è semanticamente rilevante, mentre altre fungono da supporto nascosto.

Sebbene i moderni risolutori SAT calcolino efficientemente assegnazioni soddisfacenti totali, la derivazione di implicanti brevi richiede tipicamente chiamate SAT ripetute o post-elaborazione dedicata. Analogamente, le formulazioni standard SAT-to-Ising/QUBO sono intrinsecamente limitate: mappano le formule CNF in funzioni di energia quadratiche dove gli stati fondamentali corrispondono ad assegnazioni totali. Il modello Ising/QUBO assegna un valore a ogni spin, mancando di una rappresentazione nativa per variabili "non assegnate". Di conseguenza, il calcolo di implicanti brevi è storicamente stato lasciato ad algoritmi esterni piuttosto che essere catturato all'interno del modello di ottimizzazione quadratica stessa.

2. Metodologia

Gli autori propongono un framework di ottimizzazione unificato che supporta nativamente assegnazioni parziali a tre valori (Vero, Falso, Non Assegnato) all'interno di un modello quadratico Ising/QUBO.

2.1 Rappresentazione a Doppia Polarità

Per rappresentare le variabili non assegnate, il framework introduce una codifica a doppia polarità. Per ogni variabile proposizionale $A_i$, vengono utilizzati due spin binari $(p_i, n_i)$:

• $(1, 0) \implies A_i = \top$
• $(0, 1) \implies A_i = \bot$
• $(0, 0) \implies A_i$ è non assegnata (indifferente)
• $(1, 1) \implies$ Incoerente (vietato)

Viene aggiunta una penalità di coerenza semantica $M \cdot p_i n_i$ per vietare lo stato incoerente.

2.2 Codifica delle Clausole

Le clausole sono codificate utilizzando funzioni di penalità quadratiche standard. Per una clausola $C_k = (\ell_1 \lor \ell_2 \lor \ell_3)$, i letterali sono mappati sui loro spin di polarità corrispondenti. Per mantenere la forma quadratica, viene introdotta una variabile ausiliaria $c_k$ per catturare la condizione in cui i primi due letterali sono falsi. La funzione di energia penalizza le configurazioni in cui tutti i letterali sono falsi (ovvero, tutti gli spin corrispondenti sono 0).

2.3 Sparsità e Funzione Obiettivo

Viene aggiunto un termine di sparsità alla funzione di energia: $E_{sparse} = \gamma \sum (p_i + n_i)$. Questo termine penalizza gli spin attivi, orientando l'ottimizzatore verso configurazioni con meno variabili assegnate (implicanti più brevi).
La funzione di energia totale è:
$$E_F = \sum M p_i n_i + \sum E_{clause}(k) + \gamma \sum (p_i + n_i)$$

2.4 Regimi di Peso

Il documento stabilisce condizioni teoriche sui pesi ($\lambda$ per le penalità delle clausole, $M$ per la coerenza, $\gamma$ per la sparsità) per garantire la correttezza. Nello specifico, se $\lambda > n\gamma$ e $M > n\gamma$ (dove $n$ è il numero di variabili), gli stati fondamentali della funzione di energia corrispondono esattamente a implicanti di cardinalità minima.

2.5 Riduzione e Proiezione

• Riduzione degli Implicanti: Data un'assegnazione soddisfacente totale, il framework restringe lo spazio di ricerca fissando gli spin di polarità "opposta" a 0. Ciò permette all'ottimizzatore di rimuovere solo letterali dall'assegnazione esistente, trovando la sotto-assegnazione più breve che rimane un implicante valido.
• Proiezione: Per focalizzarsi su un sottoinsieme di variabili visibili $P$, la penalità di sparsità viene applicata solo alle variabili in $P$. Le variabili nascoste $H$ rimangono non vincolate dalla sparsità, agendo come supporto ausiliario libero. Ciò permette al modello di trovare assegnazioni brevi su $P$ soddisfacendo la formula tramite $H$.

3. Contributi Chiave

1. Codifica Nativa a Tre Valori: Una codifica SAT-to-Ising/QUBO che rappresenta nativamente le assegnazioni parziali (Vero/Falso/Non Assegnato) tramite semantica a doppia polarità, eliminando la necessità di post-elaborazione esterna per interpretare gli stati "non assegnati".
2. Varianti Flessibili dell'Obiettivo: Formulazioni QUBO in cui la riduzione degli implicanti è ottenuta tramite restrizioni di polarità e la proiezione è ottenuta limitando le penalità di sparsità alle variabili visibili, tutto all'interno di una singola struttura fissa di modello quadratico.
3. Garanzie Teoriche: Identificazione di specifici regimi di peso ($\lambda > n\gamma, M > n\gamma$) che garantiscono che gli stati fondamentali corrispondano a implicanti di cardinalità minima. Il documento fornisce un criterio per riconoscere gli implicanti validi direttamente dal valore finale dell'energia.
4. Validazione Empirica: Una valutazione utilizzando il ricottura simulata su formule 3-SAT casuali e formule non-CNF, dimostrando la capacità della codifica di produrre assegnazioni parziali brevi e raggiungere la minimalità attraverso affinamento iterativo.

4. Risultati Sperimentali

Gli autori hanno valutato la codifica utilizzando Ricottura Simulata (SA) su due set di benchmark:

• 3-SAT Casuale: Istanze soddisfacenti con bassa densità di clausole per variabile ($m/n = 1.5$).
• Formule Non-CNF: Formule booleane convertite in CNF tramite trasformazioni di Tseitin/Plaisted-Greenbaum, creando un contesto proiettato con variabili ausiliarie nascoste.

Risultati Chiave:

• Compattezza: Sul 3-SAT casuale, la codifica lascia in media circa un terzo delle variabili non assegnate preservando la soddisfacibilità.
• Minimalità: Mentre la SA di base spesso trova assegnazioni di cardinalità minima su istanze piccole-medie, i tassi di successo diminuiscono all'aumentare della dimensione del problema a causa di minimi locali. Tuttavia, l'affinamento iterativo (congelare la migliore soluzione e rieseguire la SA per ridurre ulteriormente) migliora significativamente i risultati.
• Minimalità vs. Cardinalità Minima: L'affinamento iterativo raggiunge la minimalità per inclusione (implicanti primi) con alta probabilità. Raggiungere la cardinalità minima (dimensione globale minima) è più difficile ma frequentemente osservato, specialmente nei benchmark non-CNF dove la struttura permette completamenti nascosti uniformi.
• Contesto Proiettato: Nella modalità proiettata, il metodo recupera con successo assegnazioni di cardinalità minima sulle variabili visibili, anche con un'alta proporzione di variabili ausiliarie nascoste (65–70% del totale delle variabili).

5. Significato e Affermazioni

Il documento afferma che questo framework offre un approccio di ottimizzazione unificato per il calcolo di assegnazioni parziali brevi, sostituendo la necessità di sottoroutine di riduzione esterne in pipeline AllSAT o di spiegazione.

• Significato Teorico: Colma il divario tra la natura di "assegnazione totale" dei modelli Ising e i requisiti di "assegnazione parziale" di molti compiti di ragionamento, introducendo una rappresentazione a doppia polarità con regimi di peso dimostrabili per la minimalità.
• Significato Pratico: La codifica funge da "sostituzione diretta" per i passaggi di riduzione nei flussi di lavoro esistenti. Gli autori sottolineano che l'approccio è robusto sotto backend di ottimizzazione generici (come la Ricottura Simulata) e non richiede hardware specializzato per dimostrare la validità semantica, sebbene notino che ricottori quantistici o macchine Ising specializzate potrebbero potenzialmente produrre risultati migliori.
• Limitazioni: Gli autori riconoscono modestamente che, sebbene la codifica garantisca stati fondamentali di cardinalità minima teoricamente, gli ottimizzatori euristici potrebbero rimanere intrappolati in minimi locali. Inoltre, nel contesto proiettato, la codifica impone una "testimone uniforme" (un'unica assegnazione nascosta per tutti i completamenti visibili), che è un requisito più rigoroso rispetto alla semantica standard degli implicanti proiettati, sebbene gli autori sostengano che ciò valga per molte conversioni pratiche non-CNF.

Il lavoro si posiziona come una validazione semantica delle codifiche quadratiche per il ragionamento parziale, dimostrando che con un'adeguata regolazione dei parametri e affinamento iterativo, i modelli Ising/QUBO possono calcolare efficacemente implicanti minimi e di cardinalità minima.