Technische Samenvatting: Het leren van splitting heuristieken voor parallelle string-solvers

Probleemstelling

String-constraint solvers zijn essentieel voor het verifiëren van string-manipulerende programma's in domeinen zoals de handhaving van beveiligingsbeleid en symbolische executie. Veel praktische string-constraints zijn echter onbeslisbaar, en bestaande solvers worstelen vaak met schaalbaarheid en complexe real-world instanties. Hoewel multi-core architecturen een kans bieden voor parallel oplossen, hangt de effectiviteit van divide-and-conquer strategieën (specifiek cube-and-conquer) sterk af van de kwaliteit van de splitting heuristieken. Deze heuristieken bepalen op welk atoom (constraint) er geb branched wordt om de zoekruimte te partitioneren in subproblemen.

Huidige splitting heuristieken zijn doorgaans handmatig ontworpen en statisch. Ze slagen er vaak niet in om zich aan te passen aan de specifieke structurele kenmerken van individuele constraint-instanties. Bovendien lijden bestaande geautomatiseerde benaderingen in het SAT-domein, zoals pairwise classificatie, onder aanzienlijke beperkingen wanneer ze worden toegepast op SMT string solving:

1. Verlies van kwantitatieve informatie: Het reduceren van oplostijden tot binaire labels leidt tot het verlies van fijnmazige kosteninformatie.
2. Cascaderende fouten: Seriele vergelijkingen in pairwise classificatie leiden tot foutaccumulatie, wat de voorspellingskwaliteit verslechtert.
3. Schaalbaarheid: Pairwise methoden vereisen lineaire (of zelfs slechtere) scans over kandidaat-paren, wat computationeel duur is.
4. Domeintoepasbaarheid: Eerdere geautomatiseerde methoden zijn voornamelijk gevalideerd in SAT, met een onbewezen toepasbaarheid op SMT-theorieën zoals strings.

Methodologie

De auteurs introduceren Owl, een datagedreven framework dat automatisch splitting heuristieken genereert voor parallelle string solvers. De kerninnovatie is het herformuleren van het atoomselectieprobleem van een classificatietaak naar een regressietaken.

1. Probleemformulering als regressie

In plaats van twee atomen te vergelijken om te bepalen welke "beter" is (classificatie), voorspelt Owl de continue oplostijd ($Time(\varphi, p)$) die nodig is om de subproblemen op te lossen die ontstaan door te splitsen op een specifiek atoom $p$.

• Kostendefinitie: De doelvariabele is gedefinieerd op basis van de parallelle executie-uitkomst van de twee takken ($\varphi \land p$ en $\varphi \land \neg p$). Bijvoorbeeld, als beide takken bevredigbaar (satisfiable) zijn, is de kosten het minimum van hun oplostijden; als beide onbevredigbaar (unsatisfiable) zijn, is de kosten het maximum.
• Voordeel: Deze benadering behoudt de continuïteit van prestatie-indicatoren, vermijdt discretisatiefouten van classificatie en elimineert de noodzaak voor uitputtende pairwise vergelijkingen, waardoor de inferentie-overhead wordt verminderd.

2. Feature Engineering

Om de regressiemodel te ondersteunen, hebben de auteurs een uitgebreide feature-set van 77 features ontworpen voor elk kandidaat-atoom, verdeeld in twee categorieën:

• Statische Features (66 features): Afgeleid van de formule-structuur zonder solver-executie. Deze omvatten operator-distributies (bijv. tellingen van str.increment, re.union), clausiegrootte en grafische eigenschappen (bijv. variabele-clausule graden).
• Dynamische Features (11 features): Gevangen via korte-termijn lookahead en lookback heuristieken tijdens de solver-executie.
  • Lookback: Houdt historische solver-staten bij, zoals het aantal keren dat een atoom voorkwam in conflict-clausules of geleerde lemma's.
  • Lookahead: Simuleert beperkte constraint-propagatie (meestal begrensd aan ~600 conflicten) om directe consequenties te observeren, zoals het aantal nieuwe toewijzingen of geleerde clausules.

3. Modelselectie en Training

