Learning to Rank the Initial Branching Order of SAT Solvers

Dit onderzoek toont aan dat het gebruik van grafische neurale netwerken om de initiële vertakkingsvolgorde van SAT-oplossers te voorspellen aanzienlijke snelheidswinst oplevert voor willekeurige en pseudo-industriële problemen, maar minder effectief is voor complexe industriële instanties doordat de dynamische heuristieken van de solver de initiële voorspelling snel overschrijven.

De kern

Stel je voor dat je een gigantisch labyrint moet doorkruisen om de uitgang te vinden. Dit labyrint is een SAT-probleem (een wiskundig raadsel over waar of niet-waar). Een computer die dit probeert op te lossen, is als een verkennersgroep die elke weg moet uitproberen tot ze de uitgang vinden.

Deze verkenners gebruiken een slimme strategie: ze kiezen bij elke splitsing in het labyrint welke weg ze eerst nemen. In de wereld van computers heet dit branching (vertakken).

Het Probleem: De Slechte Gids

Normaal gesproken kiezen deze computers (de "SAT-solvers") willekeurig of op basis van vaste, oude regels welke weg ze eerst nemen. Het probleem is dat ze soms een heel slechte keuze maken. Ze lopen urenlang de verkeerde kant op, terwijl er een snelle route was die ze hadden kunnen vinden als ze maar even hadden geweten welke weg de beste was.

Het vinden van die perfecte eerste weg is echter erg moeilijk voor de computer zelf. Het is als proberen een kaart te tekenen terwijl je nog in het donker loopt.

De Oplossing: Een AI die de kaart tekent

De auteurs van dit paper hebben een slimme truc bedacht. In plaats van dat de computer zelf moet raden, laten ze een AI (een Graph Neural Network of GNN) eerst naar het labyrint kijken en een startpunt voorspellen.

Stel je voor dat je een ervaren gids hebt die het labyrint van bovenaf heeft gezien. Deze gids zegt: "Vergeet die eerste weg links, die is een doodlopende straat. Begin rechts, bij die grote boom!"

De computer luistert naar deze gids, begint daar, en hoopt dat dit hem veel tijd bespaart.

Wat hebben ze gedaan? (De Experimenten)

1. De Gids testen: Eerst hebben ze bewezen dat het echt uitmaakt waar je begint. Als je de "beste" eerste weg kiest, is het soms duizenden keren sneller dan als je de "slechtste" kiest.
2. De Gids leren: Hoe leer je die AI-gids? Ze hebben drie manieren bedacht om te bepalen wat de "beste" start is:
   • De Conflict-methode: Kijk waar de meeste ruzies (conflicten) zijn in het labyrint en begin daar.
   • De Eerste-stap-methode: Probeer elke weg één keer als eerste en kijk welke het snelst werkt.
   • De Genetische methode: Laat een computer evolueren door willekeurige routes te proberen en de beste te verbeteren (zoals natuurlijke selectie).
3. De Test: Ze hebben de AI getraind op kleine labyrinten en toen gekeken of ze het ook kon op grotere labyrinten.

De Resultaten: Succes en Grenzen

• Bij kleine en middelgrote labyrinten: Het werkt fantastisch! De AI kon de computer helpen om tot 50% sneller te zijn. De AI leerde de structuur van het probleem en gaf een heel goed startadvies.
• Bij enorme, complexe labyrinten: Hier wordt het lastig. Bij de allerzwaarste industriële problemen (zoals die van echte bedrijven) werkt het minder goed.

Waarom werkt het niet altijd?
De auteurs geven twee grappige redenen:

1. De computer is koppig: De AI geeft een startadvies, maar de computer heeft zijn eigen, zeer snelle interne regels. Bij grote problemen vergeten de computer deze regels zo snel dat het advies van de AI al voorbij is voordat het iets doet. Het is alsof je een gids vraagt om de weg te wijzen, maar de verkenners rennen zo hard dat ze de gids al voorbij zijn voordat hij kan spreken.
2. De complexiteit: Bij heel grote problemen is het voor de AI gewoon te moeilijk om het perfecte startpunt te voorspellen. Het labyrint is te ingewikkeld.

Conclusie

Dit onderzoek laat zien dat het een goed idee is om een AI te gebruiken om een startadvies te geven aan een computer die wiskundige raadsels oplost. Het werkt heel goed voor veel soorten problemen en kan zelfs op grotere problemen worden toegepast dan waarvoor de AI is getraind.

Het is echter geen wondermiddel voor alle problemen. Voor de allerzwaarste taken moet de computer nog steeds zijn eigen slimme regels gebruiken, omdat de AI dan niet snel genoeg is om de computer bij te houden. Maar voor veel dagelijkse taken is deze "AI-gids" een enorme winst voor snelheid.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "Learning to Rank the Initial Branching Order of SAT Solvers", geschreven in het Nederlands.

Probleemstelling

Het oplossen van het Boolese satisfiabiliteitsprobleem (SAT) is fundamenteel voor formele verificatie en geautomatiseerd bewijzen. State-of-the-art SAT-oplossers (zoals MiniSat en CaDiCaL) vertrouwen op conflict-gedreven clausule learning (CDCL) en handgemaakte heuristieken om de combinatorische zoekruimte te beheersen. Hoewel deze heuristieken gemiddeld goed werken, falen ze vaak bij specifieke, complexe probleeminstanties.

