Der Algorithmus, der Daten zum Tanzen bringt – und komplexe Probleme schnell löst

Linktabelle

1 Einleitung

2 Tanzende Links

3 Die Programmiersprache Rust

4 RAC: Hardware-/Software-Co-Assurance im großen Maßstab

5 Rust und RAR

5.1 Eingeschränktes algorithmisches Rust

6 Tanzende Links in Rust und 6.1 Definitionen

6.2 Übersetzung nach ACL2

6.3 Tanzende Verbindungssätze

7 Verwandte Arbeiten

8 Fazit

9 Danksagungen und Referenzen

„Dancing Links“ bezeichnet eine Optimierung für eine Implementierung einer zirkulären, doppelt verknüpften Listendatenstruktur, die eine schnelle Entfernung und Wiederherstellung von Listenelementen ermöglicht. Die Dancing Links-Optimierung wird hauptsächlich in schnellen Algorithmen zum Finden exakter Cover verwendet und wurde von Knuth in Band 4B seiner wegweisenden Reihe The Art of Computer Programming populär gemacht. Wir beschreiben eine Implementierung der Dancing Links-Optimierung in der Programmiersprache Rust sowie ihre formale Verifizierung mithilfe des ACL2-Theorembeweisers. Rust hat in den letzten Jahren bei Unternehmen wie Amazon, Google und Microsoft als moderner, speichersicherer Nachfolger von C/C++ erhebliche Anerkennung gefunden und wird sowohl in die Betriebssystemkernel von Linux als auch von Windows integriert. Unser Interesse an Rust rührt von seinem Potenzial als Hardware-/Software-Co-Assurance-Sprache mit Anwendung auf kritische Systeme her. Wir haben eine Rust-Untermenge entwickelt, die von Russinoffs Restricted Algorithmic C (RAC) inspiriert ist und die wir fantasievoll Restricted Algorithmic Rust oder RAR genannt haben. In früheren Arbeiten haben wir unsere erste Implementierung einer RAR-Toolchain beschrieben, bei der wir die RAR-Quelle einfach in RAC transpilieren. Auf diese Weise nutzen wir eine Reihe vorhandener Hardware-/Software-Co-Assurance-Tools mit minimalem Zeit- und Arbeitsaufwand. In diesem Artikel beschreiben wir die RAR Rust-Teilmenge, beschreiben unsere verbesserte Prototyp-RAR-Toolchain und erläutern detailliert das Design und die Überprüfung einer kreisförmigen doppelt verknüpften Listendatenstruktur unter Verwendung der Dancing Links-Optimierung in RAR, wobei vollständige Beweise für die funktionale Korrektheit mithilfe des ACL2-Theorembeweisers erbracht werden.

1 Einleitung

Das exakte Überdeckungsproblem [17] versucht in seiner einfachsten Form, für eine n × m-Matrix mit binären Elementen alle Teilmengen der Zeilen der Matrix so zu finden, dass alle Spaltensummen genau eins ergeben. Dieses grundlegende Konzept lässt sich natürlich auch auf Matrixelemente erweitern, die in einem bestimmten Zahlenbereich liegen; so ist beispielsweise das beliebte Puzzlespiel Sudoku ein erweitertes exaktes Überdeckungsproblem für eine 9 × 9-Matrix mit Elementwerten im Bereich von 1 bis einschließlich 9.

Das Problem der exakten Überdeckung ist NP-vollständig, aber Informatiker haben rekursive, nichtdeterministische Backtracking-Algorithmen entwickelt, um exakte Überdeckungen zu finden. Ein solches Verfahren ist Knuths Algorithmus X, der in [17] beschrieben wird. In diesem Algorithmus sind die Elemente der Matrix über zirkuläre, doppelt verknüpfte Listen verbunden, und einzelne Elemente werden entfernt oder wiederhergestellt, während der Algorithmus fortschreitet, Backtracking durchläuft usw. Da diese Entfernungen und Wiederherstellungen aus/in die Liste recht häufig sind, ist es ein lobenswertes Ziel, diese Operationen effizient zu gestalten. Hier kommen Knuths „Dancing Links“ ins Spiel, die zu einem optimierten Algorithmus zum Finden exakter Überdeckungen führen, den Knuth DLX (Dancing Links applied to algorithm X) nennt.

2 Tanzende Links

Das Konzept hinter Dancing Links ist ganz einfach: Wenn ein bestimmtes Element Y einer Liste in einem Exact-Cover-Algorithmus entfernt wird, ist es sehr wahrscheinlich, dass dasselbe Element später wiederhergestellt wird.

als die mit Element Y verbundenen „vorherigen“ und „nächsten“ Links auf „Null“ zu setzen, wie es eine gute Programmierhygiene normalerweise vorschreiben würde, lässt der Programmierer bei Dancing Links die Linkwerte für das entfernte Element bestehen. Der Remove-Operator von Dancing Links löscht also Element Y aus der Liste, setzt das „nächste“ Element des vorhergehenden Elements X auf das folgende Element Z und setzt das „vorherige“ Element von Z auf einen Link zu X, berührt aber nicht die „nächsten“ und „vorherigen“ Links des entfernten Elements Y. Wenn Y später wiederhergestellt werden muss, wird es mit einem einfachen Restore-Operator einfach wieder in die Liste eingehängt. Um es mit Knuths Worten auszudrücken: Wenn man die Listenlinks überwacht, während der DLX-Algorithmus fortschreitet, scheinen die Links zu „tanzen“, daher der Name. Knuths Dancing Links-Funktionalität ist in Abb. 1 zusammengefasst.