Knight: il giro del cavallo







Il giro del cavallo


Il giro del cavallo

Sommario

Nel 1985 veniva stampato un testo unico nel suo genere: «Artificial Intelligence Projects for the Commodore 64». Presentiamo uno degli esempi più noti tratti da tale libro, il che ci fornisce un’ottima occasione per parlare di un problema scacchistico che ha interessato nei secoli matematici del calibro di Eulero, Legendre, Vandermonde e soprattutto della tecnica dimostrativa computazionale con la quale recentemente è stato risolto.

Come d’abitudine, l’articolo è disponibile anche in formato PDF (caldamente consigliato). Sono inoltre disponibili i sorgenti e il project file per CBM Prg Studio in formato ZIP.

«Sans les mathématiques on ne pénètre point au fond de la philosophie. Sans les philosophie on ne pénètre point au fond des mathématiques. Sans le deux, on ne pénètre point au fond de rien.»

(Gottfried W. Leibniz, 1646-1716)

Introduzione.

Scopo del presente articolo è la presentazione di un programma BASIC V2 che molti di noi «retroprogrammatori» si sono all’epoca divertiti a digitare durante lo studio di un testo più unico che raro sulla IA applicata al C64 [9]: uno dei primi testi applicativi di larga diffusione ad introdurre tecniche all’epoca altamente innovative, che solo molti anni dopo sarebbero state trattate sistematicamente in volumi di meritata fama come [10]. Il linguaggio è intenzionalmente informale, divulgativo e didascalico, scevro da particolari pretese di rigore, al fine di raggiungere il più vasto uditorio informatico possibile.

Knight’s tour.

Generare un singolo percorso, chiuso o aperto che sia, è un problema relativamente difficile che ha interessato molti tra i più grandi ingegni matematici, inclusi lo svizzero Eulero (Leonhard Euler, 1707–1783), Abraham de Moivre (1667–1754), Adrien-Marie Legendre (1752–1833), Alexandre-Théophile Vandermonde (1735–1796) e numerosi altri. La fama del problema è tale che si può tranquillamente asserire che non esista testo di ludomatematica e raccolta di rompicapo logici che non ne faccia menzione, in qualche forma. Nel 1823 H. C. von Warnsdorff descrisse una euristica [1] ancor oggi utilizzata, basata sulla scelta di una casella privilegiata in base al minimo numero di mosse disponibili: tale euristica, nonostante la sua scarsa efficienza computazionale, ha conosciuto una certa fortuna anche nell’epoca d’oro del retroprogramming, essendo usata come base di una implementazione in C (Acorn C, per l’esattezza) all’interno di un famosissimo testo di rompicapo informatici [5]. Il lettore interessato troverà una trattazione pressoché completa della storia del problema in http://www.mayhematics.com/t/1n.htm e una raccolta di fonti in http://www.velucchi.it/mathchess/knight.htm.
image: Numbered Closed Tour.gif
Figura 2: Esempio di percorso chiuso su una scacchiera non standard


6 × 6

con numerazione progressiva delle caselle visitate. A ciascuna cella viene assegnato un ordinale naturale che ne contraddistingue la posizione nella sequenza delle visite. In questo caso si è scelto di partire da zero, in modo che l’ordinale risponda alla domanda «quante celle precedono quella corrente?». Nell’ordine è implicito anche il verso di percorrenza, pertanto anche questo percorso, come quello illustrato in fig. 1, è un percorso chiuso diretto.

Dal punto di vista combinatorio e computazionale il problema si presta ovviamente a estensioni e generalizzazioni, tutte debitamente studiate da lungo tempo e oggetto di uno specifico teorema dovuto ad A. Schwenk [11] che determina l’esistenza dei percorsi in base alle dimensioni generiche


m × n

della scacchiera. In termini generali, chiedere se con un cavallo sia possibile occupare in successione tutte le


n × n

