Thema3419: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Norbert Manthey (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Abschlussarbeit |Titel DE=Verbinden von Suchabstraktionen zur echten Suche |Titel EN=Relating Search Abstractions to Actual Search |Abschlussarbeitstyp=Bache…“) |
Markus Krötzsch (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
| Zeile 4: | Zeile 4: | ||
|Abschlussarbeitstyp=Bachelor, Master, Diplom, Studienarbeit | |Abschlussarbeitstyp=Bachelor, Master, Diplom, Studienarbeit | ||
|Betreuer=Norbert Manthey | |Betreuer=Norbert Manthey | ||
|Abschlussarbeitsstatus=Nicht mehr verfügbar | |||
|Abschlussarbeitsstatus= | |||
|Beschreibung DE=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. | |Beschreibung DE=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. | ||
|Beschreibung EN=Modern SAT solver are highly complex systems with many integrated techniques and heuristics. To make this technology available for teaching, we developed an abstraction: finding an exit in a maze. The task of this project is to find example formulas that are related to the special situations in the maze, such that a SAT solver behaves exactly like the agent in the maze. | |Beschreibung EN=Modern SAT solver are highly complex systems with many integrated techniques and heuristics. To make this technology available for teaching, we developed an abstraction: finding an exit in a maze. The task of this project is to find example formulas that are related to the special situations in the maze, such that a SAT solver behaves exactly like the agent in the maze. | ||
}} | }} | ||
Aktuelle Version vom 16. April 2021, 21:53 Uhr
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.
