著者：  （１）デビッド・S・ハーディン、シーダーラピッズ、アイオワ州、米国（david.s.hardin@gmail.com）。 リンク一覧 1 はじめに 2 ダンスリンク 3 Rustプログラミング言語 4 RAC: 大規模なハードウェア/ソフトウェアの共同保証 5 Rust と RAR   5.1 制限付きアルゴリズム Rust   6 Rust のダンスリンクと 6.1 定義 6.2 ACL2への翻訳 6.3 ダンシングリンク定理 7 関連研究 8 結論 9 謝辞と参考文献 「Dancing Links」は、リスト要素の高速な削除と復元を可能にする、循環的な二重リンクリストデータ構造実装の最適化を意味します。Dancing Links 最適化は、主に正確なカバーを見つけるための高速アルゴリズムで使用され、Knuth の代表作 The Art of Computer Programming の第 4B 巻で広く知られるようになりました。ここでは、Rust プログラミング言語での Dancing Links 最適化の実装と、ACL2 定理証明器を使用した形式検証について説明します。Rust は、Amazon、Google、Microsoft などの企業で、C/C++ の最新のメモリセーフな後継言語としてここ数年で大きな支持を得ており、Linux と Windows の両方のオペレーティング システム カーネルに統合されています。Rust に対する私たちの関心は、クリティカル システムへの応用を含む、ハードウェア/ソフトウェアの相互保証言語としての可能性に由来しています。私たちは、Russinoff の Restricted Algorithmic C (RAC) にヒントを得て Rust サブセットを作成し、想像力豊かに Restricted Algorithmic Rust (RAR) と名付けました。以前の研究では、RAR ソースを RAC に単純にトランスパイルする RAR ツールチェーンの初期実装について説明しました。これにより、時間と労力を最小限に抑えながら、既存のハードウェア/ソフトウェア共同保証ツールを多数活用できます。この論文では、RAR Rust サブセットについて説明し、改良されたプロトタイプ RAR ツールチェーンについて説明し、RAR の Dancing Links 最適化を採用した循環二重リンク リスト データ構造の設計と検証について詳細に説明します。機能の正しさの完全な証明は、ACL2 定理証明器を使用して達成されます。  1 はじめに 完全被覆問題[17]は、最も単純な形では、2元要素を持つn×m行列について、すべての列の合計がちょうど1になるような行列の行の部分集合をすべて見つけようとするものです。この基本的な概念は、ある数値範囲にある行列要素に自然に拡張されます。実際、人気のパズルゲームである数独は、1から9までの範囲の要素値を持つ9×9行列の拡張完全被覆問題です。 完全被覆問題は NP 完全ですが、コンピュータ科学者は完全被覆を見つけるために再帰的で非決定的なバックトラッキング アルゴリズムを考案しました。そのような手順の 1 つが、[17] で説明されている Knuth のアルゴリズム X です。このアルゴリズムでは、行列の要素は循環的な二重リンク リストを介して接続され、アルゴリズムが進むにつれて、バックトラッキングなどが行われ、個々の要素が削除または復元されます。リストからの削除やリストへの復元は非常に一般的なので、これらの操作を効率化することは称賛に値する目標です。ここで Knuth の「Dancing Links」が登場し、Knuth が DLX (アルゴリズム X に適用された Dancing Links) と呼ぶ、完全被覆を見つけるための最適化されたアルゴリズムが生まれました。  2 ダンスリンク ダンシングリンクの背後にある概念は非常に単純です。リストの特定の要素Yが正確なカバーアルゴリズムで削除されると、同じ要素が後で復元される可能性が非常に高くなります。したがって、  要素 Y に関連付けられた「前の」リンクと「次の」リンクを「ゼロにする」のではなく、Dancing Links では、プログラマは削除された要素のリンク値をそのまま残します (これは、優れたプログラミング衛生基準では通常求められます)。Dancing Links 削除演算子は、リストから要素 Y を削除し、先行する要素 X の「次の」要素を次の要素 Z に設定し、Z の「前の」要素を X へのリンクに設定しますが、削除された要素 Y の「次の」リンクと「前の」リンクには触れません。後で Y を復元する必要がある場合は、単純な復元演算子を使用してリストに Y を戻すだけです。Knuth の言葉を借りれば、DLX アルゴリズムの進行中にリスト リンクを監視すると、リンクが「踊っている」ように見えるため、この名前が付けられています。Knuth の Dancing Links 機能は、図 1 にまとめられています。 この論文は、CC BY 4.0 DEED ライセンスの下で 。 arxiv で公開されています

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

Read My Stories

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

knuth's blog

このオーディオは、ストーリーの元の言語で制作されています。

データを踊らせ、複雑な問題を素早く解決するアルゴリズム

About Author

コメント

ラベル

この記事は

Related Stories

目に見えない層: ユーザーインタビューがかけがえのない資産である理由

HackerNoon Coded: HackerNoonが最も活発に活動している上位10カ国

暗号通貨の成長: 効果的なユーザーペルソナの作成

フォーラムからフィードへ: ソーシャルメディアアルゴリズムがデジタルインタラクションを形作る仕組み

目に見えない層: ユーザーインタビューがかけがえのない資産である理由

HackerNoon Coded: HackerNoonが最も活発に活動している上位10カ国

暗号通貨の成長: 効果的なユーザーペルソナの作成

フォーラムからフィードへ: ソーシャルメディアアルゴリズムがデジタルインタラクションを形作る仕組み

Light-Mode

Classic

Newspaper

Dark-Mode

Neon Noir

Minty

HN StartUps