Auswahl von SAT Instanzen zur Evaluation von Solvern
| Vortragende(r) | Youheng Lü | |
|---|---|---|
| Vortragstyp | Proposal | |
| Betreuer(in) | Jakob Bach | |
| Termin | Fr 12. März 2021 | |
| Vortragsmodus | ||
| Kurzfassung | Das schnelle und effiziente Lösen von SAT-Instanzen ist für viele Bereiche relevant, zum Beispiel Kryptografie, Scheduling-Algorithmen oder formale Verifikation von Algorithmen. Um die Geschwindigkeit von SAT-Solvern zu evaluieren, gibt es die SAT Competition, in der verschiedene Solver gegeneinander antreten, um Hunderte von SAT-Instanzen zu lösen. Da dies viel Zeit beansprucht, möchten wir eine Methode vorschlagen, die die Anzahl der Instanzen verringert. Indem wir die Instanzen nach Eigenschaften und Laufzeiten clustern, möchten wir eine Benchmark erstellen, die deutlich weniger Instanzen beinhaltet, aber wenig Informationsverlust bietet. Diese evaluieren wir am Ende mithilfe einer „Benchmark“ Competition, wo wir vergleichen, ob die Sieger der SAT Competition auch die „Benchmark“ Competition gewinnen. Zusätzlich möchten wir in dieser Bachelorarbeit auch herausfinden, welche Instanzeigenschaften eine besondere Rolle beim Clustering spielen und ob ein Clustering von Solvern relevant ist. | |