Transfer Learning from Foundational Optimization Embeddings to Unsupervised SAT Representations

Probleemstelling

Mixed-Integer Programming (MIP) en Boolean Satisfiability (SAT) zijn fundamentele formalismen voor combinatorisch redeneren. Hoewel Graph Neural Networks (GNN's) krachtige structurele representaties voor deze problemen kunnen leren, zijn bestaande modellen vaak beperkt door:

1. Afhankelijkheid van labels: Ze vereisen vaak labels gegenereerd door solvers (bijv. satisfiability-status), wat duur en tijdrovend is.
2. Gebrek aan generalisatie: Modellen moeten vaak opnieuw worden getraind voor elke nieuwe domein of taak en presteren slecht bij distributiewijzigingen.
3. Gebrek aan universele representaties: Er bestaat nog geen "foundation model" dat generieke, onbewaakte (unsupervised) embeddings leert die zowel voor optimalisatie (MIP) als beslissingsproblemen (SAT) bruikbaar zijn.

De kernvraag van dit onderzoek is: Kunnen embeddings die zijn getraind op MIP-structuren (foundational optimization embeddings) worden overgedragen naar SAT-problemen, en kunnen ze nuttige, onbewaakte representaties genereren zonder solver-labels?

Methodologie

De auteurs passen het Forge-architectuur (oorspronkelijk ontwikkeld voor MIP) toe op SAT-instanties via drie varianten van transfer learning.

1. Representatie en Encoding:

• SAT naar MIP: Een CNF-formule (SAT) wordt omgezet in een 0-1 MIP-instantie. Elke Booleaanse variabele wordt een binaire variabele, en elke clause wordt een lineaire ongelijkheid.
• Grafische Representatie: Zowel MIP als de geëncodeerde SAT worden weergegeven als een bipartiete graaf met knopen voor constraints (clauses) en variabelen, verbonden via een rand als een variabele in een constraint voorkomt.
• Forge Architectuur: Het model gebruikt een twee-laags GraphSAGE-encoder, gevolgd door Vector Quantization (VQ) en een decoder. Het doel is het reconstrueren van knoop-features en randen (auto-encoder), wat leidt tot generieke embeddings zonder supervisorie.

2. De Drie Transfer-Varianten:
De auteurs testen drie benaderingen om de overdracht te evalueren:

• Forge-MIP (Zero-change transfer): Het oorspronkelijk op MIP getrainde model wordt direct toegepast op SAT-instanties (geëncodeerd als MIP). Zowel de architectuur als de MIP-specifieke knoop-features blijven ongewijzigd. Dit test puur gewichts-overdracht.
• Forge-MIP-SAT (Feature-adapted transfer): De vooraf getrainde MIP-weights worden behouden, maar de input-features worden vervangen door SAT-specifieke features:
  • Constraint-features: Breedte van de clause, aantal positieve/negatieve literals, ratio.
  • Variabele-features: Graad (aantal clauses), positieve/negatieve graad, genormaliseerde waarden.
    Dit isoleert het effect van feature-specialisatie.
• Forge-SAT (SAT-native model): De Forge-architectuur wordt behouden, maar de MIP-weights worden verworpen. Het model wordt vanaf nul (van scratch) getraind op SAT-data (G4SATBench) met SAT-specifieke features. Dit test of het trainingsparadigma zelf generaliseert.

Belangrijkste Bijdragen

1. Architectuur-overdracht: Aanpassing van de Forge-architectuur voor SAT via een SAT-naar-MIP encoding-pijplijn.
2. Gewichts-overdracht: Het aantonen dat vooraf getrainde MIP-embeddings (Forge-MIP) al nuttige structurele informatie bevatten voor SAT, en dat feature-specialisatie (Forge-MIP-SAT) de prestaties verder verbetert.
3. SAT-native Foundation Model: Introductie van Forge-SAT, een model dat het Forge-trainingsparadigma hergebruikt maar volledig gespecialiseerd is in SAT-data.
4. Empirische Evaluatie: De eerste uitgebreide studie die foundation models overbrengt van optimalisatie naar beslissingsproblemen, specifiek gericht op onbewaakte taken (clustering).
5. Open Source: Publicatie van alle vooraf getrainde modellen en pipelines, waardoor het mogelijk is om direct embeddings te genereren voor willekeurige SAT-instanties, clauses en variabelen.

Resultaten

De experimenten zijn uitgevoerd op de G4SATBench dataset (Hard split), bestaande uit 1400 onzichtbare formules uit zeven verschillende probleemtypen (random, pseudo-industrieel, combinatorisch), verdeeld over SAT en UNSAT.

Evaluatiemetrics:

• Normalized Mutual Information (NMI): Hoe goed de clusters overeenkomen met de 14 ground-truth categorieën (probleemtype + satisfiability).
• Purity: Hoe homogeen de clusters zijn.

Kernbevindingen:

• Static Baseline: Een simpele statische heuristiek (gemiddelde pooling van features) behaalde een NMI van 0.74.
• Forge-MIP: Zelfs zonder feature-aanpassing verbeterde het getransfereerde MIP-model de NMI naar 0.76. Dit bewijst dat MIP-structuren gedeelde regulariteiten hebben met SAT.
• Forge-MIP-SAT: Door MIP-weights te combineren met SAT-features, steeg de NMI naar 0.77 en de Purity naar 0.66.
• Forge-SAT: Het model dat vanaf nul op SAT-data is getraind, behaalde de beste resultaten met een NMI van 0.79 en Purity van 0.66.
• Visualisatie: De embeddings van Forge-SAT vormden 13 van de 14 verwachte compacte clusters, waarbij ze zelfs SAT en UNSAT instanties binnen hetzelfde probleemtype succesvol van elkaar scheidden.

Betekenis en Conclusie

Dit paper toont voor het eerst aan dat foundational optimization embeddings effectief kunnen worden overgedragen naar het domein van Boolean Satisfiability.

• Unificatie: Het bewijst dat er een gedeelde structurele taal bestaat tussen MIP en SAT die door een enkel model kan worden geleerd.
• Onbewaakte Leren: Het succes van onbewaakte pretraining betekent dat men nu betekenisvolle SAT-representaties kan genereren zonder afhankelijk te zijn van dure solver-labels of specifieke taak-tuning.
• Toekomstperspectief: Hoewel de huidige studie zich richt op clustering, opent dit de weg voor het gebruik van deze embeddings in downstream taken zoals satisfiability-predicatie, het leiden van SAT-solvers (heuristieken), en het uitbreiden naar bredere Constraint Satisfaction Problems (CSP).

De auteurs concluderen dat het mogelijk is om hybride foundation modellen te trainen op een mengsel van MIP- en SAT-data, wat een belangrijke stap is naar een universeel representatief framework voor zowel optimalisatie- als beslissingsproblemen.