Auswahl von SAT-Instanzen zur Evaluation von Solvern

Aus SDQ-Institutsseminar
Version vom 19. Juli 2021, 12:14 Uhr von Jakob Bach (Diskussion | Beiträge)
(Unterschied) ← Nächstältere Version | Aktuelle Version (Unterschied) | Nächstjüngere Version → (Unterschied)
Vortragende(r) Youheng Lü
Vortragstyp Bachelorarbeit
Betreuer(in) Jakob Bach
Termin Fr 23. Juli 2021
Vortragsmodus
Kurzfassung Das schnelle und effiziente Lösen von SAT-Instanzen ist für viele Bereiche relevant, zum Beispiel Kryptografie, Scheduling oder formale Verifikationen. Um die Geschwindigkeit von SAT-Solvern zu evaluieren, gibt es SAT-Instanzenmengen, die die Solver lösen müssen. Diese Instanzenmengen (Benchmarks) bestehen aus Hunderten von unterschiedlichen Instanzen. Um ein repräsentatives Ergebnis zu erhalten, muss eine Benchmark viele unterschiedliche Instanzen haben, da unterschiedliche Solver auf unterschiedlichen Instanzen gut sind. Wir gehen aber davon aus, dass wir Benchmarks erstellen können, die kleiner als die aktuellen Benchmarks sind, die immer noch repräsentative Ergebnisse liefern.

In unserer Arbeit stellen wir einen Ansatz vor, der aus einer gegebenen repräsentativen Benchmark eine kleinere Teilmenge wählt, die als repräsentative Benchmark dienen soll. Wir definieren dabei, dass eine Benchmark repräsentativ ist, wenn der Graph der Laufzeiten ein festgelegtes Ähnlichkeitsmaß gegenüber der ursprünglichen Benchmark überschreitet. Wir haben hierbei einen BeamSearch-Algorithmus erforscht. Am Ende stellen wir allerdings fest, dass eine zufällige Auswahl besser ist und eine zufällige Auswahl von 10 % der Instanzen ausreicht, um eine repräsentative Benchmark zu liefern.