🤖 AI

Learning Splitting Heuristics for Parallel String Solvers

Dieses Paper schlägt einen datengesteuerten Ansatz vor, um automatisch Splitting-Heuristiken für parallele String-Solver zu erlernen, wobei nachgewiesen wird, dass diese gelernten Heuristiken sowohl in der Anzahl der gelösten Formeln als auch in der durchschnittlichen Lösungszeit bei der Implementierung in Z3seq und Z3str4 manuell entworfene Heuristiken signifikant übertreffen.

Ursprüngliche Autoren: Chenhao Gao, Peisen Yao

Veröffentlicht 2026-06-23

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Chenhao Gao, Peisen Yao

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie versuchen, ein riesiges, unglaublich kompliziertes Jigsaw-Puzzle zu lösen. Dieses Puzzle repräsentiert die Logik eines Computerprogramms, das speziell mit Text arbeitet (wie Passwörter, Benutzernamen oder Dateipfade). Ihr Ziel ist es herauszufinden, ob es eine Möglichkeit gibt, die Teile so anzuordnen, dass alles perfekt zusammenpasst (eine „erfüllbare“ Lösung) oder ob das Puzzle kaputt und unmöglich zu vervollständigen ist (eine „unerfüllbare“ Lösung).

Dies ist die Aufgabe eines String-Solvers. Doch diese Puzzles sind oft so groß und komplex, dass ein einzelner Mensch (oder ein einzelner Computer-Kern), der versucht, sie Stück für Stück zu lösen, ewig brauchen würde.

Das Problem: Zu viele Entscheidungen, zu langsam

Um diese Puzzles schneller zu lösen, verwenden Computer eine Strategie namens „Divide and Conquer“ (Teile und Herrsche). Anstatt das ganze Puzzle auf einmal zu lösen, teilen sie das große Puzzle in zwei kleinere Stapel auf. Diese Stapel werden dann an verschiedene Arbeiter (Computer-Kerne) gesendet, die sie gleichzeitig lösen.

Die entscheidende Frage lautet: Wie entscheiden Sie, wo Sie das Puzzle zerschneiden?

Wenn Sie an der falschen Stelle schneiden, erhalten Sie vielleicht zwei riesige, schwierige Stapel, die immer noch ewig zur Lösung brauchen.
Wenn Sie an der richtigen Stelle schneiden, lösen Sie vielleicht die eine Hälfte sofort oder machen die verbleibende Hälfte sehr einfach.

Derzeit verwenden Computer handgefertigte Regeln (Heuristiken), um zu entscheiden, wo sie schneiden. Denken Sie bei diesen manuellen Regeln an ein Rezept, das von einem Koch geschrieben wurde, der die spezifischen Zutaten in Ihrer Küche noch nie probiert hat. Der Koch könnte sagen: „Schneide immer zuerst das rote Teil an“, aber manchmal ist ausgerechnet das rote Teil der schwierigste Teil des Puzzles. Diese manuellen Regeln sind oft suboptimal und erfordern viel menschliche Arbeit, um sie anzupassen.

Die Lösung: Owl (Der lernende Koch)

Die Autoren dieses Papers führen ein neues Werkzeug namens Owl ein. Anstatt sich auf ein statisches Rezept zu verlassen, ist Owl ein datengesteuerter Lerner. Owl beobachtet den Computer beim Lösen tausender Puzzles, lernt aus seinen Fehlern und findet heraus, wie man das Puzzle für jedes spezifische Instanz am besten schneidet.

So funktioniert Owl, unter Verwendung einer einfachen Analogie:

1. Der alte Weg: Der „Geschmackstest“ (Paarweise Klassifizierung)

Frühere Versuche, dies zu automatisieren, nutzten eine Methode, die einem Blindverkostungstest ähnelt. Um zwischen zwei Teilen (Teil A und Teil B) zu entscheiden, fragte der Computer: „Wenn ich A wähle, ist es besser als B?“ Dies geschah für jedes mögliche Paar.

Der Fehler: Dies ist langsam und fehleranfällig. Wenn der Computer früh einen kleinen Fehler macht (denkt, A sei besser als B), summiert sich dieser Fehler auf, was zu einer schrecklichen endgültigen Entscheidung führt. Es ist, als würde man versuchen, 100 Songs zu bewerten, indem man sie nur paarweise miteinander vergleicht; ein einzener schlechter Vergleich ruiniert die gesamte Liste.

