Auswahl von SAT-Instanzen zur Evaluation von Solvern: Unterschied zwischen den Versionen

Aktuelle Version vom 19. Juli 2021, 13:14 Uhr

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.

@@ Zeile 5: / Zeile 5: @@
 |betreuer=Jakob Bach
 |termin=Institutsseminar/2021-07-23 Zusatztermin
-|kurzfassung=<To do>
+|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.
 }}