En informática y métodos formales , un solucionador SAT es un programa informático que tiene como objetivo resolver el problema de satisfacibilidad booleano . Al ingresar una fórmula sobre variables booleanas , como "( x o y ) y ( x o no y )", un solucionador SAT muestra si la fórmula es satisfacible , lo que significa que hay posibles valores de x e y que hacen que la fórmula sea verdadera, o insatisfacible, lo que significa que no existen tales valores de x e y . En este caso, la fórmula es satisfacible cuando x es verdadera, por lo que el solucionador debe devolver "satisfacible". Desde la introducción de algoritmos para SAT en la década de 1960, los solucionadores SAT modernos se han convertido en artefactos de software complejos que involucran una gran cantidad de heurísticas y optimizaciones de programas para funcionar de manera eficiente.
Según un resultado conocido como el teorema de Cook-Levin , la satisfacibilidad booleana es un problema NP-completo en general. Como resultado, solo se conocen algoritmos con complejidad exponencial en el peor de los casos. A pesar de esto, durante la década de 2000 se desarrollaron algoritmos eficientes y escalables para SAT, que han contribuido a avances espectaculares en la capacidad de resolver automáticamente instancias de problemas que involucran decenas de miles de variables y millones de restricciones. [1]
Los solucionadores SAT suelen comenzar convirtiendo una fórmula a la forma normal conjuntiva . A menudo se basan en algoritmos básicos como el algoritmo DPLL , pero incorporan una serie de extensiones y características. La mayoría de los solucionadores SAT incluyen tiempos de espera, por lo que finalizarán en un tiempo razonable incluso si no pueden encontrar una solución con un resultado como "desconocido". A menudo, los solucionadores SAT no solo brindan una respuesta, sino que pueden brindar información adicional, incluida una asignación de ejemplo (valores para x , y , etc.) en caso de que la fórmula sea satisfacible o un conjunto mínimo de cláusulas insatisfacibles si la fórmula es insatisfacible.
Los solucionadores SAT modernos han tenido un impacto significativo en campos como la verificación de software , el análisis de programas , la resolución de restricciones , la inteligencia artificial , la automatización del diseño electrónico y la investigación de operaciones . Los solucionadores potentes están disponibles como software gratuito y de código abierto y están integrados en algunos lenguajes de programación, como la exposición de los solucionadores SAT como restricciones en la programación de lógica de restricciones .
Una fórmula booleana es cualquier expresión que se pueda escribir utilizando variables booleanas (proposicionales) x, y, z, ... y las operaciones booleanas AND, OR y NOT. Por ejemplo,
Una asignación consiste en elegir, para cada variable, una asignación VERDADERA o FALSA. Para cualquier asignación v , se puede evaluar la fórmula booleana, que se evalúa como verdadera o falsa. La fórmula es satisfacible si existe una asignación (denominada asignación satisfactoria ) para la que la fórmula se evalúa como verdadera.
El problema de satisfacibilidad booleana es un problema de decisión que pide, a partir de una fórmula booleana, determinar si la fórmula es satisfacible o no. Este problema es NP-completo .
Los solucionadores SAT generalmente se desarrollan utilizando uno de dos enfoques principales: el algoritmo Davis–Putnam–Logemann–Loveland (DPLL) y el aprendizaje de cláusulas impulsado por conflictos (CDCL).
Un solucionador SAT DPLL emplea un procedimiento sistemático de búsqueda de retroceso para explorar el espacio (de tamaño exponencial) de asignaciones de variables en busca de asignaciones satisfactorias. El procedimiento de búsqueda básico se propuso en dos artículos fundamentales a principios de la década de 1960 (consulte las referencias a continuación) y ahora se lo conoce comúnmente como el algoritmo DPLL . [2] [3] Muchos enfoques modernos para la resolución práctica de SAT se derivan del algoritmo DPLL y comparten la misma estructura. A menudo, solo mejoran la eficiencia de ciertas clases de problemas SAT, como instancias que aparecen en aplicaciones industriales o instancias generadas aleatoriamente. [4] Teóricamente, se han demostrado límites inferiores exponenciales para la familia de algoritmos DPLL. [ cita requerida ]
Los solucionadores SAT modernos (desarrollados en la década de 2000) vienen en dos versiones: "basados en conflictos" y "anticipados". Ambos enfoques descienden de DPLL. [4] Los solucionadores basados en conflictos, como el aprendizaje de cláusulas basado en conflictos (CDCL), amplían el algoritmo de búsqueda DPLL básico con un análisis de conflictos eficiente, aprendizaje de cláusulas, saltos hacia atrás , una forma de propagación de unidades de "dos literales vigilados" , ramificación adaptativa y reinicios aleatorios. Se ha demostrado empíricamente que estos "extras" de la búsqueda sistemática básica son esenciales para manejar las grandes instancias SAT que surgen en la automatización del diseño electrónico (EDA). [5] La mayoría de los solucionadores SAT de última generación se basan en el marco CDCL a partir de 2019. [6] Las implementaciones más conocidas incluyen Chaff [7] y GRASP . [8]
Los solucionadores de anticipación tienen reducciones especialmente fortalecidas (que van más allá de la propagación de cláusulas unitarias) y las heurísticas, y generalmente son más fuertes que los solucionadores impulsados por conflictos en instancias difíciles (mientras que los solucionadores impulsados por conflictos pueden ser mucho mejores en instancias grandes que en realidad tienen una instancia fácil adentro). [ cita requerida ]
El solucionador de conflictos MiniSAT, que tuvo un éxito relativo en la competencia SAT de 2005, solo tiene alrededor de 600 líneas de código. Un solucionador de SAT paralelo moderno es ManySAT. [9] Puede lograr aceleraciones superlineales en clases importantes de problemas. Un ejemplo de solucionadores de anticipación es march_dl, que ganó un premio en la competencia SAT de 2007. El solucionador CP-SAT de Google, parte de OR-Tools , ganó medallas de oro en las competencias de programación con restricciones Minizinc en 2018, 2019, 2020 y 2021.
Ciertos tipos de grandes instancias aleatorias satisfacibles de SAT se pueden resolver mediante propagación de encuesta (SP). [ cita requerida ] Particularmente en aplicaciones de diseño y verificación de hardware , la satisfacibilidad y otras propiedades lógicas de una fórmula proposicional dada a veces se deciden en función de una representación de la fórmula como un diagrama de decisión binaria (BDD).
A los distintos solucionadores del SAT les resultará fácil o difícil resolver distintos casos, y algunos se destacan en demostrar la insatisfacción y otros en encontrar soluciones. Todos estos comportamientos se pueden observar en los concursos de resolución del SAT. [10]
Los solucionadores SAT paralelos se dividen en tres categorías: algoritmos de cartera, de divide y vencerás y de búsqueda local paralela . Con carteras paralelas, se ejecutan varios solucionadores SAT diferentes al mismo tiempo. Cada uno de ellos resuelve una copia de la instancia SAT, mientras que los algoritmos de divide y vencerás dividen el problema entre los procesadores. Existen diferentes enfoques para paralelizar algoritmos de búsqueda local.
La Competencia Internacional de Resolución de Problemas SAT tiene una trayectoria paralela que refleja los avances recientes en la resolución de problemas SAT en paralelo. En 2016, [11] 2017 [12] y 2018, [13] las pruebas de referencia se ejecutaron en un sistema de memoria compartida con 24 núcleos de procesamiento , por lo que los solucionadores diseñados para memoria distribuida o procesadores de múltiples núcleos podrían no haber estado a la altura.
En general, no existe ningún solucionador de SAT que tenga un mejor rendimiento que el resto de solucionadores en todos los problemas de SAT. Un algoritmo puede tener un buen rendimiento en casos de problemas con los que otros tienen dificultades, pero tendrá un peor rendimiento en otros casos. Además, dada una instancia de SAT, no hay una forma fiable de predecir qué algoritmo resolverá esta instancia con especial rapidez. Estas limitaciones motivan el enfoque de cartera paralela. Una cartera es un conjunto de algoritmos diferentes o configuraciones diferentes del mismo algoritmo. Todos los solucionadores de una cartera paralela se ejecutan en procesadores diferentes para resolver el mismo problema. Si un solucionador finaliza, el solucionador de la cartera informa que el problema es satisfacible o insatisfacible según este solucionador. Todos los demás solucionadores finalizan. La diversificación de las carteras mediante la inclusión de una variedad de solucionadores, cada uno con un buen rendimiento en un conjunto diferente de problemas, aumenta la solidez del solucionador. [14]
Muchos solucionadores utilizan internamente un generador de números aleatorios . Diversificar sus semillas es una forma sencilla de diversificar una cartera. Otras estrategias de diversificación implican habilitar, deshabilitar o diversificar ciertas heurísticas en el solucionador secuencial. [15]
Una desventaja de las carteras paralelas es la cantidad de trabajo duplicado. Si se utiliza el aprendizaje de cláusulas en los solucionadores secuenciales, compartir cláusulas aprendidas entre solucionadores que se ejecutan en paralelo puede reducir el trabajo duplicado y aumentar el rendimiento. Sin embargo, incluso la simple ejecución de una cartera de los mejores solucionadores en paralelo hace que un solucionador paralelo sea competitivo. Un ejemplo de un solucionador de este tipo es PPfolio. [16] [17] Fue diseñado para encontrar un límite inferior para el rendimiento que un solucionador SAT paralelo debería ser capaz de ofrecer. A pesar de la gran cantidad de trabajo duplicado debido a la falta de optimizaciones, funcionó bien en una máquina de memoria compartida. HordeSat [18] es un solucionador de cartera paralela para grandes grupos de nodos informáticos. Utiliza instancias configuradas de forma diferente del mismo solucionador secuencial en su núcleo. Particularmente para las instancias SAT duras, HordeSat puede producir aceleraciones lineales y, por lo tanto, reducir significativamente el tiempo de ejecución.
En los últimos años, los solucionadores de SAT de cartera paralela han dominado la vía paralela de las Competiciones Internacionales de Solución de SAT. Entre los ejemplos notables de dichos solucionadores se incluyen Plingeling y painless-mcomsps. [19]
A diferencia de las carteras paralelas, el algoritmo de dividir y vencer en paralelo intenta dividir el espacio de búsqueda entre los elementos de procesamiento. Los algoritmos de dividir y vencer, como el algoritmo de división y vencer secuencial, ya aplican la técnica de dividir el espacio de búsqueda, por lo que su extensión hacia un algoritmo paralelo es sencilla. Sin embargo, debido a técnicas como la propagación de unidades, después de una división, los problemas parciales pueden diferir significativamente en complejidad. Por lo tanto, el algoritmo de división y vencer normalmente no procesa cada parte del espacio de búsqueda en la misma cantidad de tiempo, lo que genera un problema de equilibrio de carga desafiante . [14]
Debido al retroceso no cronológico, la paralelización del aprendizaje de cláusulas impulsadas por conflictos es más difícil. Una forma de superar esto es el paradigma Cube-and-Conquer [20] . Sugiere resolver en dos fases. En la fase "cubo", el problema se divide en muchos miles, hasta millones, de secciones. Esto se hace mediante un solucionador de anticipación, que encuentra un conjunto de configuraciones parciales llamadas "cubos". Un cubo también puede verse como una conjunción de un subconjunto de variables de la fórmula original. Junto con la fórmula, cada uno de los cubos forma una nueva fórmula. Estas fórmulas pueden ser resueltas de forma independiente y concurrente por solucionadores impulsados por conflictos. Como la disyunción de estas fórmulas es equivalente a la fórmula original, se informa que el problema es satisfacible, si una de las fórmulas es satisfacible. El solucionador de anticipación es favorable para problemas pequeños pero difíciles, [21] por lo que se utiliza para dividir gradualmente el problema en múltiples subproblemas. Estos subproblemas son más fáciles pero aún grandes, lo que es la forma ideal para un solucionador impulsado por conflictos. Además, los solucionadores de anticipación consideran el problema completo, mientras que los solucionadores impulsados por conflictos toman decisiones basadas en información que es mucho más local. Hay tres heurísticas involucradas en la fase del cubo. Las variables en los cubos son elegidas por la heurística de decisión. La heurística de dirección decide qué asignación de variable (verdadera o falsa) explorar primero. En instancias de problemas satisfacibles, es beneficioso elegir primero una rama satisfacible. La heurística de corte decide cuándo dejar de expandir un cubo y, en su lugar, reenviarlo a un solucionador secuencial impulsado por conflictos. Preferiblemente, los cubos son igualmente complejos de resolver. [20]
Treengeling es un ejemplo de un solucionador paralelo que aplica el paradigma Cube-and-Conquer. Desde su introducción en 2012, ha tenido múltiples éxitos en la Competencia Internacional de Solucionadores SAT. Cube-and-Conquer se utilizó para resolver el problema de las ternas pitagóricas booleanas . [22]
Cube-and-Conquer es una modificación o generalización del enfoque Divide-and-conquer basado en DPLL utilizado para calcular los números de Van der Waerden w(2;3,17) y w(2;3,18) en 2010 [23] donde ambas fases (división y solución de los problemas parciales) se realizaron utilizando DPLL.
Una estrategia para un algoritmo de búsqueda local paralelo para la resolución de problemas SAT es probar múltiples cambios de variable simultáneamente en diferentes unidades de procesamiento. [24] Otra es aplicar el enfoque de cartera mencionado anteriormente, sin embargo, no es posible compartir cláusulas ya que los solucionadores de búsqueda local no producen cláusulas. Alternativamente, es posible compartir las configuraciones que se producen localmente. Estas configuraciones se pueden utilizar para guiar la producción de una nueva configuración inicial cuando un solucionador local decide reiniciar su búsqueda. [25]
Los algoritmos que no forman parte de la familia DPLL incluyen algoritmos de búsqueda local estocásticos . Un ejemplo es WalkSAT . Los métodos estocásticos intentan encontrar una interpretación satisfactoria, pero no pueden deducir que una instancia SAT no es satisfacible, a diferencia de los algoritmos completos, como DPLL. [4]
Por el contrario, los algoritmos aleatorios como el algoritmo PPSZ de Paturi, Pudlak, Saks y Zane establecen las variables en un orden aleatorio de acuerdo con algunas heurísticas, por ejemplo, la resolución de ancho acotado . Si la heurística no puede encontrar la configuración correcta, la variable se asigna aleatoriamente. El algoritmo PPSZ tiene un tiempo de ejecución [ aclarar ] de para 3-SAT. Este fue el tiempo de ejecución más conocido para este problema hasta 2019, cuando Hansen, Kaplan, Zamir y Zwick publicaron una modificación de ese algoritmo con un tiempo de ejecución de para 3-SAT. Este último es actualmente el algoritmo más rápido conocido para k-SAT en todos los valores de k. En el entorno con muchas asignaciones satisfactorias, el algoritmo aleatorio de Schöning tiene un mejor límite. [26] [27] [28]
Los solucionadores SAT se han utilizado para ayudar a demostrar teoremas matemáticos a través de pruebas asistidas por computadora . En la teoría de Ramsey , se calcularon varios números de Van der Waerden previamente desconocidos con la ayuda de solucionadores SAT especializados que se ejecutaban en FPGAs . [29] [30] En 2016, Marijn Heule , Oliver Kullmann y Victor Marek resolvieron el problema de las ternas pitagóricas booleanas utilizando un solucionador SAT para demostrar que no hay forma de colorear los números enteros hasta 7825 de la manera requerida. [31] [32] Heule también calculó valores pequeños de los números de Schur utilizando solucionadores SAT. [33]
Los solucionadores SAT se utilizan en la verificación formal de hardware y software . En la verificación de modelos (en particular, la verificación de modelos acotados), los solucionadores SAT se utilizan para verificar si un sistema de estados finitos satisface una especificación de su comportamiento previsto. [34] [35]
Los solucionadores SAT son el componente central sobre el cual se construyen los solucionadores de teorías de módulo de satisfacibilidad (SMT), que se utilizan para problemas como programación de trabajos , ejecución simbólica , verificación de modelos de programas , verificación de programas basada en lógica de Hoare y otras aplicaciones. [36] Estas técnicas también están estrechamente relacionadas con la programación de restricciones y la programación lógica .
En la investigación de operaciones , los solucionadores SAT se han aplicado para resolver problemas de optimización y programación. [37]
En la teoría de la elección social , los solucionadores SAT se han utilizado para demostrar teoremas de imposibilidad. [38] Tang y Lin utilizaron solucionadores SAT para demostrar el teorema de Arrow y otros teoremas de imposibilidad clásicos. Geist y Endriss lo utilizaron para encontrar nuevas imposibilidades relacionadas con extensiones de conjuntos. Brandt y Geist utilizaron este enfoque para demostrar una imposibilidad sobre soluciones de torneo a prueba de estrategias . Otros autores utilizaron esta tecnología para demostrar nuevas imposibilidades sobre la paradoja de la no presentación , la monotonía a mitad de camino y las reglas de votación probabilísticas . Brandl, Brandt, Peters y Stricker lo utilizaron para demostrar la imposibilidad de una regla a prueba de estrategias, eficiente y justa para la elección social fraccionaria . [39]
a menudo pueden manejar problemas con millones de restricciones y cientos de miles de variables.