2. Der Owl-Weg: Die „Zeitreise“ (Regression)

Owl verfolgt einen klügeren Ansatz. Anstatt zu fragen „Ist A besser als B?“, fragt es: „Wie lange wird es dauern, das Puzzle zu lösen, wenn ich A wähle?“ und „Wie lange dauert es, wenn ich B wähle?“

Die Analogie: Stellen Sie sich vor, Sie sind ein Projektmanager. Anstatt Ihr Team zu fragen: „Ist Aufgabe A besser als Aufgabe B?“, fragen Sie Ihren KI-Assistenten: „Wenn wir Aufgabe A erledigen, wie viele Stunden wird das Projekt dauern? Wenn wir Aufgabe B erledigen, wie viele Stunden?“
Der Vorteil: Die KI liefert eine spezifische Zahl (z. B. „Aufgabe A dauert 2 Stunden, Aufgabe B dauert 10 Stunden“). Dies bewahrt das vollständige Bild. Sie wissen nicht nur, dass A „besser“ ist; Sie wissen, dass es viel besser ist. Dies vermeilt die Fehlerkette, die bei der alten Methode auftritt.

3. Die Merkmale: In die Kristallkugel schauen

Um diese Vorhersagen zu treffen, nutzt Owl zwei Arten von Hinweisen (Features):

Statische Merkmale: Diese sind vergleichbar mit dem Blick auf den Deckel des Puzzle-Kartons. Sie verraten Owl die Form der Teile, wie viele rote Teile es gibt und die allgemeine Komplexität des Bildes.
Dynamische Merkmale: Dies ist vergleichbar mit dem Beobachten des Zusammenbaus eines Puzzles in Echtzeit. Owl prüft: „Hat dieses Teil schon einmal zu Konflikten geführt? Sieht es so aus, als würde es andere Teile schnell freischalten?“

Durch die Kombination dieser Hinweise baut Owl ein Modell, das die „Lösungszeit“ für jeden potenziellen Schnitt vorhersagt. Es wählt dann den Schnitt, der die kürzeste Zeit verspricht.

Die Ergebnisse: Schneller und klüger

Die Autoren haben Owl auf zwei der weltweit besten Puzzle-Solver (Z3seq und Z3str4) getestet. Sie fanden heraus:

Mehr gelöste Puzzles: Mit der Hilfe von Owl lösten die Computer signifikant mehr Puzzles, bevor ihnen die Zeit ausging. Beispielsweise löste Z3seq mit 4 Arbeitern 46 mehr Puzzles, als es allein gekonnt hätte.
Schnellere Geschwindigkeit: Die durchschnittliche Zeit zur Lösung eines Puzzles sank um etwa 44 % bis 59 %.
Skalierbarkeit: Je mehr Arbeiter (Computer-Kerne) sie hinzufügten, desto besser performte Owl, was beweist, dass es ein Team effektiv managen kann.

Zusammenfassung

Kurz gesagt ersetzt dieses Paper die „Rate-und-Prüfe“-Regeln für das Aufteilen komplexer Textprobleme durch ein kluges, lernendes System. Anstatt zu fragen „Welches ist besser?“, fragt das System „Wie lange wird das dauern?“ und nutzt diese präzise Antwort, um die beste Entscheidung zu treffen. Dies verwandelt einen langsamen, fehleranfälligen Prozess in einen schnellen, effizienten Prozess und ermöglicht es Computern, komplexe String-Probleme wesentlich effektiver zu lösen.

Technisches Resümee: Erlernen von Splitting-Heuristiken für parallele String-Solver

Problemstellung

String-Constraint-Solver sind essenziell für die Verifizierung von String-manipulierenden Programmen in Domänen wie der Durchsetzung von Sicherheitsrichtlinien und der symbolischen Ausführung. Viele praktische String-Constraints sind jedoch unentscheidbar, und bestehende Solver haben oft mit Skalierbarkeit und komplexen realen Instanzen zu kämpfen. Während Multi-Core-Architekturen eine Chance für das parallele Lösen bieten, hängt die Effektivität von Divide-and-Conquer-Strategien (speziell Cube-and-Conquer) stark von der Qualität der Splitting-Heuristiken ab. Diese Heuristiken bestimmen, auf welches Atom (Constraint) verzweigt werden soll, um den Suchraum in Teilprobleme zu partitionieren.

