Wie schrieb Reto Aschwanden doch so schön zu seiner neuen Stelvio Version 4.2?
“Ein paar Verbesserungen da und dort, neben einem hässlichen Bug weniger…”
Der Fehler trat gelegentlich bei der Parallelisierung auf, und die Verbesserungen resultieren aus den noch tieferen Strategie-Analysen, die Reto im Zusammenhang mit der Prüfung der 57,5 Züge langen Beweispartie eingeführt hat.
Mehr Details gibt es natürlich in der Dokumentation, die wie immer lesenswert ist!
Kürzlich konnte Reto Aschwanden die Sensation vermelden: Es ist ihm mit seinem Prüfprogramm Stelvio gelungen, die Korrektheit der berühmten Beweispartie in 57,5 Zügen von Dmitri W. Pronkin und Andriy Frolkin nachzuweisen.
Dankenswerter Weise lässt er uns mit seinem für diesen Blog geschriebenen Artikel an der Geschichte dieser historischen, noch vor wenigen Jahren für absolut undenkbar gehaltenen Leistung der Verifizierung des 57.5-Beweispartie Längenrekords teilhaben: Der Computer-Laie bekommt einen gut nachvollziehbaren Eindruck von der Komplexität dieser Prüfung, und der Spezialist erhält zusätzliche Hinweise zur ausgefeilten Lösestrategie von Stelvio.
Und wir alle lernen nebenbei noch etwas über die richtige Lagerung von Wein …
Heute hat Reto Aschwanden eine neue Version von Stelvio veröffentlicht: Version 4.1 steht zum Download bereit.
Die neue Version enthält weitere Verbesserungen in der Strategieanalyse und damit potenziell eine weitere Beschleunigung der Prüfung speziell längerer Beweispartien, aber auch die Behebung eines “horrible bug”, der unter gewissen Umständen in Version 4.0 dazu führen konnte, dass eine Aufgabe fälschlich als korrekt ausgewiesen wurde.
Hintergründe und Empfehlungen, wie ihr damit umgehen könnt, gibt Reto speziell in der WhatsNew Datei — hier solltet ihr also unbedingt hineinschauen!
Nach längerer Zeit hat Reto Aschwanden heute eine neue Version von Stelvio veröffentlicht: Version 4.0 steht zum Download bereit.
Das Hochzählen der “Major Version” ist vollkommen berechtigt, es gibt viele Neuerungen. Die bedeutendste ist sicherlich, dass nun Prüfer-Angaben zu den von Stelvio verwendeten Strategien möglich sind. Damit verliert ein “korrekt”-Ergebnis natürlich das Prädikat “Computer-geprüft”. Heute schreibt man dafür ja gern HC+ (checked by human and computer).
Deshalb gilt meine Standard-Empfehlung Lest das Handbuch! bei dieser Version doppelt und dreifach!
Ja, ist denn heut’ schon Weihnachten?
Eigentlich nicht, wenn man auf den Kalender schaut — für die Freunde der orthodoxen Beweispartien aber in gewisser Weise schon, denn Reto Aschwanden hat heute die Version 2.0 von Stelvio, seinem Prüfprogramm für Beweispartien, veröffentlicht.
Bei einem Versionswechsel kann man schon damit rechnen, dass sich am Programm eine ganze Menge getan hat — und dem ist auch so:
Beispielsweise kann Stelvio nun unter gewissen Umständen notwendigen Schachschutz erkennen. Für Aufgaben, die den für einen der Könige benötigen, kann das eine drastische Beschleunigung der Tests bedeuten, da ein Schachschutz meist mehrere ansonsten freie Züge erfordert.
Allgemein hat Reto auch die Strategieanalyse verbessert und noch wirkungsvoller gemacht, ebenso die Parallelisierung der Prüfungen.
Insgesamt also eine Menge “Tuning unter der Motorhaube”, das den Versionssprung sicherlich gerechtfertigt. Mehr Details findet ihr wie immer in der Dokumentation.
Reto Aschwanden hat die Version 1.6 seine Beweispartie-Prüfprogramms Stelvio veröffentlicht. Ihr könnt sie wie immer von der Stelvio-Seite herunterladen!
Dieses Mal liegt der Schwerpunkt auf zusätzlicher Information für den Prüfer Reto schreibt dazu: “Hauptsächliche Neuigkeit ist die Visualisierung der Strategie-Suche, damit man eine Ahnung bekommt, ob man noch 10 Jahre oder nur noch 10 Sekunden warten muss, bis alle Strategien gefunden wurden.”
Hier könnt ihr schon mal einen Screenshot dazu sehen:
Reto Aschwanden hat die Version 1.5 seine Beweispartie-Prüfprogramms Stelvio veröffentlicht, die wegen meines Urlaubs zwei Tage hier gelegen hat. Ihr könnt sie wie immer von der Stelvio-Seite herunterladen!
Eine Menge Verbesserungen (Beschleunigungen, weniger Speicherbedarf) “unter der Motorhaube” gibt es. Das führt dazu, dass die Beweispartie in 58,5 Zügen in den ersten 51 Zügen in realistischer Zeit geprüft werden kann — danach allerdings “explodiert” der Suchbaum. aber “51 Züge” ist schon ein Wort: Davon hätte man bis vor Kurzem nicht einmal zu träumen gewagt …
Prüfprogramme für Beweispartien haben besonders dann große Probleme, in überschaubarer Zeit ein Prüfergebnis zu liefern, wenn sowohl bei Weiß als auch bei Schwarz “freie”, also nicht aus dem Diagramm ableitbare Züge vorhanden sind: Beim “Brute Force” Rechnen, also der Berücksichtigung aller theoretisch möglichen Züge, führt dies schnell zu extremen Prüfzeiten, die etwa exponenziell mit der Anzahl der freien Züge wächst. Wie sagte mal ein Professor während meines Studiums? “Nichts wächst so schnell wie exponenziell.” (Schaut euch mal die Ackermannfunktion an, wenn ihr sehen wollt, wie schnell “exponenziell” wachsen kann!)
Kann man einem Prüfprogramm nun “menschliche Erkenntnisse” zum Beispiel zu Reihenfolgen von Zügen oder zur Mindest- und Höchstzahl von Zügen eines Steins mitteilen, so kann man damit die Prüfzeiten drastisch verkürzen — man muss sich dabei “nur” darüber im Klaren sein, dass dies keine vollständige Computerprüfung darstellt, denn wenn die Überlegungen zu möglichen Einschränkungen (englisch: “constraints”) des Suchbaums einen Denk- oder Notationsfehler enthalten, kann das Ergebnis unseres Rechenknechts (englisch: “computer”) natürlich nicht korrekt sein.
Natch und Euklide enthalten rudimentäre Möglichkeiten, solche “constrains” einzugeben und zu nutzen; diese wurden bei Jacobi noch erweitert. In dem interessanten Artikel “Solving program Jacobi equipped with constraints — a new tool to check proof games” haben nun Michel Caillaud, Nicolas Dupont und François Labelle anhand von jeweils drei orthodoxen und Märchen-Beweispartien die Möglichkeiten ausführlich dargestellt. Dieser lesenswerte Artikel kann auf Julias Fairy-Seite als pdf-Datei gelesen bzw. direkt heruntergeladen werden.
Sehr empfehlenswerte Lektüre!