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

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

"Ö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.