caselle di una scacchiera equivale a ricercare l’esistenza di un cammino hamiltoniano nel grafo equivalente, nel quale gli archi rappresentano le mosse e i nodi le caselle della scacchiera. Tradurre il problema in termini di grafi hamiltoniani significa quindi verificare se esiste nel grafo considerato almeno un cammino chiuso detto «ciclo hamiltoniano» che contiene ogni vertice del grafo una ed una sola volta; nel caso di percorso «aperto» come definito sopra, si tratta invece di cercare un «cammino hamiltoniano». Purtroppo è ben noto che ambedue i problemi, nella loro forma generale, sono NP-completi: la buona notizia è che invece la specifica istanza costituita dal problema di nostro interesse è computabile in tempo lineare, come dimostrato in [3]. Ben più difficile risulta il problema dell’enumerazione completa di tutti i possibili percorsi chiusi e aperti, tanto che sono occorsi vari secoli per addivenire ad una risposta definitiva inerente il problema originale e quindi la scacchiera standard


8 × 8

: i possibili percorsi chiusi diretti (ossia distinti anche per il verso in cui si attraversa una data sequenza di caselle, come quello in fig. 1) sono ben

26.534.728.821.064

e lapalissianamente, se ignoriamo il verso di percorrenza (si parla in questo caso di percorsi non diretti), tale valore si dimezza. Il conteggio è stato confermato circa venti anni fa unicamente tramite l’uso di sofisticate tecniche computazionali per l’enumerazione esaustiva. Nonostante l’enorme mole di energie profuse e la grande notorietà del problema da almeno undici secoli, infatti, solo in tempi recenti l’enumerazione dei percorsi chiusi ha trovato soluzione [12, 4], peraltro dopo una sfortunata falsa partenza a metà anni Novanta dovuta ad un errore di implementazione, mentre è recentissimo un tentativo di enumerazione computazionale dei percorsi aperti [8].

L’enumerazione delle soluzioni.

image: BDT.jpg
Figura 3: Costruzione di un albero di decisione binario BDT dalla relativa tabella di verità. Le linee tratteggiate, per convenzione, indicano il percorso da seguire quando la variabile nel nodo soprastante ha valore 0 o FALSE.

Un valore dell’ordine di ventiseimila miliardi di configurazioni per i giri del cavallo lascia facilmente intuire che una enumerazione esaustiva richiede elevate risorse computazionali per essere completata in tempi accettabili, come pure l’uso di appropriate strutture dati. In questo caso, a metà anni Novanta, sono stati utilizzati dei BDD (Binary Decision Diagrams, si veda [7]) e loro varianti, l’unica struttura dati in grado di garantire al tempo stesso la compattezza e la facilità di elaborazione richieste per una enumerazione massiva del genere. I BDD sono stati inizialmente concepiti come formalismo per la verifica di software e firmware per applicazioni critiche, tuttavia il loro recepimento a livello applicativo in tale settore è stato piuttosto tardo, mentre paradossalmente si sono quasi immediatamente diffusi nel mondo dei CAD EDA per la verifica a livello hardware di chip logici VLSI come microcontroller, SoC, CPU e altri chip ad elevata complessità.

image: OBDD.jpg
Figura 4: Applicando sequenzialmente le tre regole di eliminazione delle duplicazioni e delle ridondanze al BDT di fig. 3 si ottiene l’OBDD riportato più a destra.

Senza scendere nei dettagli, per non appesantire la trattazione, si propone solo un intuitivo esempio di elementare derivazione di OBDD (Ordered BDD) da una funzione booleana di tre variabili espressa tramite tabella di verità, nelle figure 3 e 4, tramite applicazione di una terna di regole di semplificazione e sintesi che non specifichiamo esplicitamente. Ciò che desideriamo qui è solo incuriosire il lettore e trasmettere l’idea che la rappresentazione con OBDD consta nella quasi totalità dei casi di un numero nettamente inferiore di nodi rispetto all’albero completo di partenza, pur rappresentando esattamente la medesima funzione booleana, senza perdita d’informazione: ciò è sufficiente ad intuirne la maggiore efficienza in spazio, come pure una generale riduzione del tempo complessivo di attraversamento ed elaborazione.

