Erklärbare k-Portfolios von SAT-Solvern (Verteidigung): Unterschied zwischen den Versionen

Aus SDQ-Institutsseminar
Keine Bearbeitungszusammenfassung
(kein Unterschied)

Version vom 10. Mai 2021, 15:13 Uhr

Vortragende(r) Luc Mercatoris
Vortragstyp Bachelorarbeit
Betreuer(in) Jakob Bach
Termin Fr 14. Mai 2021
Vortragsmodus
Kurzfassung Das SAT-Problem ist ein bekanntes NP-vollständiges Problem aus der theoretischen Informatik. Es handelt es sich um die Problemstellung, ob für eine gegebene aussagenlogische Formel G eine Variablenbelegung existiert, sodass G erfüllt ist.

Portfolio-basierte Methoden zum Lösen von SAT Instanzen nutzen die komplementäre Stärke von einer Menge von verschiedenen SAT Algorithmen aus. Hierbei wird aus einer gegebenen Menge von Algorithmen, dem sogenannten Portfolio, mittels eines Vorhersagemodells derjenige Algorithmus ausgewählt, der die bestmögliche Performance für die betrachtete SAT-Instanz verspricht.

In dieser Arbeit interessieren wir uns besonders für erklärbare Portfolios, sprich für Portfolios, für die man nachvollziehen kann, wie die Vorhersage zu ihrem Ergebnis kommt. Gute Erklärbarkeit resultiert einerseits aus einer geringen Größe des Portfolios, andererseits aus einer reduzierten Komplexität des Vorhersagemodells.

Im Vordergrund der Arbeit liegt das effiziente Finden von kleinen Portfolios aus einer größeren Menge von Algorithmen, sowie den Einfluss der Portfoliogröße auf die Performance des Portfolios.