paint-brush
Verileri Dans Ettiren ve Karmaşık Sorunları Hızlı Çözen Algoritmaile@knuth

Verileri Dans Ettiren ve Karmaşık Sorunları Hızlı Çözen Algoritma

ile Knuth
Knuth HackerNoon profile picture

Knuth

@knuth

Knuth's mastery weaves theory and practice, a tale of computation,...

3 dk. read2025/01/21
Read on Terminal Reader
Read this story in a terminal
Print this story
tldt arrow
tr-flagTR
Bu hikayeyi Türkçe okuyun!
en-flagEN
Read this story in the original language, English!
de-flagDE
Lesen Sie diese Geschichte auf Deutsch!
es-flagES
Lee esta historia en Español!
ja-flagJA
この物語を日本語で読んでください!
mg-flagMG
Vakio amin'ny teny malagasy ity tantara ity!
he-flagHE
קרא את הסיפור הזה בעברית!
so-flagSO
Sheekadan Af-Soomaali ku akhri!
ky-flagKY
Бул окуяны кыргызча окуңуз!
si-flagSI
මේ කතාව සිංහලෙන් කියවන්න!
ay-flagAY
¡Aka sarnaqäw aymar arun ullart’apxam!
zu-flagZU
Funda le ndaba ngesiZulu!
lt-flagLT
Skaitykite šią istoriją lietuvių kalba!
TR

Çok uzun; Okumak

Araştırma, Rust'ın Knuth'un Dans Eden Bağlantılar optimizasyonunun uygulanmasını, ACL2 aracılığıyla resmi doğrulama ile, tam örtü sorunu için verimli ve güvenli çözümler hedefleyerek araştırıyor
featured image - Verileri Dans Ettiren ve Karmaşık Sorunları Hızlı Çözen Algoritma
Knuth HackerNoon profile picture
Knuth

Knuth

@knuth

Knuth's mastery weaves theory and practice, a tale of computation, in the realm of computer science.

0-item

STORY’S CREDIBILITY

Academic Research Paper

Academic Research Paper

Part of HackerNoon's growing list of open-source research papers, promoting free access to academic material.

Yazar:

(1) David S. Hardin, Cedar Rapids, IA ABD (david.s.hardin@gmail.com).

Bağlantılar Tablosu

1 Giriş

2 Dans Bağlantısı

3 Rust Programlama Dili

4 RAC: Ölçekte Donanım/Yazılım Ortak Güvencesi

5 Pas ve RAR

5.1 Sınırlı Algoritmik Rust

Rust'ta 6 Dans Eden Bağlantı ve 6.1 Tanımları

6.2 ACL2'ye Çeviri

6.3 Dans Bağlantıları Teoremleri

7 İlgili Çalışma

8 Sonuç

9 Teşekkürler ve Referanslar


"Dancing Links", hızlı liste öğesi kaldırma ve geri yükleme sağlayan dairesel çift bağlantılı liste veri yapısı uygulamasına yönelik bir optimizasyonu ifade eder. Dancing Links optimizasyonu, esas olarak tam örtüleri bulmak için hızlı algoritmalarda kullanılır ve Knuth tarafından çığır açan The Art of Computer Programming serisinin 4B Cildinde popüler hale getirilmiştir. Rust programlama dilinde Dancing Links optimizasyonunun bir uygulamasını ve ACL2 teorem kanıtlayıcısını kullanarak resmi doğrulamasını açıklıyoruz. Rust, Amazon, Google ve Microsoft gibi şirketlerde C/C++'ın modern, bellek açısından güvenli bir halefi olarak son birkaç yılda önemli bir destek topladı ve hem Linux hem de Windows işletim sistemi çekirdeklerine entegre ediliyor. Rust'a olan ilgimiz, kritik sistemlere uygulanmasıyla bir donanım/yazılım eş güvence dili olarak potansiyelinden kaynaklanmaktadır. Russinoff'un Sınırlandırılmış Algoritmik C'sinden (RAC) esinlenerek, yaratıcı bir şekilde Sınırlandırılmış Algoritmik Rust veya RAR adını verdiğimiz bir Rust alt kümesi oluşturduk. Önceki çalışmamızda, RAR kaynağını basitçe RAC'ye aktardığımız bir RAR araç zincirinin ilk uygulamasını tanımladık. Bunu yaparak, minimum zaman ve emek yatırımıyla bir dizi mevcut donanım/yazılım eş güvence aracından yararlanıyoruz. Bu makalede, RAR Rust alt kümesini tanımlıyoruz, geliştirilmiş prototip RAR araç zincirimizi tanımlıyoruz ve ACL2 teorem kanıtlayıcısı kullanılarak gerçekleştirilen işlevsel doğruluğun tam kanıtlarıyla, RAR'da Dans Eden Bağlantılar optimizasyonunu kullanan dairesel çift bağlantılı liste veri yapısının tasarımını ve doğrulamasını ayrıntılı olarak açıklıyoruz.

