Ny Algorithm Mampidihy Data—ary mamaha haingana ny olana sarotra

Latabatra Rohy

1 Fampidirana

2 Rohy mandihy

3 Ny fiteny Programming Rust

4 RAC: Fiaraha-miasa amin'ny Hardware/Software amin'ny ambaratonga

5 Rust sy RAR

5.1 harafesina algorithmic voafetra

6 Rohy mandihy amin'ny harafesina sy famaritana 6.1

6.2 Dikanteny amin'ny ACL2

6.3 Dihy Rohy Theorem

7 Asa mifandray

8 Famaranana

9 Fankasitrahana sy fanovozan-kevitra

Ny "Rohy Dihy" dia manondro fanatsarana ny fametrahana rafitra angon-drakitra misy rohy roa mifamatotra izay manome ny fanesorana sy famerenana amin'ny laoniny ny singa lisitra haingana. Ny optimization Dancing Links dia ampiasaina voalohany indrindra amin'ny algorithm haingana hahitana ny fonony marina, ary nalaza tamin'i Knuth ao amin'ny Boky 4B amin'ny andian-tantarany The Art of Computer Programming. Manoritsoritra ny fampiharana ny fanatsarana ny Dancing Links amin'ny fiteny fandaharana Rust izahay, ary koa ny fanamarinana ara-dalàna amin'ny fampiasana ny prover theorem ACL2. Nahazo fankatoavana manan-danja i Rust tato anatin'ny taona vitsivitsy ho toy ny mpandimby maoderina sy azo antoka ho an'ny C/C ++ amin'ny orinasa toa an'i Amazon, Google, ary Microsoft, ary ampidirina ao anatin'ny kernel rafitra fandidiana Linux sy Windows. Ny fahaliananay amin'ny Rust dia avy amin'ny mety ho fiteny iaraha-miasa amin'ny fitaovana/rindrambaiko, miaraka amin'ny fampiharana amin'ny rafitra mitsikera. Namorona ampahany amin'ny Rust izahay, aingam-panahy avy amin'ny Russinoff's Restricted Algorithmic C (RAC), izay nomenay an-tsaina hoe Restricted Algorithmic Rust, na RAR. Tamin'ny asa teo aloha, dia nanoritsoritra ny fampiharana voalohany ny RAR toolchain izahay, izay amidinay fotsiny ny loharano RAR ho ao amin'ny RAC. Amin'ny fanaovana izany, dia mampiasa fitaovana maromaro miaraka amin'ny fanomezan-toky ny hardware/logiciel izahay miaraka amin'ny fampiasam-bola kely indrindra amin'ny fotoana sy ezaka. Ato amin'ity lahatsoratra ity, dia mamaritra ny RAR Rust subset, mamaritra ny fanatsarana ny prototype RAR rojom-pitaovana, ary amin'ny antsipiriany ny famolavolana sy ny fanamarinana ny faribolana boribory misy rohy roa rafitra angon-drakitra mampiasa ny Dancing Links Optimization ao amin'ny RAR, miaraka amin'ny porofo feno momba ny asa marina vita tamin'ny fampiasana ny ACL2 theorem prover.

1 Fampidirana

Ny olan'ny fonony marina [17], amin'ny endriny tsotra indrindra, dia manandrana mitady, ho an'ny matrice n × m misy singa binary, ny ampahany rehetra amin'ny andalana amin'ny matrix ka ny fitambaran'ny tsanganana dia iray marina. Ity hevitra fototra ity dia miitatra amin'ny singa matrix izay ao anatin'ny salan'isa sasany; Eny tokoa, ny lalao piozila malaza Sudoku dia olan'ny fonony miitatra ho an'ny matrice 9×9 misy sanda singa ao anatin'ny 1 hatramin'ny 9, tafiditra ao anatin'izany.

Ny tena olan'ny fonony dia ny NP-complete, fa ny mpahay siansa momba ny solosaina dia namolavola algorithm miverimberina tsy voafaritra mba hahitana ny fonony marina. Ny fomba iray toy izany dia ny Algorithm X an'i Knuth, voalaza ao amin'ny [17]. Ao anatin'ity algorithm ity, ny singa ao amin'ny matrix dia mifandray amin'ny alàlan'ny lisitra misy ifandraisany roa, ary ny singa tsirairay dia esorina, na averina amin'ny laoniny, rehefa mandeha ny algorithm, mihemotra, sns. , tanjona mendri-piderana ny fanatanterahana ireo asa ireo. Eo no idiran'ny "Rohin'ny Dihy" an'i Knuth, ka nahatonga ny algorithm nohatsaraina hitadiavana fonony marina izay antsoin'i Knuth hoe DLX (Rohy Dihy ampiharina amin'ny algorithm X).

2 Rohy mandihy

Ny foto-kevitra ao ambadiky ny Dancing Links dia tsotra: rehefa esorina amin'ny algorithm fandrakofana marina ny singa Y amin'ny lisitra iray, dia azo inoana fa haverina amin'ny laoniny io singa io any aoriana. Noho izany, raha ny marina

noho ny "aotra" ny rohy 'teo aloha' sy 'manaraka' mifandray amin'ny singa Y, satria ny fahadiovan'ny fandaharana tsara dia matetika no mandidy, ao amin'ny Dancing Links, ny programmer dia mamela ny soatoavin'ny rohy ho an'ilay singa nesorina. Ny Dancing Links manala ny operator dia mamafa ny singa Y amin'ny lisitra, mametraka ny singa 'manaraka' amin'ny singa X eo aloha amin'ity singa Z manaraka ity, ary mametraka ny singa 'teo aloha' amin'ny Z amin'ny rohy mankany X, fa tsy mikasika ny ' rohy manaraka' sy 'teo aloha' amin'ny singa Y nesorina. Taty aoriana, raha mila averina amin'ny laoniny ny Y, dia averina amin'ny lisitra fotsiny amin'ny alalan'ny opérateur famerenana tsotra. Araka ny tenin'i Knuth, raha misy manara-maso ny lisitry ny rohy rehefa mandeha ny algorithm DLX, dia toa 'mandihy' ireo rohy, noho izany ny anarana. Ny fiasan'ny Dancing Links an'i Knuth dia fintinina ao amin'ny sary 1.