El algoritmo que hace bailar a los datos y resuelve problemas complejos rápidamente

Tabla de enlaces

1 Introducción

2 enlaces de baile

3 El lenguaje de programación Rust

4 RAC: Coaseguramiento de hardware y software a escala

5. Óxido y RAR

5.1 Algorítmico restringido de Rust

6 enlaces de baile en Rust y 6.1 definiciones

6.2 Traducción a ACL2

6.3 Teoremas de enlaces danzantes

7 Trabajos relacionados

8 Conclusión

9 Agradecimientos y referencias

“Dancing Links” connota una optimización para una implementación de estructura de datos de lista doblemente enlazada circular que permite la eliminación y restauración rápida de elementos de la lista. La optimización Dancing Links se utiliza principalmente en algoritmos rápidos para encontrar coberturas exactas, y ha sido popularizada por Knuth en el Volumen 4B de su serie seminal The Art of Computer Programming. Describimos una implementación de la optimización Dancing Links en el lenguaje de programación Rust, así como su verificación formal utilizando el demostrador de teoremas ACL2. Rust ha obtenido un respaldo significativo en los últimos años como un sucesor moderno y seguro para la memoria de C/C++ en empresas como Amazon, Google y Microsoft, y se está integrando en los núcleos de los sistemas operativos Linux y Windows. Nuestro interés en Rust surge de su potencial como lenguaje de coaseguramiento de hardware/software, con aplicación a sistemas críticos. Hemos creado un subconjunto de Rust, inspirado en el C algorítmico restringido (RAC) de Russinoff, al que hemos llamado imaginativamente Rust algorítmico restringido o RAR. En un trabajo anterior, describimos nuestra implementación inicial de una cadena de herramientas RAR, en la que simplemente transpilamos el código fuente RAR en RAC. Al hacerlo, aprovechamos una serie de herramientas de co-aseguramiento de hardware/software existentes con una inversión mínima de tiempo y esfuerzo. En este artículo, describimos el subconjunto Rust de RAR, describimos nuestro prototipo mejorado de cadena de herramientas RAR y detallamos el diseño y la verificación de una estructura de datos de lista doblemente enlazada circular que emplea la optimización Dancing Links en RAR, con pruebas completas de corrección funcional logradas utilizando el demostrador de teoremas ACL2.

1 Introducción

El problema de cobertura exacta [17], en su forma más simple, intenta encontrar, para una matriz n × m con elementos binarios, todos los subconjuntos de las filas de la matriz de manera que todas las sumas de las columnas sean exactamente uno. Esta noción básica se extiende naturalmente a los elementos de la matriz que están en un rango numérico; de hecho, el popular juego de rompecabezas Sudoku es un problema de cobertura exacta extendido para una matriz 9 × 9 con valores de elementos en el rango de 1 a 9, inclusive.

El problema de la cobertura exacta es NP-completo, pero los científicos informáticos han ideado algoritmos de retroceso recursivos y no deterministas para encontrar coberturas exactas. Uno de estos procedimientos es el algoritmo X de Knuth, descrito en [17]. En este algoritmo, los elementos de la matriz se conectan mediante listas circulares doblemente enlazadas y los elementos individuales se eliminan o restauran a medida que avanza el algoritmo, experimentando un retroceso, etc. Como estas eliminaciones y restauraciones fuera/dentro de la lista son bastante comunes, hacer que estas operaciones sean eficientes es un objetivo loable. Aquí es donde entran en juego los "Dancing Links" de Knuth, que dan como resultado un algoritmo optimizado para encontrar coberturas exactas que Knuth llama DLX (Dancing Links aplicado al algoritmo X).

2 enlaces de baile

El concepto detrás de Dancing Links es bastante simple: cuando se elimina un elemento Y dado de una lista en un algoritmo de cobertura exacta, es muy probable que ese mismo elemento se restaure más adelante. Por lo tanto, en lugar de

En lugar de poner a cero los enlaces "anterior" y "siguiente" asociados con el elemento Y, como dictaría normalmente la buena higiene de programación, en Dancing Links, el programador deja los valores de enlace en su lugar para el elemento eliminado. El operador de eliminación de Dancing Links elimina así el elemento Y de la lista, fijando el elemento "siguiente" del elemento precedente X en el siguiente elemento Z, y fijando el elemento "anterior" de Z en un enlace a X, pero sin tocar los enlaces "siguiente" y "anterior" del elemento eliminado Y. Más tarde, si es necesario restaurar Y, simplemente se vuelve a conectar a la lista utilizando un operador de restauración simple. En palabras de Knuth, si uno monitorea los enlaces de la lista a medida que avanza el algoritmo DLX, los enlaces parecen "bailar", de ahí el nombre. La funcionalidad de Dancing Links de Knuth se resume en la Fig. 1.