I-Algorithm Eyenza Ukudansa Kwedatha—futhi Ukuxazulula Izinkinga Eziyinkimbinkimbi Ngokushesha

Ithebula Lezixhumanisi

1 Isingeniso

2 Izixhumanisi Zokudansa

3 The Rust Programming Language

4 RAC: Hardware/Software Co-Assurance at Scale

5 Ukugqwala kanye ne-RAR

5.1 Ukugqwala kwe-algorithmic okukhawulelwe

6 Izixhumanisi Zokudansa ku-Rust kanye 6.1 Izincazelo

6.2 Ukuhumusha ku-ACL2

6.3 Izithiyori Zezixhumanisi Zokudansa

7 Umsebenzi Ohlobene

8 Isiphetho

9 Ukubonga kanye Nezikhombo

I-"Dancing Links" isho ukuthuthukiswa ekusetshenzisweni kwesakhiwo sedatha yohlu oluxhunywe kabili oluyindilinga oluhlinzeka ngokususa nokubuyiselwa kwezinto zohlu ngokushesha. Ukwenziwa ngcono kwe-Dancing Links kusetshenziswa kakhulu kuma-algorithms asheshayo ukuze kutholwe amakhava aqondile, futhi kuye kwaduma u-Knuth kuVolumu 4B ochungechungeni lwakhe oluyisipesheli oluthi The Art of Computer Programming. Sichaza ukuqaliswa kokuthuthukiswa kwe-Dancing Links ngolimi lohlelo lwe-Rust, kanye nokuqinisekiswa kwakho okusemthethweni kusetshenziswa i-ACL2 theorem prover. I-Rust ithole ukugunyazwa okubalulekile eminyakeni embalwa edlule njengomlandeli wesimanje, ophephile kwinkumbulo ku-C/C++ ezinkampanini ezifana ne-Amazon, Google, ne-Microsoft, futhi ihlanganiswa kuzo zombili izinhlaka zesistimu yokusebenza ye-Linux ne-Windows. Intshisekelo yethu ku-Rust isukela emandleni ayo njengolimi lokuqinisekisa ngokubambisana kwezingxenyekazi zekhompiyutha/zesofthiwe, ngokusebenza ezinhlelweni ezibucayi. Senze isethi engaphansi ye-Rust, egqugquzelwe yi-Russinoff's Restricted Algorithmic C (RAC), esiyiqambe ngengqondo ukuthi Restricted Algorithmic Rust, noma i-RAR. Emsebenzini odlule, sichaze ukuqaliswa kwethu kokuqala kochungechunge lwamathuluzi lwe-RAR, lapho sivele siguqule umthombo we-RAR ku-RAC. Ngokwenza kanjalo, sisebenzisa inani lamathuluzi akhona wokuqinisekisa ngokubambisana wezingxenyekazi zekhompiyutha/zesofthiwe ngokutshalwa kwezimali okuncane kwesikhathi nomzamo. Kuleli phepha, sichaza isethi engaphansi ye-RAR Rust, sichaza uchungechunge lwethu lwamathuluzi oluthuthukisiwe lwe-RAR, futhi sichaza ngokuningiliziwe ukwakheka nokuqinisekiswa kwesakhiwo sedatha esiyindilinga esixhunywe kabili sisebenzisa ukuthuthukiswa kwe-Dancing Links ku-RAR, enobufakazi obugcwele bokufaneleka kokusebenza okufezwe kusetshenziswa I-ACL2 theorem prover.

1 Isingeniso

Inkinga yekhava okuyiyonayona [17], ngendlela yayo elula, izama ukuthola, ku-n × m matrix enezici kanambambili, wonke amasethi angaphansi emigqa ye-matrix ukuze zonke izibalo zekholomu zibe yinto eyodwa ncamashi. Lo mbono oyisisekelo udlulela ngokwemvelo ezintweni ze-matrix ezisebangeni elithile lezinombolo; ngempela, igeyimu yendida edumile i-Sudoku iyinkinga enwetshiwe yekhava ye-matrix engu-9× 9 enamanani ama-elementi kububanzi obungu-1 ukuya ku-9, ngokuhlanganisa.

Inkinga yekhava okuyiyonayona iphelele nge-NP, kodwa ososayensi bamakhompiyutha baklame izindlela zokuhlehlisa eziphindaphindayo, ezinganqunyelwe ukuze bathole izembozo eziqondile. Inqubo eyodwa enjalo i-Algorithm X ka-Knuth, echazwe ku- [17]. Kule algorithm, izingxenye ze-matrix zixhunywe ngezinhlu eziyisiyingi ezixhunywe kabili, futhi izakhi ngazinye ziyasuswa, noma zibuyiselwe, njengoba i-algorithm iqhubeka, ibhekana nokuhlehla, njll. Njengoba lokhu kususwa nokubuyiselwa kokuphuma/kufakwe ohlwini kuvame kakhulu. , ukwenza le misebenzi iphumelele kuwumgomo oncomekayo. Kulapho “Izixhumanisi Zokudansa” zika-Knuth zingena khona, okuholela ku-algorithm elungiselelwe yokuthola amakhava aqondile i-Knuth awabiza nge-DLX (Izixhumanisi Zokudansa zisetshenziswe ku-algorithm X).

2 Izixhumanisi Zokudansa

Umqondo we-Dancing Links ulula kakhulu: uma ingxenye engu-Y yohlu isuswa ku-algorithm yekhava ncamashi, maningi amathuba okuthi yona le nto izobuyiselwa kamuva. Ngakho, kunalokho

kunokuthi “ziro khipha” izixhumanisi 'zangaphambili' kanye 'nezilandelayo' ezihlotshaniswa ne-elementi Y, njengoba ukuhlanzeka okuhle kwezinhlelo ngokuvamile kungasho, kokuthi Izixhumanisi Zokudansa, umhleli ushiya amanani esixhumanisi endaweni yento esusiwe. I-Dancing Links isusa u-opharetha ngaleyo ndlela isusa i-elementi Y ohlwini, ibeka ingxenye 'elandelayo' ye-elementi X eyandulele engxenyeni engu-Z, bese ibeka ingxenye 'yangaphambili' ka-Z ibe isixhumanisi esiya ku-X, kodwa ingayithinti i-' izixhumanisi ezilandelayo' kanye 'nezangaphambili' zento esusiwe engu-Y. Kamuva, uma u-Y edinga ukubuyiselwa, ivele ixhunywe ohlwini kusetshenziswa isisebenzisi esilula sokubuyisela. Ngamagama ka-Knuth, uma umuntu eqapha uhlu luxhumanisa njengoba i-algorithm ye-DLX iqhubeka, izixhumanisi zibonakala 'ziyadansa', yingakho igama. Umsebenzi we-Knuth's Dancing Links ufinyezwa ku-Fig. 1.