La dimostrazione computazionale di Wegener e Löbbing sul numero complessivo di percorsi chiusi del cavallo ha speciale rilevanza anche perché è parte di un importantissimo filone che annovera alcuni dei più grandi successi dell’uso del calcolatore in campo dimostrativo: una panoramica su tali dimostrazioni ottenute tramite il calcolatore sarebbe del tutto fuori luogo nel presente contesto, ma possiamo almeno citare il teorema dei quattro colori [2] o il problema delle arance di Keplero [6], forse tra i più emblematici e discussi esempi. Non occorre certo che il lettore possieda una specializzazione in teoria della dimostrazione e dei modelli per intuire che in questi casi il problema principale, rispetto ad una usuale dimostrazione matematica come concepita fin dai tempi di Euclide, si sposta dal garantire la correttezza del procedimento logico e la consequenzialità tra i singoli passaggi della dimostrazione al dover garantire la correttezza di uno (o più) programmi software e relativo hardware. Gli approcci normalmente seguiti in questi casi si basano indirettamente sulla molteplicità di prove indipendenti effettuate con hardware e software distinti, oppure (più frequentemente) sulla verifica formale diretta della correttezza del software e del funzionamento dell’hardware, argomento interessante e vastissimo quanto misconosciuto da una maggioranza di addetti ai lavori nel mondo IT. Il problema di Keplero appena citato è un ottimo e ben noto esempio di quest’ultima strategia di convalida formale della metodologia di prova basata su hardware/software.

Cenni sui metodi formali.

I metodi formali, come appena accennato, consentono di garantire in modo logicamente rigoroso che un software, firmware o anche un hardware rispettino una specifica, a sua volta formalizzata in modo non ambiguo. I linguaggi utilizzati in questo ambito sono detti appunto linguaggi formali e sono linguaggi simbolici, di natura strettamente logico-matematica, dotati di un vocabolario, di una sintassi e di una semantica non ambigua: il tutto specificato in modo formale e rigoroso. Esistono diverse classi di linguaggi formali sviluppati negli ultimi 35-40 anni di studio sul software engineering e sui metodi informazionali, nella branca meglio nota come VVT ossia (Software) Validation, Verification and Testing:
  • Linguaggi algebrici come LARCH, OBJ, LOTOS, CASL;
  • Linguaggi di modellazione come Z, VDM, CSP;
  • Reti di Petri, BDD, MDD, altri automi a stati finiti;
  • Logiche temporali lineari, circolari, branching (CTL*, da cui derivano CTL e LTL…);
  • Linguaggi più recenti, come OCL o Trio, basati sostanzialmente sui linguaggi di modellazione ibridati con altri simbolismi semiformali (es. UML). A tale proposito, il lettore presti particolare attenzione al fatto che sia UML che i diagrammi di flusso ISO 5807:1985 in tutte le loro varianti (es. Jackson) non sono in alcun modo linguaggi formali.
