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

に Knuth3m2025/01/21

長すぎる; 読むには

この研究では、ACL2による形式検証を伴うKnuthのDancing Links最適化のRust実装を調査し、正確なカバー問題に対する効率的で安全なソリューションを目指しています。

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

著者：

（１）デビッド・S・ハーディン、シーダーラピッズ、アイオワ州、米国（[email protected]）。

リンク一覧

1 はじめに

2 ダンスリンク

3 Rustプログラミング言語

4 RAC: 大規模なハードウェア/ソフトウェアの共同保証

5 Rust と RAR

5.1 制限付きアルゴリズム Rust

6 Rust のダンスリンクと 6.1 定義

「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 にまとめられています。