Algoritmas, kuris priverčia duomenis šokti ir greitai išspręsti sudėtingas problemas

Nuorodų lentelė

1 Įvadas

2 Šokių nuorodos

3 Rust programavimo kalba

4 RAC: bendras techninės ir programinės įrangos užtikrinimas mastu

5 Rūdys ir RAR

5.1 Riboto algoritmo rūdys

6 šokių nuorodos rūdyje ir 6.1 apibrėžimai

6.2 Vertimas į ACL2

6.3 Šokamųjų saitų teoremos

7 Susiję darbai

8 Išvada

9 Padėka ir nuorodos

„Šokančios nuorodos“ reiškia apskrito, dvigubai susieto sąrašo duomenų struktūros diegimo optimizavimą, kuris užtikrina greitą sąrašo elementų pašalinimą ir atkūrimą. „Dancing Links“ optimizavimas pirmiausia naudojamas greituose algoritmuose, siekiant rasti tikslius viršelius, ir jį išpopuliarino Knuthas savo pagrindinės serijos „Kompiuterių programavimo menas“ 4B tome. Mes aprašome Dancing Links optimizavimo įgyvendinimą Rust programavimo kalba, taip pat formalų jo patikrinimą naudojant ACL2 teoremos tikrintoją. „Rust“ per pastaruosius kelerius metus sulaukė didelio pritarimo kaip modernus, saugus atmintį C/C++ įpėdinis tokiose įmonėse kaip „Amazon“, „Google“ ir „Microsoft“, ir yra integruojamas į „Linux“ ir „Windows“ operacinių sistemų branduolius. Mūsų susidomėjimas Rust kyla iš jos, kaip techninės ir programinės įrangos bendro užtikrinimo kalbos potencialo, taikomo svarbioms sistemoms. Sukūrėme rūdžių poaibį, įkvėptą Russinoff's Restricted Algorithmic C (RAC), kurį išradingai pavadinome Restricted Algorithmic Rust arba RAR. Ankstesniame darbe aprašėme pradinį RAR įrankių grandinės įgyvendinimą, kai RAR šaltinį tiesiog perkeliame į RAC. Taip elgdamiesi su minimaliomis laiko ir pastangų investicijomis panaudojame daugybę esamų techninės ir (arba) programinės įrangos bendro užtikrinimo priemonių. Šiame darbe aprašome RAR Rust poaibį, aprašome patobulintą RAR įrankių grandinės prototipą ir išsamiai aprašome apskrito dvigubai susieto sąrašo duomenų struktūros projektavimą ir patikrinimą, naudojant Dancing Links optimizavimą RAR, su visais funkcinio teisingumo įrodymais, atliktais naudojant ACL2 teoremos tikrintojas.

1 Įvadas

Tikslus viršelio uždavinys [17], paprasčiausia forma, bando rasti n × m matricoje su dvejetainiais elementais visus matricos eilučių poaibius, kad visos stulpelių sumos būtų tiksliai viena. Ši pagrindinė sąvoka natūraliai apima matricos elementus, kurie yra tam tikrame skaitiniame diapazone; iš tiesų, populiarus dėlionės žaidimas Sudoku yra išplėstinė tiksli 9 × 9 matricos su elementų reikšmėmis nuo 1 iki 9 imtinai uždengimo problema.

Tiksli viršelio problema yra visiškai NP, tačiau kompiuterių mokslininkai sukūrė rekursinius, nedeterministinius atgalinio sekimo algoritmus, kad surastų tikslius viršelius. Viena iš tokių procedūrų yra Knutho algoritmas X, aprašytas [17]. Šiame algoritme matricos elementai sujungiami per apskritus, dvigubai susietus sąrašus, o atskiri elementai pašalinami arba atkuriami, kai algoritmas tęsiasi, grįžta atgal ir pan. Kadangi šie pašalinimai ir atkūrimai iš sąrašo/į jį yra gana dažni. veiksmingos šios operacijos yra pagirtinas tikslas. Čia atsiranda Knutho „Šokančios nuorodos“, todėl sukurtas optimizuotas algoritmas tikslių viršelių paieškai, kurią Knuthas vadina DLX (X algoritmui taikomos šokių nuorodos).

2 Šokių nuorodos

„Dancing Links“ koncepcija yra gana paprasta: kai tam tikras sąrašo elementas Y pašalinamas pagal tikslų viršelio algoritmą, labai tikėtina, kad vėliau tas pats elementas bus atkurtas. Taigi, veikiau

nei „nuliui“ su elementu Y susijusias „ankstesnes“ ir „kitas“ nuorodas, kaip paprastai diktuoja gera programavimo higiena, „Dancing Links“ programuotojas palieka pašalinto elemento nuorodų reikšmes. Operatorius „Dancing Links Remove“ pašalina elementą Y iš sąrašo, nustatydamas „kitą“ ankstesnio elemento X elementą į kitą elementą Z, o „ankstesnį“ elementą Z nustatydamas kaip nuorodą į X, bet neliesdamas „ Kitos ir ankstesnės pašalinto elemento Y nuorodos. Vėliau, jei Y reikės atkurti, jis tiesiog įtraukiamas atgal į sąrašą naudojant paprastą atkūrimo operatorių. Knutho žodžiais tariant, jei stebime sąrašo nuorodas, kai vyksta DLX algoritmas, nuorodos atrodo kaip „šokti“, taigi ir pavadinimas. Knutho Dancing Links funkcionalumas apibendrintas 1 pav.