Verbinden von Suchabstraktionen zur echten Suche

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
Toggle side column

Verbinden von Suchabstraktionen zur echten Suche

Thema nicht mehr verfügbar
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.