Aktuelle Splitting-Heuristiken sind typischerweise manuell entworfen und statisch. Sie versäumen es oft, sich an die spezifischen strukturellen Charakteristika einzelner Constraint-Instanzen anzupassen. Zudem leiden bestehende automatisierte Ansätze im SAT-Bereich, wie etwa die paarweise Klassifizierung, unter erheblichen Einschränkungen, wenn sie auf SMT-String-Solving angewendet werden:

Verlust quantitativer Informationen: Die Reduktion von Lösungszeiten auf binäre Labels verwirft feingranulare Kosten-Daten.
Kaskadierende Fehler: Serielle Vergleiche in der paarweisen Klassifizierung führen zu einer Fehlerakkumulation, was die Vorhersagequalität verschlechtert.
Skalierbarkeit: Paarweise Methoden erfordern lineare (oder schlechtere) Scans über Kandidatenpaare, was rechenintensiv ist.
Domänenanwendbarkeit: Vorherige automatisierte Methoden wurden primär in SAT validiert, wobei ihre Anwendbarkeit auf SMT-Theorien wie Strings unbewiesen bleibt.

Methodik

Die Autoren führen Owl ein, ein datengesteuertes Framework, das automatisch Splitting-Heuristiken für parallele String-Solver generiert. Die Kerninnovation besteht darin, das Problem der Atom-Auswahl von einer Klassifizierungsaufgabe in eine Regressionsaufgabe umzuformulieren.

1. Problemformulierung als Regression

Anstatt zwei Atome zu vergleichen, um zu bestimmen, welches „besser“ ist (Klassifizierung), sagt Owl die kontinuierliche Lösungszeit ( $Time(\varphi, p)$ ) voraus, die erforderlich ist, um die durch das Splitting auf ein bestimmtes Atom $p$ induzierten Teilprobleme zu lösen.

Definition der Kosten: Die Zielvariable wird basierend auf dem Ergebnis der parallelen Ausführung der beiden Zweige ( $\varphi \land p$ und $\varphi \land \neg p$ ) definiert. Wenn beispielsweise beide Zweige erfüllbar sind, sind die Kosten die minimale Lösungszeit ihrerseits; wenn beide unerfüllbar sind, sind die Kosten die maximale Lösungszeit.
Vorteil: Dieser Ansatz bewahrt die Kontinuität der Leistungsmetriken, vermeidet die Diskretisierungsfehler der Klassifizierung und eliminiert die Notwendigkeit erschöpfender paarweiser Vergleiche, wodurch der Inferenzaufwand reduziert wird.

2. Feature-Engineering

Um das Regressionsmodell zu unterstützen, haben die Autoren ein umfassendes Feature-Set von 77 Features für jedes Kandidatenatom entworfen, das in zwei Kategorien unterteilt ist:

Statische Features (66 Features): Abgeleitet aus der Struktur der Formel ohne Ausführung des Solvers. Dazu gehören Operator-Verteilungen (z. B. Zählungen von str.increment, re.union), Klauselgrößen und Graphen-Eigenschaften (z. B. Variable-Clause-Grade).
Dynamische Features (11 Features): Erfasst durch kurzfristige Lookahead- und Lookback-Heuristiken während der Solver-Ausführung.
- Lookback: Verfolgt historische Solver-Zustände, wie etwa die Anzahl der Male, in denen ein Atom in Konfliktklauseln oder gelernten Lemmas auftauchte.
- Lookahead: Simuliert eine begrenzte Constraint-Propagation (typischerweise begrenzt auf ~600 Konflikte), um unmittelbare Konsequenzen zu beobachten, wie etwa die Anzahl neuer Zuweisungen oder gelernter Klauseln.

3. Modellauswahl und Training

Algorithmus: Das System verwendet Random Forest Regression als zentrales prädiktives Modell. Diese Wahl balanciert Vorhersagegenauigkeit mit Inferenzgeschwindigkeit und Robustheit gegenüber verrauschten Labels (Variationen in den Lösungszeiten).
Trainingsdaten: Ein Datensatz wird erstellt, indem der Solver auf diversen Benchmark-Formeln ausgeführt, auf verschiedenen Atomen gesplittet und die resultierenden Lösungszeiten sowie Feature-Vektoren aufgezeichnet werden.
Bereitstellung: Das trainierte Modell wird in den Solver integriert (Z3seq und Z3str4). An jedem Entscheidungspunkt konstruiert der Solver eine Feature-Matrix für Kandidatenatome, sendet diese an einen parallelen Worker-Prozess via IPC und erhält das vorhersagte Atom mit der niedrigsten geschätzten Lösungszeit zurück.

