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

Aus IPD-Institutsseminar
Zur Navigation springen Zur Suche springen
K (Ey6451 verschob die Seite Predicting the Performance of SAT Solvers nach Erklärbare k-Portfolios von SAT-Solvern: Änderung des Titels der Arbeit)
 
(kein Unterschied)

Aktuelle Version vom 14. Dezember 2020, 15:52 Uhr

Vortragende(r) Luc Mercatoris
Vortragstyp Proposal
Betreuer(in) Jakob Bach
Termin Do 17. Dezember 2020
Kurzfassung Das SAT-Problem ist eines der wohl bekanntesten NP-vollständigen Probleme. Hierbei handelt es sich um die Problemstellung, ob für eine gegebene aussagenlogische Formel G eine Variablenbelegung existiert, sodass G erfüllt ist.

Zum Lösen des SAT-Problems gibt es eine Vielzahl an unterschiedlichen Ansätzen, sogenannte SAT-Solver. Wie sich herausgestellt hat, ist die Performance der verschiedenen Solver jedoch stark von den jeweiligen Instanzen abhängig, für die es das SAT-Problem zu lösen gilt.

Deshalb interessiert man sich für Mengen von Solvern, die sich möglichst gut ergänzen, sogenannte Portfolios. Auf einem Portfolio wird dann mithilfe von Features der gegebenen Instanz eine Auswahl getroffen, welcher Solver wahrscheinlich der Beste ist.

Studien zeigen, dass solche Portfolios in ihrer Performance einzelnen Solvern weit überlegen sind, weshalb diese genauer untersucht werden sollten. Hauptaugenmerk der Arbeit liegt auf der Auswahl an möglichst kleinen Portfolios und auf kleinen Mengen von Instanzfeatures und der daraus resultierenden Performance.