Prof. Dr. Jens Lehmann

Navigation: Info Pages → SMV System and Loyd's Puzzle

SMV System and Loyd's Puzzle

SMV-System

Die Ausarbeitung und die Präsentation zum Thema SMV-System war Thema eines Proseminars der Fakultät Informatik der TU Dresden im Sommersemester 2003. Das SMV-System is ein Mittel zur Verifizierung von Eigenschaften von Hard- und Softwaresystemen.

Loyd's Puzzle

Mit Hilfe des SMV-Systems habe ich ein Programm geschrieben, welches die Unlösbarkeit des Loyd-Puzzles zeigt. Sam Loyd war ein amerikanischer Puzzle-Erfinder in der zweiten Hälfte des 19. Jahrhunderts. 1878 brachte er ein Puzzle unter dem Namen "Loyd's Fifteen" bzw. "Loyd's Puzzle" heraus. Loyd bot jedem $1000 an, der eine Lösung des Puzzles präsentieren konnte. Eine Begeisterung für das Puzzle ging rund um die Welt, die bis zu Rubik's Würfel 1980 nicht übertroffen wurde. Jedesmal schien die Lösung des Puzzles nah zu sein, aber niemand schaffte es eine Lösung zu präsentieren.

Loyd's Puzzle ist ein einfaches Verschiebe-Puzzle, bei dem man einzelne Plättchen mit Hilfe eines freien Platzes verschieben kann. Anfangs- und Zielstellung (die sich nur durch das vertauschen von 14 und 15 unterscheiden) sind hier gezeigt:

Anfangsstellung
Anfangsstellung
      Zielstellung
Zielstellung

Downoad des SMV-Programms zum Nachweis der Unlösbarkeit: loyd_own_16.smv (2.9 KB)
Das Programm ist natürlich sehr rechenaufwändig, da es nicht auf das konkrete Problem hin optimiert ist ("State Explosion").

Unpublished Manuscripts

Presentations

print icon© 2001 - 2017, Jens Lehmann