Zentrale Beiträge

Neuartige Formulierung: Die Arbeit schlägt vor, das Design von Splitting-Heuristiken für das parallele String-Solving als Regressionsproblem statt als paarweise Klassifizierungsproblem neu zu konzipieren.
Praktisches Lern-Framework: Es führt ein Framework ein, das automatisch Heuristiken unter Verwendung eines reichhaltigen Sets aus 77 dedizierten Instanz-Features (statisch und dynamisch) generiert.
Implementierung und Evaluierung: Der Ansatz wird auf zwei State-of-the-Art String-Solvern, Z3seq und Z3str4, implementiert und evaluiert, wobei er signifikante Leistungssteigerungen gegenüber manuell entworfenen Heuristiken zeigt.

Experimentelle Ergebnisse

Die Autoren evaluierten Owl auf 1.024 QF_SLIA-Formeln aus dem SMT-LIB-Repository unter Verwendung von 4, 8, 16 und 32 Threads.

Lösungskapazität: Mit 4 Threads löste Z3seq(Owl) 46 Formeln mehr (eine Steigerung von 4,8 %) als die Baseline, und Z3str4(Owl) löste 9 Formeln mehr. Diese Verbesserungen blieben über alle Thread-Konfigurationen hinweg bestehen.
Laufzeitleistung:
- Z3seq(Owl) erreichte eine durchschnittliche Beschleunigung von 1,44× bei 32 Threads.
- Z3str4(Owl) erreichte eine durchschnittliche Beschleunigung von 1,59× bei 32 Threads.
Vorhersagegenauigkeit: Die Regressionsmodelle übertrafen die Standard-Lookahead-Heuristiken und eine paarweise Klassifizierungs-Baseline signifikant. Für Z3seq identifizierte das Modell die Top-20 % der Atome in fast 45 % der Fälle korrekt, verglichen mit der Zufallswahrscheinlichkeit der Baseline.
Overhead: Der Rechenaufwand für die Feature-Extraktion und Modell-Inferenz war minimal und machte nur 23,6 % der gesamten Lösungszeit aus, was mit dem Overhead der Standard-Lookahead-Heuristik vergleichbar oder sogar niedriger ist.
Feature-Wichtigkeit: Analysen zeigten, dass sich zwar die spezifischen Feature-Rankings zwischen den Solvern unterscheiden (was auf solver-spezifische Optimierungsbedarfe hindeutet), kritische Features wie „Anzahl der Zuweisungen“, „Lookahead-Score“ und spezifische String-Operation-Counts jedoch konsistent wichtig bleiben.

Bedeutung und Ansprüche

Das Paper behauptet, dass Owl einen bedeutenden Fortschritt im parallelen String-Constraint-Solving durch die Automatisierung des Designs von Splitting-Heuristiken darstellt. Durch die Verschiebung von manuellen, statischen Heuristiken hin zu datengesteuerten Regressionsmodellen passt sich der Ansatz effektiv an die spezifischen Charakteristika komplexer String-Constraints an.

Die Autoren betonen, dass ihre Methode:

Bestehende manuell erstellte Heuristiken sowohl in der Anzahl der gelösten Instanzen als auch in der durchschnittlichen Lösungszeit übertrifft.
Die Probleme der Fehlerakkumulation und des Informationsverlusts, die in paarweisen Klassifizierungsansätzen inhärent sind, mildert.
Demonstriert, dass gelernte Heuristiken effizient in bestehende CDCL( $T$ )-basierte Solver (Z3seq und Z3str4) integriert werden können, um das Potenzial paralleler Architekturen auszuschöpfen.

Die Arbeit kommt zu dem Schluss, dass, obwohl die Effizienz des sequentiellen Solvers die Gesamteschleunigung begrenzt, die gelernten Heuristiken die Parallelität effektiv maximieren, indem sie gut ausbalancierte Teilprobleme erzeugen, was zu substanziellen praktischen Verbesserungen der Lösungskapazität führt.