האלגוריתם שגורם לנתונים לרקוד - ולפתור בעיות מורכבות במהירות

טבלת קישורים

1 הקדמה

2 קישורי ריקוד

3 שפת התכנות חלודה

4 RAC: שיתוף חומרה/תוכנה בקנה מידה

5 חלודה ו-RAR

5.1 חלודה אלגוריתמית מוגבלת

6 קישורים רוקדים בחלודה והגדרות 6.1

6.2 תרגום ל-ACL2

6.3 משפטי קישורי ריקוד

7 עבודה קשורה

8 מסקנה

9 תודות והפניות

"קישורים רוקדים" מקשרת אופטימיזציה ליישום מבנה נתוני רשימה מעגלי מקושר כפול, המספק הסרה ושיחזור מהיר של רכיבי רשימה. האופטימיזציה של Dancing Links משמשת בעיקר באלגוריתמים מהירים כדי למצוא כיסויים מדויקים, וזכה לפופולריות על ידי Knuth בכרך 4B של הסדרה המכוננת שלו, The Art of Computer Programming. אנו מתארים יישום של האופטימיזציה של Dancing Links בשפת התכנות Rust, כמו גם את האימות הפורמלי שלה באמצעות מוכיח משפט ACL2. Rust זכתה לתמיכה משמעותית בשנים האחרונות כיורשת מודרנית, בטוחה בזיכרון, של C/C++ בחברות כמו אמזון, גוגל ומיקרוסופט, והיא משולבת בליבת מערכות ההפעלה לינוקס ו-Windows כאחד. העניין שלנו ב-Rust נובע מהפוטנציאל שלה כשפת אבטחת חומרה/תוכנה, עם יישום למערכות קריטיות. יצרנו תת-קבוצה של Rust, בהשראת ה-Restricted Algorithmic C (RAC) של Russinoff, שקראנו לה בדמיון Restricted Algorithmic Rust, או RAR. בעבודה קודמת, תיארנו את היישום הראשוני שלנו של שרשרת כלים RAR, שבה אנו פשוט מעבירים את מקור ה-RAR ל-RAC. על ידי כך, אנו ממנפים מספר כלי אבטחת שיתוף חומרה/תוכנה קיימים במינימום השקעה של זמן ומאמץ. במאמר זה, אנו מתארים את תת-קבוצת ה-RAR Rust, מתארים את שרשרת הכלים RAR המשופרת שלנו, ומפרטים את התכנון והאימות של מבנה נתונים עגול ברשימה מקושרת כפולה המשתמש באופטימיזציה של Dancing Links ב-RAR, עם הוכחות מלאות של נכונות תפקודית באמצעות מוכיח משפט ACL2.

1 הקדמה

בעיית הכיסוי המדויקת [17], בצורתה הפשוטה ביותר, מנסה למצוא, עבור מטריצה n × m עם אלמנטים בינאריים, את כל תת-הקבוצות של שורות המטריצה כך שכל סכומי העמודות הם אחד בדיוק. מושג בסיסי זה משתרע באופן טבעי על רכיבי מטריצה הנמצאים בטווח מספרי כלשהו; ואכן, משחק הפאזל הפופולרי סודוקו הוא בעיית כיסוי מדויקת מורחבת עבור מטריצה של 9×9 עם ערכי אלמנטים בטווח של 1 עד 9, כולל.

בעיית הכיסוי המדויקת היא NP-שלמה, אבל מדעני מחשב המציאו אלגוריתמים רקורסיביים, לא דטרמיניסטים לעקיבה לאחור כדי למצוא כיסויים מדויקים. הליך אחד כזה הוא האלגוריתם X של Knuth, המתואר ב-[17]. באלגוריתם זה, אלמנטים של המטריצה מחוברים באמצעות רשימות מעגליות מקושרות כפולות, ואלמנטים בודדים מוסרים, או משוחזרים, ככל שהאלגוריתם מתקדם, עוברים מעקב לאחור, וכו'. מכיוון שההסרות והשחזורים הללו מתוך/אל הרשימה הם די שכיחים , ביצוע פעולות אלו ליעילות היא מטרה ראויה לשבח. כאן נכנס לתמונה "קישורי הריקוד" של Knuth, וכתוצאה מכך אלגוריתם אופטימלי למציאת כיסויים מדויקים שאותם Knuth מכנה DLX (Dancing Links מיושם על אלגוריתם X).

2 קישורי ריקוד

הרעיון מאחורי Dancing Links הוא די פשוט: כאשר אלמנט Y נתון ברשימה מוסר באלגוריתם כיסוי מדויק, סביר מאוד שאותו אלמנט ישוחזר מאוחר יותר. כך, יותר נכון

מאשר "אפס" את הקישורים ה'קודמים' וה'הבאים' הקשורים לרכיב Y, כפי שהיגיינת תכנות טובה תכתיב בדרך כלל, ב-Dancing Links, המתכנת משאיר את ערכי הקישור במקום עבור האלמנט שהוסר. אופרטור ההסרה של קישורים רוקדים מוחק אלמנט Y מהרשימה, מגדיר את האלמנט 'הבא' של האלמנט הקודם X לאלמנט Z הבא, ומגדיר את האלמנט 'הקודם' של Z לקישור ל-X, אך לא נוגע ב-' קישורים next' ו-'Previous' של האלמנט Y שהוסר. מאוחר יותר, אם יש צורך לשחזר Y, הוא פשוט מחובר חזרה לרשימה באמצעות אופרטור שחזור פשוט. במילותיו של Knuth, אם עוקבים אחר קישורי הרשימה ככל שאלגוריתם DLX מתקדם, הקישורים נראים כ'רוקדים', ומכאן השם. הפונקציונליות של קישורי הריקוד של Knuth מסוכמת באיור 1.