Erklärbare k-Portfolios von SAT-Solvern: Unterschied zwischen den Versionen
(Die Seite wurde neu angelegt: „{{Vortrag |vortragender=Luc Mercatoris |email=uxruc@student.kit.edu |vortragstyp=Proposal |betreuer=Jakob Bach |termin=Institutsseminar/2020-12-17 |kurzfassung…“) |
K (Ey6451 verschob die Seite Predicting the Performance of SAT Solvers nach Erklärbare k-Portfolios von SAT-Solvern: Änderung des Titels der Arbeit) |
||
| (Eine dazwischenliegende Version desselben Benutzers wird nicht angezeigt) | |||
| Zeile 5: | Zeile 5: | ||
|betreuer=Jakob Bach | |betreuer=Jakob Bach | ||
|termin=Institutsseminar/2020-12-17 | |termin=Institutsseminar/2020-12-17 | ||
|kurzfassung= | |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. | |||
}} | }} | ||
Aktuelle Version vom 14. Dezember 2020, 15:52 Uhr
| Vortragende(r) | Luc Mercatoris | |
|---|---|---|
| Vortragstyp | Proposal | |
| Betreuer(in) | Jakob Bach | |
| Termin | Do 17. Dezember 2020 | |
| 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. | |