Transfer Learning from Foundational Optimization Embeddings to Unsupervised SAT Representations

Titolo

Transfer Learning da Embedding di Ottimizzazione Fondamentale a Rappresentazioni Unsupervised per SAT

1. Il Problema

Le rappresentazioni strutturali per problemi combinatori come la Programmazione a Numeri Interi Misti (MIP) e la Soddisfacibilità Booleana (SAT) sono tradizionalmente apprese tramite Graph Neural Networks (GNN). Tuttavia, questi modelli presentano limitazioni significative:

• Dipendenza dalle etichette: Richiedono spesso etichette generate dai solver (es. soluzioni ottimali o stati di soddisfacibilità) per l'addestramento supervisionato.
• Scarsa generalizzazione: Tendono a non generalizzare bene tra diversi domini, distribuzioni di dati o scale di istanze.
• Mancanza di modelli fondazionali: Non esiste un modello pre-addestrato generico che possa essere riutilizzato per compiti diversi senza un ri-addestramento completo.

Il paper si pone la domanda fondamentale: le rappresentazioni pre-addestrate su strutture di ottimizzazione (MIP) possono trasferirsi efficacemente a problemi di decisione (SAT) in modo non supervisionato?

2. Metodologia

Gli autori adattano l'architettura Forge, un modello fondazionale pre-addestrato su un vasto corpus eterogeneo di istanze MIP, al dominio SAT. La metodologia si basa su tre pilastri:

A. Rappresentazione Grafica Bipartita

Sia le formule CNF (SAT) che le istanze MIP possono essere rappresentate come grafi bipartiti con nodi di vincolo e nodi di variabile.

• Codifica SAT-to-MIP: Una formula CNF viene codificata come un problema MIP 0-1. Ogni variabile booleana diventa una variabile binaria e ogni clausola diventa un vincolo lineare. Questo permette di utilizzare la stessa struttura di grafo e l'architettura Forge senza modifiche strutturali.

B. Varianti di Transfer Learning

Il paper esplora tre varianti per valutare diversi livelli di trasferimento:

1. Forge-MIP (Trasferimento a zero cambiamenti): Utilizza direttamente il modello Forge pre-addestrato su MIP. Le istanze SAT sono codificate come MIP e vengono utilizzati i feature specifici per MIP (es. limiti, coefficienti della funzione obiettivo) sui nodi del grafo.
2. Forge-MIP-SAT (Trasferimento adattato ai feature): Mantiene i pesi pre-addestrati e l'architettura Forge, ma sostituisce i feature dei nodi MIP con feature specifiche per SAT.
   • Feature Clausole: Larghezza, conteggio letterali positivi/negativi, rapporto pos/neg.
   • Feature Variabili: Grado totale, gradi positivi/negativi, rapporti e normalizzazioni.
3. Forge-SAT (Modello nativo SAT): Mantiene l'architettura Forge ma scarta i pesi pre-addestrati su MIP. Il modello viene pre-addestrato da zero su un corpus di istanze SAT (G4SATBench) utilizzando i feature specifici per SAT.

3. Contributi Chiave

1. Adattamento dell'Architettura: Dimostrazione che l'architettura Forge, nata per MIP, può essere applicata a SAT tramite una pipeline di codifica e l'uso di feature specifiche.
2. Validazione del Transfer di Pesi: Evidenza che i pesi pre-addestrati su problemi di ottimizzazione (MIP) catturano già regolarità strutturali utili per i problemi di decisione (SAT), e che l'adattamento dei feature migliora ulteriormente le prestazioni.
3. Modello Fondazionale Nativo SAT: Introduzione di Forge-SAT, un modello pre-addestrato specificamente su SAT che riutilizza il paradigma di training fondazionale.
4. Valutazione Empirica: Prima valutazione empirica di questi embedding su compiti unsupervised (clustering) su benchmark SAT standard.
5. Rilascio Open Source: Pubblicazione di tutti i modelli pre-addestrati e delle pipeline di training, permettendo la generazione di embedding per istanze SAT arbitrarie "out-of-the-box".

4. Risultati Sperimentali

Gli esperimenti sono stati condotti sul benchmark G4SATBench, utilizzando istanze "Hard" da 7 diversi tipi di problemi (random, pseudo-industriali, combinatoriali) con un equilibrio tra istanze SAT (soddisfacibili) e UNSAT (insoddisfacibili).

• Compito di Valutazione: Clustering non supervisionato delle embedding a livello di istanza per recuperare la distribuzione sottostante dei problemi e distinguere SAT da UNSAT.
• Metriche: Normalized Mutual Information (NMI) e Purity.
• Risultati Quantitativi:
  • Baseline Statica (Static-SAT): Un semplice pooling di feature statistiche ottiene un NMI di 0.74.
  • Forge-MIP: Il trasferimento diretto dai pesi MIP migliora l'NMI a 0.76, dimostrando che le rappresentazioni di ottimizzazione sono trasferibili.
  • Forge-MIP-SAT: L'adattamento dei feature su pesi MIP pre-addestrati raggiunge un NMI di 0.77.
  • Forge-SAT: Il modello pre-addestrato da zero su SAT ottiene le prestazioni migliori con un NMI di 0.79 e una Purity di 0.66.
• Osservazioni Qualitative: La visualizzazione 2D (PaCMAP) mostra che Forge-SAT riesce a formare 13 cluster compatti e ben separati su 14 gruppi target, distinguendo chiaramente non solo i tipi di problema, ma anche la fattibilità (SAT vs UNSAT) all'interno dello stesso tipo.

5. Significato e Implicazioni

• Unificazione dei Domini: Il lavoro dimostra per la prima volta che esiste una sovrapposizione strutturale significativa tra problemi di ottimizzazione (MIP) e problemi di decisione (SAT), permettendo il trasferimento di modelli fondazionali tra questi domini.
• Indipendenza dai Solver: Il metodo è completamente unsupervised. Non richiede etichette generate da solver SAT o MIP, rendendo scalabile la creazione di rappresentazioni per istanze arbitrarie.
• Fondamento per Modelli Unificati: Apre la strada a modelli fondazionali ibridi che possono essere pre-addestrati su miscele di MIP e SAT, potenzialmente unificando la rappresentazione per l'intera classe dei problemi di soddisfacimento dei vincoli (CSP) e della programmazione a vincoli (CP).
• Impatto Pratico: Fornisce strumenti pronti all'uso per generare embedding significativi per istanze SAT, utili per compiti downstream come la previsione della soddisfacibilità, la selezione di solver o l'euristica guidata dai solver, senza necessità di addestramento supervisionato specifico.

In sintesi, il paper stabilisce un nuovo paradigma per l'apprendimento di rappresentazioni nel campo della logica combinatoria, spostando l'attenzione dall'addestramento supervisionato specifico per task a modelli fondazionali pre-addestrati su larga scala capaci di generalizzare attraverso domini diversi.