Esistono poi ulteriori approcci complementari alla verifica del software, sostanzialmente basati sulle semantiche formali dei linguaggi di programmazione, tra i quali spicca senz’altro l’interpretazione astratta, implementata in alcuni framework software di grande successo.
I linguaggi menzionati, e i loro affini, permettono in generale la specifica e la verifica di proprietà statiche ma anche dinamiche del software, secondo il tipo di linguaggio/framework: in molte occasioni la soluzione migliore è, infatti, la combinazione integrata di più metodi formali. Si noti tuttavia che l’uso di linguaggi formali fornisce le garanzie richieste senza l’uso di test, che sono notoriamente insufficienti dal punto di vista logico a garantire il funzionamento a specifica di un software, come già sottolineava il noto Edsger Dijkstra (1930–2002) negli anni Settanta. Non a caso infatti Dijkstra, fisico teorico dedicatosi per l’intera carriera all’informatica, è considerato uno dei più importanti precursori dell’uso sistematico dei metodi formali.
L’uso di un linguaggio formale richiede di operare una duplice astrazione di tipo matematico, a livello sia procedurale che rappresentativo: questo è il loro punto di estrema forza ed universalità, ma è anche causa di una serie di difficoltà operative nell’utilizzo, che richiede predisposizione, costanza e pratica assidua. Un linguaggio formale nasce sostanzialmente per assolvere a due scopi:
1)
Fornire una descrizione matematicamente corretta e non ambigua delle specifiche (specifica formale del software o livello 0); questo serve a comprendere perfettamente la specifica, aggirando i limiti del linguaggio naturale, evidenziando anche eventuali incongruenze della specifica stessa.
2)
Verificare in modo estremamente rigoroso, con una vera e propria dimostrazione logica – esattamente come un qualsiasi teorema – che il software scritto rispetti la specifica (verifica formale del software, livello 1).
Nella pratica invalsa sono riconosciuti tre livelli principali di uso e applicazione dei FL, con costi ovviamente diversi: si va dalla semplice specifica formale, allo sviluppo e verifica formali, fino alla completa dimostrazione di correttezza (“livello 2” in letteratura), il livello più esaustivo e dai costi più elevati.
Siamo consapevoli del fatto che molti lettori vedono menzionati qui per la prima volta i principali linguaggi formali e soprattutto le loro straordinarie capacità nel garantire la correttezza di software, firmware e hardware. Chi opera nel mercato mainstream ed è abituato a considerare inevitabile l’uso continuato di espressioni come «bug», «errore software», «patch», «vulnerabilità» ed altro può trovare difficile perfino concepire una simile realtà. Tuttavia, i metodi e i linguaggi formali sono la normalità quotidiana in tutti i settori nei quali sono fondamentali l’elevata affidabilità e sicurezza del sistema, definite quantitativamente dalle varie normative come EN 60880 (nucleare ed energetica), MIL-STD-498 (sistemi d’arma e tattici), ESA PSS05 (aerospaziale), EN 50128 (ferroviario), EN 61508 (sicurezza funzionale in ambito industriale) e le sue numerose derivate quali EN 61511 per l’industria di processo, EN 60601 per l’elettromedicale, etc.. I metodi formali, oltre ad essere il principale pilastro della proverbiale affidabilità dei sistemi embedded critici e anche di alcuni sofisticati sistemi di elaborazione mission-critical in ambito bancario o assicurativo, sono anche estremamente importanti in ambito delle organizzazioni tecnico-scientifiche come IEEE, ACM, ISO ed in generale nella definizione degli standard.
La recente normativa avionica RTCA DO-333 (applicata in realtà in un’ampia casistica di sistemi in vari settori industriali, militari e civili), la più rigorosa attualmente in vigore, regola e armonizza l’utilizzo di metodi formali nell’intero ciclo di sviluppo hardware, firmware e software. Sperabilmente avremo modo di tornare sull’argomento.

Il programma del testo.

Si presenta nel seguito il completo listato in BASIC V2 così come proposto da [9]. La data del testo, le inerenti limitazioni di potenza elaborativa della piattaforma e la stessa posizione del problema nel libro (si tratta in pratica del terzo listato del primo capitolo, dopo due semplici variazioni sulle torri di Hanoi ideate da F. Lucas nel diciannovesimo secolo) fanno immediatamente pensare che siamo ben lontani dalle vette di sofisticazione combinatoria ed enumerativa accennate nell’excursus sul problema affrontato nei paragrafi precedenti. Infatti, con doverosa onestà intellettuale, l’autore stesso sottolinea che non vi è traccia di «intelligenza» nel programma, in senso strettamente algoritmico: si tratta di un singolo percorso chiuso diretto pregenerato, i cui dati sono memorizzati negli statement DATA alle linee


601 ÷ 608

. L’unica elaborazione effettuata è il ricalcolo della sequenza data la casella di partenza. Non occorre tuttavia sottolineare come, trattandosi di un percorso chiuso che per definizione tocca tutte le 64 caselle, è in realtà del tutto indifferente da quale di esse si scelga di partire.

