Fundamentalmente, el enfoque más común es en realidad la fuerza bruta fundamentalmente: retroceso . Usted asigna repetidamente un valor a las variables hasta que encuentra una contradicción; luego, deshace algunas tareas hasta que pueda volver a intentarlo. Finalmente, en algún momento, obtendrás una tarea satisfactoria o te quedarás sin opciones que prueben que la fórmula no es satisfactoria.
Este es exactamente el mismo enfoque que el algoritmo ingenuo y extremadamente lento que probablemente implementaría usted mismo. Y, sin embargo, sigue siendo lo que usan los solucionadores más rápidos. Aun así, logran ser mucho más rápidos en la práctica.
¿Cómo lo hacen? Bueno, parte de esto es que los buenos solucionadores SAT se implementan muy bien con todo tipo de optimizaciones de bajo nivel. Afortunadamente, no es solo esto: también hay algunas ideas algorítmicas interesantes.
- ¿Qué sucede dentro del hardware de la CPU cuando la CPU ejecuta una instrucción?
- ¿Qué es una norma de lotes en el aprendizaje automático?
- ¿Hay algún fenómeno observable en informática que no podamos explicar?
- ¿Cuáles son algunos ejemplos complejos y prácticos de los equilibrios de Nash?
- ¿Debería un curso de introducción a la universidad CS enseñar con o sin IDE?
Hay tres formas generales de mejorar un algoritmo de retroceso: ser inteligente sobre la propagación de valores, elegir el orden en el que examinar las cláusulas y saber cómo fallar temprano . Las principales ideas algorítmicas para resolver SAT rápidamente son una combinación de estas. Sin embargo, encontrar formas de mejorar cualquiera de estos aspectos es muy difícil. No solo tiene que usar un método que conduzca a una búsqueda más rápida, sino que el método también debe ser rápido para calcularse porque lo ejecutará en cada paso del algoritmo. Esto crea un problema de optimización muy delicado entre la efectividad de cualquier heurística dada y su complejidad.
Algunas de las ideas más importantes se combinan en el algoritmo DPLL. Este algoritmo es el núcleo detrás de algunos de los solucionadores de SAT más rápidos como miniSAT. DPLL mejora el enfoque de retroceso básico al aprovechar las estructuras comunes en los problemas SAT del mundo real que le permiten simplificar la fórmula y, por lo tanto, recortar el espacio de búsqueda. Las técnicas de simplificación particulares son la propagación de unidades , la eliminación literal pura y la detección de cláusulas vacías . Las versiones modernas también son particularmente inteligentes sobre el orden en que se asignan las variables; El enfoque actualmente favorecido se basa en encontrar cláusulas de conflicto .
Una cláusula de “unidad” es una con una sola variable; esto se resuelve trivialmente estableciendo esa cláusula en true. Simplificar cláusulas unitarias se llama propagación unitaria . Esto nos da una asignación que podemos usar para simplificar la fórmula.
Otra forma de simplificar una fórmula es buscar variables puras . Una variable es pura si nunca o siempre se niega. Una variable pura solo tiene un valor posible que hace que todas sus cláusulas sean verdaderas, por lo que podemos asignarla de inmediato. Esta es otra tarea que nos permite simplificar la fórmula.
Cada vez que simplificamos la fórmula, podemos encontrar nuevas variables para simplificar. Por ejemplo, la propagación de unidades a menudo conduce a una serie en cascada de propagaciones de unidades adicionales a medida que las variables se eliminan de las cláusulas. Por lo tanto, buscamos posibles simplificaciones después de cada nueva asignación.
Después de haber simplificado una fórmula dada tanto como podamos, DPLL elige una variable y le asigna un valor, lo que a su vez nos permite simplificar la fórmula. Esta es la parte de ramificación de la búsqueda, porque realmente tenemos que considerar ambas posibles asignaciones a la variable dada.
Podemos decir que cualquier asignación dada es inconsistente, lo que significa que debemos retroceder, pero buscando cláusulas vacías . Las cláusulas vacías no contienen variables; significa que nuestras suposiciones actuales nos han permitido eliminar cada variable en una cláusula. Esto, a su vez, significa que nuestra asignación no puede ser consistente, por lo que podemos rescatarnos temprano.
Una extensión moderna de DPLL implica cambiar el orden en que visitamos las cláusulas y retroceder. En particular, la idea principal es que las variables que causaron conflictos en el pasado tienen más probabilidades de causar conflictos en el futuro. Esto se puede usar para aprender cláusulas adicionales llamadas cláusulas de conflicto que incorporan directamente estos conflictos y hacen que sea más fácil que la fórmula falle antes. Esto, combinado con una forma de retroceder múltiples niveles a la vez (llamado salto hacia atrás) conduce a un algoritmo llamado Aprendizaje de cláusulas controladas por conflictos (CDCL).
Un enfoque completamente diferente es la búsqueda local estocástica . La idea básica es simple: primero, todas las variables en una fórmula son valores asignados aleatoriamente. Si esta tarea es satisfactoria, entonces hemos terminado. De lo contrario, una de las variables se voltea y el resto de las variables se reasignan aleatoriamente. Hay algunos enfoques diferentes como WalkSAT y GSAT. La diferencia entre ellos está en cómo eligen qué variable voltear.
Estos algoritmos estocásticos tienen que lidiar con los mismos problemas que otros tipos de algoritmos de búsqueda local aleatorios. El problema más común es quedarse atascado en los máximos locales: es posible que tenga una tarea que satisfaga la mayoría de las cláusulas pero que en realidad no pueda conducir a una solución sin cambios importantes. Para evitar quedar atascado de esta manera, el algoritmo tiene alguna probabilidad de elegir aleatoriamente una asignación en lugar de seguir su heursítico normal. A mayor escala, el algoritmo también puede comenzar desde el principio si no se ha encontrado una solución durante un tiempo suficientemente largo.
En este momento, para la mayoría de los propósitos, los algoritmos de retroceso son más rápidos y los solucionadores de SAT basados en DPLL y cláusulas de conflicto han estado dominando las competiciones. Sin embargo, algunos casos de uso particulares son más adecuados para el enfoque aleatorio, como la planificación y programación automatizadas.
