Institutsseminar/2020-12-17

Termin (Alle Termine)
	Datum	Donnerstag, 17. Dezember 2020
	Uhrzeit	11:30 – 11:50 Uhr (Dauer: 20 min)
	Ort
	Webkonferenz	https://conf.dfn.de/webapp/conference/979111385
	Vorheriger Termin	Fr 11. Dezember 2020
	Nächster Termin	Fr 18. Dezember 2020

Termin in Kalender importieren: iCal (Download)

Vorträge

Vortragende(r)	Luc Mercatoris
Titel	Erklärbare k-Portfolios von SAT-Solvern
Vortragstyp	Proposal
Betreuer(in)	Jakob Bach
Vortragssprache
Vortragsmodus
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.