Technische Samenvatting: Doelbewuste Data-Augmentatie voor SAT-voorspelling

1. Probleemstelling

De toepassing van machine learning, met name Graph Neural Networks (GNN's), op NP-moeilijke problemen zoals Boolean Satisfiability (SAT) wordt fundamenteel beperkt door de hoge kosten van het genereren van gelabelde trainingsdata. Standaardpijplijnen vertrouwen op een "solver-in-the-loop"-benadering, waarbij willekeurige formules worden gegenereerd en vervolgens worden opgelost door complete SAT-solvers (bijvoorbeeld CaDiCaL) om hun labels (SAT of UNSAT) te bepalen. Naarmate de probleemgroottes toenemen, vooral in de buurt van de satisfiability-fase-overgang, wordt dit labelproces exponentieel duur, wat de schaal van bruikbare supervisie ernstig beperkt. Deze bottleneck belemmert het vermogen om grootschalige data te benutten om de structurele eigenschappen van moeilijke combinatorische problemen te vangen, een vereiste voor het succes van moderne deep learning-paradigma's.

2. Methodologie

De auteurs stellen een tweeledige aanpak voor: een doelbewuste, solver-vrije datageneratiekader en een optimalisatiebewuste GNN-architectuur.

2.1 Doelbewuste Solver-vrije Datageneratie

Het kerninzicht is een asymmetrie: terwijl het vinden van een bevredigende toewijzing voor een gegeven formule NP-moeilijk is, is het construeren van een formule rond een bekende toewijzing (of contradictie) computationeel efficiënt. De auteurs adopteren een "oplossing-eerst" perspectief, waarbij instanties worden geconstrueerd door constructie in plaats van door steekproeven en verificatie.

• SAT-instantiegeneratie: De methode steekt een willekeurige referentietoewijzing $x^*$ uit. Voor elke clausule steekt het een doel-"slack" $s^*$ uit de empirische verdeling van een doelbenchmark (bijvoorbeeld G4SATBench). De slack vertegenwoordigt het aantal literalen in een clausule dat boven het enige vereiste voor haalbaarheid wordt bevredigd. De generator construeert vervolgens deterministisch clausules met specifieke polariteiten zodat precies $s^* + 1$ literalen door $x^*$ worden bevredigd. Dit zorgt ervoor dat de instantie per constructie satisfiable is en overeenkomt met de slackverdeling van de benchmark.
• UNSAT-instantiegeneratie: De methode embedt een kleine, gegarandeerde UNSAT-kern (een set clausules die alle polariteitscombinaties van een subset van variabelen dekt) binnen een grotere set "vullende" clausules. De vullende clausules worden gegenereerd met dezelfde slack-geplante methode als SAT-instanties, in lijn met de UNSAT-slackverdeling van de benchmark. Het label is per constructie bekend (UNSAT) zonder dat een solver nodig is.
• Doelbewustheid: In tegenstelling tot generieke geplante constructies, matcht dit kader expliciet structurele statistieken (clausulebreedte, voorkomsscheefheid en slackverdelingen) van een doelbenchmark om distributieve mismatch te minimaliseren.

2.2 Lineair-programmeringsbewuste Graph Neural Network (LPGNN)

Om de algebraïsche structuur van de gegenereerde data te benutten, introduceren de auteurs de LPGNN.

• Codering: CNF-formules worden gemapt naar een binair lineair haalbaarheidsprobleem $Ax \geq b$. Slackvariabelen $s$ worden geïntroduceerd om ongelijkheden om te zetten in gelijkheden: $Ax - s = b$.
• Grafstructuur: De grafiek bevat twee knooppunttypes: variabele knooppunten ($x$) en slack-knooppunten ($s$). Randen verbinden variabelen met de slack-knooppunten van clausules waarin ze deelnemen.
• Berichtoverdracht met Residuen: De architectuur integreert een Lineair Programmering (LP) residumechanisme. In elke laag projecteert het netwerk knooppunt-embeddings naar een continue surrogaat $\tilde{z}$. Het berekent een constraint-residu $r = \tilde{A}\tilde{z} - b$ in de constraint-ruimte. Dit residu wordt via de getransponeerde $\tilde{A}^T r$ teruggemapt naar de knooppuntruimte, waardoor een haalbaarheidssignaal (gradiënt van de constraint-overtreding) wordt ingebracht in de knooppuntupdates. Dit stelt de GNN in staat om de onderliggende optimalisatiestructuur direct te benutten.

3. Belangrijkste Bijdragen

1. Solver-vrije Generatiekader: Een CNF-native methode om correct gelabelde SAT- en UNSAT-instanties te genereren door constructie, waardoor de behoefte aan dure solveroproepen tijdens het creëren van data wordt geëlimineerd.
2. Doelbewuste Uitlijning: Een strategie die synthetische data uitlijnt met de structurele en algebraïsche eigenschappen (specifiek slackverdelingen) van doelbenchmarks, waardoor de data effectief wordt voor downstream learning.
3. LPGNN-architectuur: Een nieuw GNN-ontwerp dat LP-gebaseerde constraint-overtredingsresiduen integreert in berichtoverdracht, waardoor algebraïsche haalbaarheidsstructuur aan het model wordt blootgelegd.
4. Data-gedreven Paradigma: Een demonstratie dat voor NP-moeilijke problemen schaalbare, taak-uitgelijnde datageneratie even cruciaal is als modelarchitectuurontwerp.

4. Experimentele Resultaten

• Generatie-efficiëntie: De voorgestelde methode bereikt snelheidswinsten van ordes van grootte in vergelijking met solver-in-the-loop-baselines. Voor grote instanties (bijvoorbeeld $n=1000$) is de solver-vrije methode ongeveer $10^{14}$ keer sneller dan de geëxtrapoleerde CaDiCaL-baseline.
• Distributieve Uitlijning: De gegenereerde instanties reproduceren trouw de slackverdelingen van de doel-G4SATBench-dataset (Figuur 1).
• Schaalingsgedrag: Het trainen van LPGNN op de gegenereerde synthetische data toont consistente verbetering in prestaties naarmate het trainingsvolume toeneemt.
  • SAT-voorspelling: De Constraint Satisfaction Rate (CSR) verbetert van ~88% naar ~99% naarmate het datavolume toeneemt van 250 naar 10k instanties.
  • UNSAT-voorspelling: Het fractie overtreden clausules ($k/m$) neemt af, wat wijst op betere toewijzingskwaliteit voor onbevredigbare instanties.
• Generalisatie: De voordelen van doelbewuste data strekken zich uit tot andere architecturen (NLocalSAT, QuerySAT) en generaliseren naar out-of-distribution testsets (moeilijkere 3-SAT-tiers en SR-families).
• Ablatie: Het verwijderen van het LP-residumechanisme uit LPGNN resulteert in lagere nauwkeurigheid en CSR, wat de waarde van het optimalisatiebewuste signaal bevestigt.
• Vergelijking met Generieke Data: Trainen op generieke, niet-uitgelijnde synthetische data levert bijna willekeurige prestaties op, wat benadrukt dat structurele uitlijning de sleutelfactor is voor succes.

5. Betekenis en Claims

Het artikel stelt dat de primaire bottleneck in op learning gebaseerde SAT-solvers niet de modelcapaciteit is, maar de kosten van het verkrijgen van gelabelde data. Door een schaalbaar, solver-vrij generatiepijplijn te introduceren dat benchmark-uitgelijnde synthetische data produceert, tonen de auteurs aan dat het mogelijk is om GNN's effectief te trainen zonder te vertrouwen op dure solvers voor supervisie.

De auteurs positioneren dit werk als een verschuiving naar een data-gedreven paradigma voor NP-moeilijke problemen. Zij betogen dat net zoals next-token predictie de schaling van taalsmodellen mogelijk maakte, schaalbare en taak-uitgelijnde datageneratie de sleutelenabler is om het potentieel van machine learning in combinatorische optimalisatie te ontsluiten. Het werk claimt niet om SAT-instanties op te lossen die onhandelbaar zijn voor huidige solvers, maar eerder om een mechanisme te bieden voor het genereren van grootschalige, hoogwaardige trainingsdata die nodig is om heuristisch zoeken en toewijzingsvoorspelling in GNN's te verbeteren. De auteurs erkennen beperkingen met betrekking tot de "synthetisch-naar-reëel"-kloof, en merken op dat vervaardigde instanties mogelijk niet perfect de verborgen gemeenschapsstructuren van gespecialiseerde industriële problemen vangen, maar betogen dat de aanpak dient als een krachtige regularisator voor in-distribution learning.