«This program is something of an expert system because the computer is able to quickly solve the problem from any first position.» ([9], pag. 16). L’autore conclude poi la sua descrizione del listato con la considerazione «The reason this program is included is that the compuler uses one set of data to solve a wide range of possibilities. I think that makes it somewhat intelligent. Intelligence is really making the best use of stored information.» (ibidem, pag. 20).
Mantenendo ben chiare queste premesse, il programma ha pur sempre una sua rilevante valenza didattica grazie alla grafica accattivante che mostra in tempo reale un’animazione con la successione completa delle mosse, marcando ogni casella con l’ordinale che la contraddistingue nel percorso e tenendo conto della locazione di partenza scelta arbitrariamente dall’utente.
10 ::::::::::::::::::::::::::::::::::::
20 REM KNIGHT'S TOUR    
30 REM    
40 REM COPYRIGHT 1983, TAB BOOKS INC.    
50 REM WRITTEN FOR THE COMMODORE 64    
60 ::::::::::::::::::::::::::::::::::::    
70 REM **** MAIN PROGRAM ****    
80 GOSUB200:REM DISPLAY INSTRUCTIONS    
90 GOSUB400:REM DEFINE GRAPHICS   
100 GOSUB600:REM DISPLAY SOLUTION   
110 OPEN1,0:INPUT#1,N$:CLOSE1:PRINTCHR$(147):POKE53281,6:POKES,0:POKES+1,0:END   
120 ::::::::::::::::::::::::::::::::::   
200 REM *** INSTRUCTIONS ***   
210 PRINTCHR$(147);:REM CLS   
220 PRINT:PRINTTAB(13);"knight's tour":PRINT   
230 PRINT"     this program displays a knight's"   
240 PRINT"tour that is, a knight in the game"   
250 PRINT"of chess can jump on all 64 squares"   
260 PRINT"of a chess board without landing on"   
270 PRINT"any square more than once."   
280 PRINT   
290 OPEN1,0   
300 PRINT"enter knight's starting position.":PRINT   
310 PRINT"enter the row.....:";:INPUT#1,R:PRINT   
320 PRINT"enter the column..:";:INPUT#1,C:PRINT   
330 CLOSE 1   
340 IFR<1ORR>8ORC<1ORC>8THEN290   
350 RETURN   
360 ::::::::::::::::::::::::::::::::::   
400 REM *** DEFINE GRAPHICS ***   
410 PRINTCHR$(147);:REM CLS   
420 FOR I=0TO63:READJ:POKE832+I,J:NEXTI   
430 DATA,,,,,,,,,,,   
440 DATA,8,,,30,,,63,,,127,   
450 DATA,111,,,15,,,31,,,62,   
460 DATA,62,,,28,,,62,,,127,   
470 DATA,127,,,,,,,,,,,,,,   
480 S=53248   
490 POKES+21,1:POKES+39,1   
500 POKES+23,1:POKES+29,1:POKE2040,13:POKE53281,14   
510 P=1016:L=-1:FORJ=1TO8:FORM=1TO3   
520 P=P+7:FORK=1TO8   
530 FORN=1TO4:P=P+1:POKEP,160:POKEP+54272,ABS(L)*3   
540 NEXTN:L=NOTL:NEXTK:P=P+1:NEXTM   
550 L=NOTL:NEXTJ:RETURN   
560 ::::::::::::::::::::::::::::::::::   
600 REM *** DISPLAY SOLUTION ***   
601 DATA 3,42,5,20,37,40,15,18   
602 DATA 6,21,2,41,16,19,36,39   
603 DATA 43,4,57,54,59,38,17,14   
604 DATA 22,7,62,1,56,53,60,35   
605 DATA 49,44,55,58,61,64,13,28   
606 DATA 8,23,48,63,52,29,34,31   
607 DATA 45,50,25,10,47,32,27,12   
608 DATA 24,9,46,51,26,11,30,33   
610 DIMBD(8,8),MD(8,8)   
615 FORJ=1TO8:FORK=1TO8:READMD(J,K):NEXTK,J   
620 N=0:X1=0:Y1=0   
625 FC=MD(R,C)-1   
626 FORJ=1TO8:FORK=1TO8:BD(J,K)=MD(J,K)-FC:IFBD(J,K)<1THENBD(J,K)=BD(J,K)+64   
627 NEXTK,J   
630 N=N+1:FORJ=1TO8:FORK=1TO8:IFBD(J,K)=NTHENR=J:C=K   
633 NEXTK,J   
635 P=1065+4*(C-1)+120*(R-1)   
640 V=48+INT(N/10):POKEP,V   
650 V=48+N-10*INT(N/10):POKEP+1,V   
660 X2=32*C-18:Y2=24*R+16:DX=X2-X1:DY=Y2-Y1   
670 IFABS(DY)>ABS(DX)THEN850   
680 FORJ=SGN(DX)TODXSTEPSGN(DX)   
690 X2=X1+J:Y2=Y1+J*DY/DX   
700 POKES,X2:POKES+1,Y2   
710 NEXTJ:IFN=64THENRETURN   
750 X1=X2:Y1=Y2:GOTO630   
850 FORJ=SGN(DY)TODYSTEPSGN(DY):Y2=Y1+J:X2=X1+J*DX/DY:GOTO700   
860 :::::::::::::::::::::::::::::::::: 
Si nota immediatamente come il semplice programma è organizzato in maniera molto ordinata, con una struttura fortemente modulare e una routine principale concisa e ben leggibile. Alle linee