1 Giriş

Kesin örtü problemi [17], en basit haliyle, ikili elemanlara sahip n × m matris için, tüm sütun toplamları tam olarak bir olacak şekilde matrisin satırlarının tüm alt kümelerini bulmaya çalışır. Bu temel kavram doğal olarak bazı sayısal aralıklarda olan matris elemanlarına kadar uzanır; aslında, popüler bulmaca oyunu Sudoku, 1 ila 9 aralığında eleman değerlerine sahip 9 × 9 matris için genişletilmiş kesin örtü problemidir.


Tam örtü problemi NP-tamdır, ancak bilgisayar bilimcileri tam örtüleri bulmak için yinelemeli, belirsiz geri izleme algoritmaları tasarladılar. Bu tür prosedürlerden biri, [17]'de açıklanan Knuth'un Algoritması X'tir. Bu algoritmada, matrisin elemanları dairesel çift bağlantılı listeler aracılığıyla bağlanır ve algoritma ilerledikçe, geri izleme vb. yapılarak tek tek elemanlar kaldırılır veya geri yüklenir. Listeden/listeye bu kaldırma ve geri yüklemeler oldukça yaygın olduğundan, bu işlemleri verimli hale getirmek övgüye değer bir hedeftir. Knuth'un "Dans Eden Bağlantılar"ı tam burada devreye girer ve Knuth'un DLX (algoritma X'e uygulanan Dans Eden Bağlantılar) adını verdiği tam örtüleri bulmak için optimize edilmiş bir algoritma ile sonuçlanır.


2 Dans Bağlantısı

Dancing Links'in ardındaki kavram oldukça basittir: Bir listenin belirli bir Y öğesi tam bir örtü algoritmasında kaldırıldığında, bu aynı öğenin daha sonra geri yüklenmesi çok olasıdır. Bu nedenle, daha ziyade



Şekil 1: Dans Eden Bağlantılar eylem halinde. (a) Kaldırma işleminden önce dairesel çift bağlantılı listenin bir bölümü; (b) Y elemanı üzerindeki kaldırma işleminden sonra; (c) Y elemanı için geri yükleme işleminden sonra.

Şekil 1: Dans Eden Bağlantılar eylem halinde. (a) Kaldırma işleminden önce dairesel çift bağlantılı listenin bir bölümü; (b) Y elemanı üzerindeki kaldırma işleminden sonra; (c) Y elemanı için geri yükleme işleminden sonra.



"Önceki" ve "sonraki" bağlantıları Y öğesiyle ilişkilendirilmiş olarak "sıfırlamaktan" daha iyi bir programlama hijyeninin normalde dikte edeceği gibi, Dans Eden Bağlantılar'da programcı kaldırılan öğe için bağlantı değerlerini yerinde bırakır. Dans Eden Bağlantılar kaldırma operatörü böylece Y öğesini listeden siler, önceki öğe X'in "sonraki" öğesini takip eden öğe Z'ye ayarlar ve Z'nin "önceki" öğesini X'e bir bağlantıya ayarlar, ancak kaldırılan öğe Y'nin "sonraki" ve "önceki" bağlantılarına dokunmaz. Daha sonra, Y'nin geri yüklenmesi gerekirse, basit bir geri yükleme operatörü kullanılarak listeye geri bağlanır. Knuth'un sözleriyle, DLX algoritması ilerledikçe liste bağlantıları izlenirse, bağlantılar "dans ediyor" gibi görünür, dolayısıyla adı budur. Knuth'un Dans Eden Bağlantılar işlevselliği Şekil 1'de özetlenmiştir.



Comment on this Story
L O A D I N G
. . . comments & more!

About Author

Knuth HackerNoon profile picture
Knuth@knuth
Knuth's mastery weaves theory and practice, a tale of computation, in the realm of computer science.

ETİKETLERİ ASIN

BU YAZI...

Read on Terminal Reader
Read this story in a terminal
 Terminal
Read this story w/o Javascript
Read this story w/o Javascript
 Lite
Also published here
X REMOVE AD