• Algoritme: Het systeem gebruikt Random Forest Regression als het kernpredictieve model. Deze keuze balanceert voorspellende nauwkeurigheid met inferentiesnelheid en robuustheid tegen ruis in labels (variaties in oplostijden).
• Trainingsdata: Een dataset wordt geconstrueerd door de solver te draaien op diverse benchmark-formules, te splitsen op diverse atomen, en de resulterende oplostijden en feature-vectoren vast te leggen.
• Implementatie: Het getrainde model wordt geïntegreerd in de solver (Z3seq en Z3str4). Op elk beslissingspunt construeert de solver een feature-matrix voor kandidaat-atomen, stuurt deze naar een parallel worker-proces via IPC, en ontvangt het voorspelde atoom met de laagste geschatte oplostijd.

Belangrijkste Bijdragen

1. Nieuwe Formulering: Het artikel stelt voor om het ontwerp van splitting heuristieken voor parallel string solving te herformuleren als een regressieprobleem in plaats van een pairwise classificatieprobleem.
2. Praktisch Leerkader: Het introduceert een framework dat automatisch heuristieken genereert met behulp van een rijke set van 77 specifieke instantie-features (statisch en dynamisch).
3. Implementatie en Evaluatie: De aanpak is geïmplementeerd en geëvalueerd op twee state-of-the-art string solvers, Z3seq en Z3str4, waarbij significante prestatiewinsten worden aangetoond ten opzichte van handmatig ontworpen heuristieken.

Experimentele Resultaten

De auteurs evalueerden Owl op 1.024 QF_SLIA formules uit de SMT-LIB repository met behulp van 4, 8, 16 en 32 threads.

• Oplossend Vermogen: Met 4 threads lost Z3seq(Owl) 46 meer formules op (een stijging van 4,8%) dan de baseline, en Z3str4(Owl) lost 9 meer formules op. Deze verbeteringen bleven standhouden over alle thread-configuraties.
• Runtime Prestaties:
  • Z3seq(Owl) bereikte een gemiddelde versnelling van 1,44× bij 32 threads.
  • Z3str4(Owl) bereikte een gemiddelde versnelling van 1,59× bij 32 threads.
• Voorspellingsnauwkeurigheid: De regressiemodellen presteerden significant beter dan de standaard lookahead heuristieken en een pairwise classificatie baseline. Voor Z3seq identificeerde het model de top 20% van de atomen in bijna 45% van de gevallen, vergeleken met willekeurige prestaties voor de baseline.
• Overhead: De computationele overhead van feature extractie en model-inferentie was minimaal en maakte slechts 23,6% van de totale oplostijd uit, wat vergelijkbaar is met of lager is dan de overhead van de standaard lookahead heuristiek.
• Feature Belangrijkheid: Analyse toonde aan dat hoewel specifieke feature-rangschikkingen variëren tussen solvers (wat wijst op de noodzaak voor solver-specifieke optimalisatie), cruciale features zoals "aantal toewijzingen", "lookahead score" en specifieke string-operatie tellingen consistent belangrijk blijven.

Betekenis en Claims

Het artikel claimt dat Owl een significante vooruitgang biedt in parallel string constraint solving door het automatiseren van het ontwerp van splitting heuristieken. Door over te stappen van handmatige, statische heuristieken naar datagedreven regressiemodellen, past de aanpak zich effectief aan de specifieke kenmerken van complexe string-constraints aan.

De auteurs benadrukken dat hun methode:

• Presteert boven bestaande handmatig vervaardigde heuristieken in zowel het aantal opgeloste instanties als de gemiddelde oplostijd.
• De problemen mitigeert van foutaccumulatie en informatieverlies die inherent zijn aan pairwise classificatie-benaderingen.
• Aantoont dat geleerde heuristieken efficiënt kunnen worden geïntegreerd in bestaande CDCL($T$)-gebaseerde solvers (Z3seq en Z3str4) om het potentieel van parallelle architecturen te ontsluiten.

Het werk concludeert dat hoewel de efficiëntie van de sequentiële solver de algemene versnelling begrenst, de geleerde heuristieken de parallellisatie effectief maximaliseren door goed gebalanceerde subproblemen te creëren, wat leidt tot substantiële praktische verbeteringen in het oplossend vermogen.