200 ÷ 350

si stampano le semplici istruzioni e si chiedono le coordinate della cella di partenza (si noti l’uso dell’istruzione OPEN 1,0 per la lettura diretta della tastiera). Le linee


400 ÷ 500

gestiscono i quattro sprite che rappresentano graficamente il cavallo, mentre le linee immediatamente successive


510 ÷ 550

disegnano la scacchiera usando dei blocchi di


3 × 4

caratteri a colori alternati. Le linee


601 ÷ 608

contengono, come già accennato, una soluzione precalcolata con partenza al centro della scacchiera (riga 4, colonna 4): è il codice alle linee


620 ÷ 627

che effettua il semplice riordino della sequenza sulla base delle coordinate di partenza immesse dall’utente. Le linee


630 ÷ 850

gestiscono l’intera animazione: calcolano le coordinate alle quali stampare a video l’ordinale della mossa corrente, effettuano tale stampa, tracciano una linea retta che unisce i centri della casella corrente e di quella di destinazione, e infine creano l’animazione degli sprite che fornisce l’illusione del movimento continuo a velocità rallentata.

Conclusioni.

Si è presentata una brevissima storia del problema detto giro del cavallo, illustrando telegraficamente le sofisticate tecniche computazionali e strutture dati richieste per enumerare tutti i possibili percorsi chiusi e aperti. Questo ci ha fornito anche l’occasione per introdurre l’argomento dei metodi e linguaggi formali di specifica e verifica. Si è infine presentato il semplice ma efficace listato proposto nell’unico testo esistente inerente l’intelligenza artificiale applicata al C64, grazie al quale abbiamo potuto almeno accennare a tematiche logico-matematiche di grande importanza, sperando di suscitare curiosità e interesse nei lettori al di là del semplice codice proposto.

Riferimenti

1Karla Alwan and Kelly Waters, “Finding Re-entrant Knight’s Tours on N-by-m Boards“, in Proceedings of the 30th Annual Southeast Regional Conference (New York, NY, USA: ACM, 1992), pp. 377–382.
2Kenneth Appel and Wolfgang Haken, Every Planar Map Is Four Colorable (American Mathematical Society, 1989).
3Axel Conrad, Tanja Hindrichs, Hussein Morsy, and Ingo Wegener, “Solution of the knight’s Hamiltonian path problem on chessboards“, Discrete Applied Mathematics 50, 2 (1994), pp. 125 – 134.
4Brendan D. Mckay, “Knight’s Tours on an 8×8 Chessboard“, (2018).
5Simon Dally, Century/Acorn User Book of Computer Puzzles: v. 1 (The Century/Acorn User) (Century, 1984).
6Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, and Roland Zumkeller, “A formal proof of the Kepler conjecture“, ArXiv e-prints (2015), pp. arXiv:1501.02155.
7Donald E. Knuth, The Art of Computer Programming, Volume 4A: Combinatorial Algorithms, Part 1 (ADDISON WESLEY PUB CO INC, 2011).
8Ernesto Mordecki and Hector Cancela, “On the number of open knight’s tours“, (2015).
9Timothy J. O’Malley, Artificial Intelligence Projects for the Commodore 64 (Tab Books, Inc., 1985).
10Stuart Russell and Peter Norvig, Artificial Intelligence: A Modern Approach (3rd Edition) (Pearson, 2009).
11Allen Schwenk, “Which rectangular chessboards have a knight’s tour?“, Mathematics Magazine 64 (1991), pp. 325-332.
12Ingo Wegener, Branching Programs and Binary Decision Diagrams (SIAM – Society for Industrial and Applied Mathematics, 2000).


Have your say