Verbinden von Suchabstraktionen zur echten Suche
Aus International Center for Computational Logic
Verbinden von Suchabstraktionen zur echten Suche
Thema nicht mehr verfügbar
- Betreuer Norbert Manthey
- Beginn
Moderne SAT Solver sind sehr komplexe Systeme mit vielen integrierten Techniken und Heuristiken. Um diese intuitiv zu verstehen wurde eine Abstraktion entwickelt: die Suche eines Ausgangs in einem Labyrinth. Zu den verschiedenen Situationen im Labyrinth sollen entsprechende Formeln gefunden werden, sodass sich der SAT Solver bei der Suche genau so verhält wie der Agent im Labyrinth.