දත්ත නර්තනය කරන ඇල්ගොරිතම-සහ සංකීර්ණ ගැටළු ඉක්මනින් විසඳන්න

සබැඳි වගුව

1 හැඳින්වීම

2 නැටුම් සබැඳි

3 රස්ට් ක්‍රමලේඛන භාෂාව

4 RAC: පරිමාණයෙන් දෘඪාංග/මෘදුකාංග සම-ඇෂුවරන්ස්

5 මලකඩ සහ RAR

5.1 සීමා සහිත ඇල්ගොරිතම මලකඩ

6 නැටුම් සබැඳි මලකඩ සහ 6.1 අර්ථ දැක්වීම්

6.2 ACL2 වෙත පරිවර්තනය

6.3 නැටුම් සබැඳි ප්‍රමේය

7 අදාළ වැඩ

8 නිගමනය

9 පිළිගැනීම් සහ යොමු කිරීම්

“ඩාන්සින් ලින්ක්ස්” මඟින් වේගවත් ලැයිස්තු මූලද්‍රව්‍ය ඉවත් කිරීම සහ ප්‍රතිසාධනය සඳහා සපයන චක්‍රලේඛ ද්විත්ව සම්බන්ධිත ලැයිස්තු දත්ත ව්‍යුහය ක්‍රියාත්මක කිරීම සඳහා ප්‍රශස්තකරණයක් අදහස් කරයි. ඩාන්සින් ලින්ක්ස් ප්‍රශස්තිකරණය ප්‍රධාන වශයෙන් වේගවත් ඇල්ගොරිතම වල නිවැරදි ආවරණ සෙවීම සඳහා භාවිතා කරන අතර, ක්නූත් විසින් ඔහුගේ මූලික කතා මාලාව වන ද ආර්ට් ඔෆ් කොම්පියුටර් ක්‍රමලේඛනයේ 4 බී වෙළුමේ ජනප්‍රිය කර ඇත. අපි රස්ට් ක්‍රමලේඛන භාෂාවෙන් ඩාන්සින් ලින්ක්ස් ප්‍රශස්තිකරණය ක්‍රියාත්මක කිරීමක් මෙන්ම ACL2 ප්‍රමේයය ප්‍රොවර් භාවිතයෙන් එහි විධිමත් සත්‍යාපනය විස්තර කරන්නෙමු. Amazon, Google, සහ Microsoft වැනි සමාගම්වල C/C++ හි නවීන මතක සුරක්ෂිත අනුප්‍රාප්තිකයෙකු ලෙස රස්ට් පසුගිය වසර කිහිපය තුළ සැලකිය යුතු අනුමැතියක් ලබාගෙන ඇති අතර Linux සහ Windows මෙහෙයුම් පද්ධති කර්නල් දෙකටම ඒකාබද්ධ වෙමින් පවතී. රස්ට් පිළිබඳ අපගේ උනන්දුව පැන නගින්නේ දෘඪාංග/මෘදුකාංග සම සහතික භාෂාවක් ලෙස, විවේචනාත්මක පද්ධති සඳහා යෙදෙන එහි විභවයෙනි. අපි Russinoff's Restricted Algorithmic C (RAC) මගින් ආනුභාව ලත් Rust උප කුලකයක් සකස් කර ඇත, එය අප විසින් පරිකල්පනීය ලෙස Restricted Algorithmic Rust හෝ RAR ලෙස නම් කර ඇත. පෙර වැඩ වලදී, අපි RAR මෙවලම් දාමයක් අපගේ මූලික ක්‍රියාත්මක කිරීම විස්තර කළෙමු, එහිදී අපි RAR මූලාශ්‍රය RAC වෙත සම්ප්‍රේෂණය කරමු. එසේ කිරීමෙන්, අපි දැනට පවතින දෘඪාංග/මෘදුකාංග සහ-ඇසුරුම් මෙවලම් ගණනාවක් අවම කාලය හා ශ්‍රමයේ ආයෝජනයකින් ප්‍රයෝජනයට ගනිමු. මෙම ලිපියෙන්, අපි RAR Rust උප කුලකය විස්තර කරන්නෙමු, අපගේ වැඩිදියුණු කළ මූලාකෘති RAR මෙවලම් දාමය විස්තර කරන්නෙමු, සහ RAR හි Dancing Links ප්‍රශස්තිකරණය භාවිතා කරන වෘත්තාකාර ද්විත්ව සම්බන්ධිත ලැයිස්තු දත්ත ව්‍යුහයක සැලසුම සහ සත්‍යාපනය විස්තර කරන්න, ක්‍රියාකාරී නිවැරදි බව පිළිබඳ සම්පූර්ණ සාක්ෂි සහිතව. ACL2 ප්‍රමේයය ඔප්පු කරන්න.

1 හැඳින්වීම