Een kritieke beslissing in een backtracking SAT-oplosser is de volgorde van het vertakken (branching order): welke variabele moet als eerste worden gekozen om de zoekboom te verkennen? Een goede startvolgorde kan de oplostijd drastisch verkorten, maar het vinden van deze optimale volgorde is zelf een moeilijk probleem. Bestaande hybride oplossers die neurale netwerken gebruiken, vereisen vaak ingrijpende wijzigingen aan de solver of polling tijdens het zoeken, wat computatief duur is.

Methodologie

De auteurs onderzoeken een preprocessing-benadering: het voorspellen van een initiële vertakkingsvolgorde met behulp van een Graph Neural Network (GNN) voordat de CDCL-oplosser start.

1. GNN Architectuur en Representatie:

   • SAT-instanties worden omgezet naar tripartiete grafen met knopen voor variabelen en clausules, en een meta-knooppunt voor snellere berichtoverdracht.
   • De GNN (gebaseerd op NeuroBack) voorspelt een score voor elke variabele. De variabelen worden vervolgens gesorteerd op deze scores om de initiële volgorde te bepalen.
   • Het model wordt getraind met LambdaRank, een loss-functie uit het domein van "learning to rank", die prioriteit geeft aan het correct plaatsen van de meest relevante variabelen (die vroeg in de zoekboom moeten komen) bovenaan de lijst.

2. Labeling Methodes (Trainingsdata generatie):
   Omdat de "optimale" volgorde niet direct bekend is, stellen de auteurs drie methoden voor om labels te genereren:

   • Conflict Labeling: Variabelen worden gerangschikt op basis van het totale aantal conflicten waarin ze tijdens het oplossen betrokken waren. Dit is een "white-box" aanpak die slechts één oplosrun vereist.
   • First Variable Labeling: Het gemiddelde aantal propagaties wordt berekend door elke variabele afzonderlijk als eerste te forceren (de rest willekeurig). Dit isoleert de bijdrage van individuele variabelen.
   • Genetic Labeling: Een optimalisatieprobleem waarbij een genetisch algoritme (hill-climbing) een volgorde zoekt die het aantal propagaties minimaliseert.

3. Integratie in de Solver:
   De voorspelde volgorde wordt niet als een statische lijst ingevoerd, maar door de activiteitsniveaus (activity levels) van de variabelen te initialiseren. Dit beïnvloedt de VSIDS-heuristiek (in MiniSat) en de VMTF-wachtrij (in CaDiCaL), waardoor de solver de voorspelde volgorde volgt zolang de interne heuristieken deze niet overschrijven.

Belangrijkste Bijdragen

• Empirische Validatie: De auteurs tonen aan dat de keuze van de eerste variabele een aanzienlijke impact heeft op de oplostijd (tot wel 2000% versnelling op kleine instanties), wat het belang van een goede initiële volgorde onderstreept.
• Drie Labeling-strategieën: Ze introduceren en vergelijken drie methoden om trainingslabels te genereren, waarbij ze inzicht geven in de leerbaarheid van elk type label.
• Hybride GNN-Oplosser: Ze presenteren een niet-invasieve pipeline die bestaande CDCL-oplossers (MiniSat en CaDiCaL) versnelt door een GNN als preprocessing-stap te gebruiken, zonder de kern van de solver te moeten herschrijven.

Resultaten

De evaluatie is uitgevoerd op drie soorten datasets: willekeurige 3-CNF instanties, G4SATBench (pseudo-industrieel) en industriële instanties (SAT Competitie).

• Willekeurige 3-CNF Instanties:

  • De GNN-initializede oplossers tonen aanzienlijke versnellingen (tot >50% reductie in propagaties) voor instanties met 200 variabelen of minder.
  • Er is een opmerkelijke generalisatie: een model getraind op kleine instanties (20-40 variabelen) werkt effectief op veel grotere instanties (tot 5-10x groter dan de trainingsdata).
  • De drie labeling-methodes presteren qua versnelling vergelijkbaar, hoewel "Conflict Labeling" iets minder goed correleerde met de voorspelde volgorde dan de andere methoden.

• Pseudo-industriële Instanties (G4SATBench):

  • Op "makkelijke" instanties worden versnellingen van 10-20% behaald.
  • Op "moeilijke" instanties (>10^5 propagaties) verdwijnt het voordeel; de prestaties komen overeen met de standaard heuristieken.

• Industriële Instanties (SAT Competitie 2024):

  • Er is geen significant voordeel gevonden ten opzichte van de baselines.
  • De auteurs attribueren dit aan twee factoren:
    1. Overwriting: Bij complexe problemen met lange oplostijden worden de initiële activiteitsniveaus snel overschreven door de dynamische heuristieken van de solver (vooral bij MiniSat zonder VMTF-wachtrij).
    2. Complexiteit: De structuur van deze grote industriële instanties is te complex voor de GNN om een betrouwbare initiële volgorde te voorspellen.

Betekenis en Conclusie

Dit paper toont aan dat het voorspellen van een initiële vertakkingsvolgorde met GNN's een veelbelovende route is om SAT-oplossers te versnellen, vooral voor gegenereerde en semi-industriële problemen. Het benadrukt dat neurale netwerken de onderliggende structuur van SAT-problemen kunnen leren om de zoekefficiëntie te verbeteren.

Echter, de studie identificeert ook de grenzen van deze aanpak: bij zeer complexe, industriële problemen overheersen de dynamische, interne heuristieken van de solver de initiële voorspelling. Dit suggereert dat toekomstig werk zich moet richten op het vinden van een evenwicht tussen neurale initiatie en de dynamische aanpassing van de solver, of op het ontwikkelen van methoden om de voorspelde volgorde effectiever te behouden tijdens het oplossen.