Algorithm-ka Ka Dhiga Dheefta Dance-iyo Xalinta Dhibaatooyinka Kakan

Shaxda Xiriirinta

1 Hordhac

2 Xidhiidhada Qoob ka ciyaarka

3 Luuqadda Barnaamijka Daxalka

4 RAC: Hubinta Wadashaqeynta Hardware/Software ee Miisaanka

5 miridhku iyo RAR

5.1 Daxalka Algorithmic xaddidan

6 Xidhiidhada qoob ka ciyaarka ee miridhku ku jiro iyo 6.1 Qeexitaanno

6.2 Tarjumaadda ACL2

6.3 Fikradaha Xiriirinta Qoob-ka-ciyaarka

7 Shaqada la xidhiidha

8 Gabagabo

9 Mahadnaq iyo Tix-raac

"Xiriirka Qoob-ka-ciyaarka" waxa uu tilmaamayaa hagaajinta qaab dhismeedka xogta liiska labajibaaran ee wareegtada ah kaas oo bixisa ka saarista iyo soo celinta liiska degdega ah. Hagaajinta isku xidhka qoob ka ciyaarka waxa loo adeegsadaa algorithms degdega ah si loo helo daboolo sax ah, waxaana caan ku ah Knuth oo ku jira Volume 4B ee taxanaheedii seminal The Art of Computer Programming. Waxaan ku sifeyneynaa hirgelinta hagaajinta Xiriirinta Qoob ka ciyaarka ee luqadda barnaamijka Rust, iyo sidoo kale xaqiijinteeda rasmiga ah iyadoo la adeegsanayo maahmaahiyaha ACL2. Rust waxa uu helay taageero la taaban karo dhowrkii sano ee la soo dhaafay isagoo ah ku guulaysta xusuusta badbaadada leh ee C/C++ ee shirkadaha sida Amazon, Google, iyo Microsoft, waxaana lagu dhex daray Linux iyo Windows kernels nidaamka hawlgalka. Xiisaha aanu u qabno Rust waxa ay ka imanaysaa awooddeeda luqadda hubinta qalabka/software, oo leh adeegsiga nidaamyada muhiimka ah. Waxa aanu samaynay qayb hoosaadka Rust, oo uu dhiiri galiyay Russinoff's Restricted Algorithmic C (RAC), kaas oo aanu si mala awaal ah ugu magac daray Rust Algorithmic Restricted, ama RAR. Shaqadii hore, waxaanu ku sharaxnay hirgalintayada bilowga ah ee qalabka RAR, kaas oo aan si fudud ugu gudbinay isha RAR RAC. Marka sidaas la sameeyo, waxaanu ka faa'iidaysanaynaa tiro ka mid ah agabka hubinta wada jirka ee hardware/software oo leh wakhtiga iyo dadaalka ugu yar ee jira. Warqadan, waxaan ku sifeyneynaa qeyb-hoosaadka RAR Rust, ku sifeyneynaa nooca qalabka RAR ee la wanaajiyey, waxaanan faahfaahineynaa naqshadeynta iyo xaqiijinta qaab dhismeedka xogta liiska labajibaaran ee wareegtada ah ee ka shaqeyneysa hagaajinta Xiriirinta Qoob ka ciyaarka ee RAR, oo leh cadeymo buuxa oo sax ah shaqeynta oo la dhammeeyey iyadoo la adeegsanayo ACL2 theorem maahmaah.

1 Hordhac

Dhibaatada dhabta ah ee daboolka ah [17], qaabka ugu fudud, waxay isku dayeysaa in la helo, n × m matrix leh walxo binary ah, dhammaan qaybaha hoose ee safafka shaxanka sida dhammaan wadarta tiirka waa mid sax ah. Fikraddan aasaasiga ah ayaa si dabiici ah u fidsan curiyayaasha matrixka kuwaas oo ku jira tiro tirooyin ah; Runtii, ciyaarta halxiraalaha caanka ah ee Sudoku waa dhibaatada daboolida saxda ah ee fidsan ee 9× 9 matrix leh qiyamka curiye ee u dhexeeya 1 ilaa 9, oo loo dhan yahay.

Dhibaatada dhabta ah ee daboolka ah waa NP-dhameystiran, laakiin saynisyahannada kombuyuutarku waxay sameeyeen algorithms dib-u-eegis ah oo aan la go'aamin si loo helo daboolo sax ah. Mid ka mid ah nidaamkan waa Knuth's Algorithm X, oo lagu sharaxay [17]. Algorithm-kan, canaasiirta jaantusku waxa ay ku xidhan yihiin liisas laba-laaban-xiran oo wareeg ah, xubno shakhsi ahna waa la saaray, ama dib loo soo celiyay, sida algoorithmamka, dib-u-socodka, iwm. , ka dhigista hawlgalladan kuwo hufan waa hadaf la mahadiyo. Tani waa meesha Knuth's "Xiriirka Qoob-ka-ciyaarka" uu ka yimaado, taasoo keentay in algorithm la hagaajiyay si loo helo daboolo sax ah oo Knuth ugu yeero DLX (Xiriirka Qoob-ka-ciyaarka lagu dabaqay algorithm X).

2 Xidhiidhada Qoob ka ciyaarka

Fikradda ka dambeysa Links-ka Qoob-ka-ciyaarka waa mid fudud: marka cutubka Y ee liiska laga saaro algorithm saxda ah ee daboolka, waxay aad ugu badan tahay in isla sheygan mar dambe dib loo soo celin doono. Sidaa darteed, halkii

Marka loo eego "eber ka baxsan" xiriirinta 'hore' iyo 'xiga' ee la xidhiidha curiyaha Y, sida nadaafadda barnaamijka wanaagsan ay caadiyan tilmaamayso, Links-yada qoob-ka-ciyaarka, barnaamij-sameeyaha wuxuu ka tagayaa qiyamka isku-xidhka ee qaybta meesha laga saaray. Xidhiidhada qoob-ka-ciyaarka waxa ay ka saarayaan hawl-wadeenka sidaas awgeed waxa ay liiska ka tirtirayaan curiyaha Y, iyaga oo dejinaya qaybta 'xigta' ee cunta hore X ee soo socota shaygan soo socda, oo waxa ay dejiyaan xubinta 'hore' ee Z xiriirinta X, laakiin aan taaban ' Xiga' iyo 'kii hore' ee curiyaha la saaray Y. Kadib, haddii Y u baahan tahay in dib loo soo celiyo, si fudud ayaa dib loogu soo celinayaa liiska iyadoo la isticmaalayo hawlwadeen fudud oo soo celin ah. Erayada Knuth, haddii mid ka mid ah uu kormeero liiska isku xirka sida DLX algorithm u socdo, xiriiriyayaashu waxay u muuqdaan 'dheesho', markaa magaca. Xidhiidhka qoob ka ciyaarka ee Knuth waxa lagu soo koobay sawirka 1.