නිවැරදි ආවරණ ගැටලුව [17], එහි සරලම ආකාරයෙන්, ද්විමය මූලද්‍රව්‍ය සහිත n × m න්‍යාසයක් සඳහා, න්‍යාසයේ පේළිවල සියලුම උප කුලක, එනම් සියලුම තීරු එකතුව හරියටම එක ලෙස සෙවීමට උත්සාහ කරයි. මෙම මූලික සංකල්පය ස්වභාවිකව යම් සංඛ්‍යාත්මක පරාසයක ඇති අනුකෘති මූලද්‍රව්‍ය දක්වා විහිදේ; ඇත්ත වශයෙන්ම, ජනප්‍රිය ප්‍රහේලිකා ක්‍රීඩාවක් වන Sudoku යනු 1 සිට 9 දක්වා පරාසයක ඇති මූලද්‍රව්‍ය අගයන් සහිත 9× 9 න්‍යාසයක් සඳහා දීර්ඝ නිවැරදි ආවරණ ගැටලුවකි.

නිවැරදි ආවරණ ගැටළුව NP-සම්පූර්ණයි, නමුත් පරිගණක විද්‍යාඥයින් නිවැරදි ආවරණ සොයා ගැනීම සඳහා පුනරාවර්තන, නිර්ණය නොවන පසුගාමී ඇල්ගොරිතම නිර්මාණය කර ඇත. එවැනි එක් ක්‍රියා පටිපාටියක් වන්නේ [17] හි විස්තර කර ඇති Knuth's Algorithm X ය. මෙම ඇල්ගොරිතමයේ, අනුකෘතියේ මූලද්‍රව්‍ය චක්‍රාකාර ද්විත්ව-සම්බන්ධිත ලැයිස්තු හරහා සම්බන්ධ වන අතර, ඇල්ගොරිතම ඉදිරියට යන විට, පසුගාමී වීම යනාදී තනි මූලද්‍රව්‍ය ඉවත් කිරීම හෝ ප්‍රතිසාධනය කිරීම සිදු කෙරේ. මෙම ඉවත් කිරීම් සහ ප්‍රතිසාධන ලැයිස්තුවෙන් පිටත/ඇතුළට සිදු කිරීම සාමාන්‍ය දෙයකි. , මෙම මෙහෙයුම් කාර්යක්ෂම කිරීම ප්‍රශංසනීය ඉලක්කයකි. Knuth ගේ "Dancing Links" පැමිණෙන්නේ මෙහිදීය, Knuth DLX (ඇල්ගොරිතම X සඳහා යෙදෙන නර්තන සබැඳි) ලෙස හඳුන්වන නිවැරදි ආවරණ සොයා ගැනීම සඳහා ප්‍රශස්ත ඇල්ගොරිතමයක් ඇති කරයි.

2 නැටුම් සබැඳි

ඩාන්සින් ලින්ක්ස් පිටුපස ඇති සංකල්පය ඉතා සරල ය: ලැයිස්තුවක ලබා දී ඇති Y මූලද්‍රව්‍ය නිශ්චිත ආවරණ ඇල්ගොරිතමයකින් ඉවත් කළ විට, මෙම මූලද්‍රව්‍යය පසුව ප්‍රතිසාධනය වීමට බොහෝ දුරට ඉඩ ඇත. මේ අනුව, ඒ වෙනුවට

හොඳ ක්‍රමලේඛන සනීපාරක්ෂාව සාමාන්‍යයෙන් නියම කරන පරිදි, Y මූලද්‍රව්‍ය හා සම්බන්ධ 'පෙර' සහ 'ඊළඟ' සබැඳි "ශුන්‍යයට" වඩා, ඩාන්සින් ලින්ක්ස් හි, ක්‍රමලේඛකයා ඉවත් කරන ලද මූලද්‍රව්‍ය සඳහා සබැඳි අගයන් තබයි. ඩාන්සින් ලින්ක්ස් ඉවත් කිරීමේ ක්‍රියාකරු විසින් ලැයිස්තුවෙන් Y මූලද්‍රව්‍යය මකා දමයි, පෙර මූලද්‍රව්‍යයේ 'ඊළඟ' මූලද්‍රව්‍යය පහත සඳහන් Z මූලද්‍රව්‍යයට සකසයි, සහ Z හි 'පෙර' මූලද්‍රව්‍යය X වෙත සබැඳියක් ලෙස සකසයි, නමුත් 'ව ස්පර්ශ නොකරයි. ඉවත් කරන ලද Y මූලද්‍රව්‍යයේ ඊළඟ' සහ 'පෙර' සබැඳි. පසුව, Y ප්‍රතිසාධනය කිරීමට අවශ්‍ය නම්, එය සරල ප්‍රතිසාධන ක්‍රියාකරුවෙකු භාවිතයෙන් නැවත ලැයිස්තුවට සම්බන්ධ කරනු ලැබේ. Knuth ගේ වචන වලින් කිවහොත්, DLX ඇල්ගොරිතම ඉදිරියට යන විට යමෙක් ලැයිස්තු සබැඳි නිරීක්ෂණය කරන්නේ නම්, සබැඳි 'නටන්න' ලෙස දිස්වේ, එබැවින් නම. Knuth's Dancing Links ක්‍රියාකාරීත්වය රූප සටහන 1 හි සාරාංශ කර ඇත.