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 genera si la fórmula es satisfactoria , lo que significa que hay posibles valores de x e y que hacen que la fórmula sea verdadera. , o insatisfactorio, lo que significa que no existen tales valores de x e y . En este caso, la fórmula es satisfactoria cuando x es verdadera, por lo que el solucionador debería devolver "satisfactible". Desde la introducción de algoritmos para SAT en la década de 1960, los solucionadores de 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 teorema de Cook-Levin , la satisfacibilidad booleana es un problema NP-completo en general. Como resultado, sólo se conocen algoritmos con una 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 dramáticos en la capacidad de resolver automáticamente instancias de problemas que involucran decenas de miles de variables y millones de restricciones. [1]
Los solucionadores del SAT a menudo comienzan convirtiendo una fórmula a su forma normal conjuntiva . A menudo se basan en algoritmos centrales 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 del SAT no solo brindan una respuesta, sino que pueden brindar más información, incluida una asignación de ejemplo (valores para x , y , etc.) en caso de que la fórmula sea satisfactoria o un conjunto mínimo de cláusulas insatisfactorias si la fórmula no es satisfactoria.
Los solucionadores SAT modernos han tenido un impacto significativo en campos que incluyen 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 exponer los solucionadores SAT como restricciones en la programación lógica de restricciones .
Una fórmula booleana es cualquier expresión que se puede escribir usando 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 , la fórmula booleana se puede evaluar y da como resultado verdadero o falso. La fórmula es satisfactoria si existe una asignación (llamada asignación satisfactoria ) para la cual la fórmula se evalúa como verdadera.
El problema de satisfacibilidad booleana es el problema de decisión que pide, al ingresar una fórmula booleana, determinar si la fórmula es satisfactible o no. Este problema es NP-completo .
Un solucionador DPLL SAT emplea un procedimiento sistemático de búsqueda de retroceso para explorar el espacio (de tamaño exponencial) de asignaciones 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 (véanse las referencias a continuación) y ahora se lo conoce comúnmente como algoritmo de Davis-Putnam-Logemann-Loveland ("DPLL" o "DLL"). [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 sólo 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 necesaria ]
Los solucionadores SAT modernos (desarrollados en la década de 2000) vienen en dos versiones: "impulsados por conflictos" y "anticipados". Ambos enfoques descienden de DPLL. [4] Los solucionadores de conflictos basados en conflictos, como el aprendizaje de cláusulas basado en conflictos (CDCL), aumentan 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 observados" , 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 conocidas incluyen Chaff [7] y GRASP . [8]
Los solucionadores de anticipación han reforzado especialmente las reducciones (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 en el interior). [ cita necesaria ]
El MiniSAT basado en conflictos, que tuvo relativamente éxito en el concurso SAT de 2005, sólo tiene unas 600 líneas de código. Un solucionador SAT paralelo moderno es ManySAT. [9] Puede lograr aceleraciones súper lineales en clases importantes de problemas. Un ejemplo de solución anticipada es march_dl, que ganó un premio en el concurso SAT de 2007. El solucionador CP-SAT de Google, parte de OR-Tools , ganó medallas de oro en las competencias de programación de restricciones Minizinc en 2018, 2019, 2020 y 2021.
Ciertos tipos de grandes instancias aleatorias satisfactorias de SAT se pueden resolver mediante propagación de encuestas (SP). [ cita necesaria ] Particularmente en aplicaciones de verificación y diseño de hardware , la satisfacibilidad y otras propiedades lógicas de una fórmula proposicional determinada a veces se deciden basándose en una representación de la fórmula como un diagrama de decisión binaria (BDD).
Diferentes solucionadores del SAT encontrarán diferentes casos fáciles o difíciles, y algunos se destacan en demostrar la insatisfacción y otros en encontrar soluciones. Todos estos comportamientos se pueden ver en los concursos de resolución del SAT. [10]
Los solucionadores SAT paralelos se dividen en tres categorías: cartera, divide y vencerás y algoritmos de búsqueda local paralelos. 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 los algoritmos de búsqueda local.
El Concurso Internacional SAT Solver tiene una pista paralela que refleja los avances recientes en la resolución paralela de SAT. En 2016, [11] 2017 [12] y 2018, [13] los puntos de referencia se ejecutaron en un sistema de memoria compartida con 24 núcleos de procesamiento , por lo que los solucionadores destinados a memoria distribuida o procesadores de muchos núcleos podrían haberse quedado cortos.
En general, no existe ningún solucionador SAT que funcione mejor que todos los demás solucionadores en todos los problemas SAT. Un algoritmo puede funcionar bien en casos problemáticos con los que otros luchan, pero funcionará peor en otros casos. Además, dada una instancia SAT, no existe una forma confiable de predecir qué algoritmo resolverá esta instancia particularmente rápido. Estas limitaciones motivan el enfoque de cartera paralela. Una cartera es un conjunto de diferentes algoritmos o diferentes configuraciones de un mismo algoritmo. Todos los solucionadores de una cartera paralela se ejecutan en diferentes procesadores para resolver el mismo problema. Si un solucionador termina, el solucionador de cartera informa que el problema es satisfactorio o insatisfactorio según ese solucionador. Todos los demás solucionadores finalizan. Diversificar las carteras al incluir una variedad de solucionadores, cada uno con un buen desempeño 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 los portafolios paralelos 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 el simple hecho de ejecutar una cartera de los mejores solucionadores en paralelo convierte a un solucionador paralelo competitivo. Un ejemplo de este tipo de solucionador es PPfolio. [16] [17] Fue diseñado para encontrar un límite inferior para el rendimiento que debería poder ofrecer un solucionador SAT paralelo. 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 paralelo para grandes grupos de nodos informáticos. Utiliza instancias configuradas de manera diferente del mismo solucionador secuencial en su núcleo. Particularmente para instancias SAT difíciles, HordeSat puede producir aceleraciones lineales y, por lo tanto, reducir significativamente el tiempo de ejecución.
En los últimos años, los solucionadores SAT de cartera paralela han dominado la pista paralela de los Concursos Internacionales de Solver SAT. Ejemplos notables de estos solucionadores incluyen Plingeling y Painless-mcomsps. [19]
A diferencia de los portafolios paralelos, el divide y vencerás paralelo intenta dividir el espacio de búsqueda entre los elementos de procesamiento. Los algoritmos de divide y vencerás, como el DPLL 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 unitaria, después de una división, los problemas parciales pueden diferir significativamente en complejidad. Por lo tanto, el algoritmo DPLL normalmente no procesa cada parte del espacio de búsqueda en la misma cantidad de tiempo, lo que genera un difícil problema de equilibrio de carga . [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 de cubo y conquista. [20] Sugiere resolver en dos fases. En la fase del "cubo", el problema se divide en muchos miles, hasta millones, de secciones. Esto lo hace un solucionador anticipado, 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 resolverse de forma independiente y simultánea mediante solucionadores de conflictos. Como la disyunción de estas fórmulas es equivalente a la fórmula original, se informa que el problema es satisfactoria si una de las fórmulas es satisfactoria. El solucionador anticipado 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 de conflictos. Además, los solucionadores anticipados 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 se eligen mediante la heurística de decisión. La heurística de dirección decide qué asignación de variable (verdadera o falsa) explorar primero. En casos 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 de conflictos secuencial. Preferiblemente los cubos son igualmente complejos de resolver. [20]
Treengeling es un ejemplo de solucionador paralelo que aplica el paradigma Cube-and-Conquer. Desde su introducción en 2012, ha tenido múltiples éxitos en el Concurso Internacional SAT Solver. Cube-and-Conquer se utilizó para resolver el problema de los triples pitagóricos booleanos . [22]
Cube-and-Conquer es una modificación o una 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 resolución de los problemas parciales) se realizaron utilizando DPLL.
Una estrategia hacia un algoritmo de búsqueda local paralelo para la resolución de SAT es probar múltiples cambios de variables simultáneamente en diferentes unidades de procesamiento. [24] Otra es aplicar el enfoque de cartera mencionado anteriormente; sin embargo, compartir cláusulas no es posible ya que los solucionadores de búsqueda locales 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ástica . Un ejemplo es WalkSAT . Los métodos estocásticos intentan encontrar una interpretación satisfactoria pero no pueden deducir que una instancia SAT sea insatisfactoria, 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 limitado . 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 3-SAT. Este último es actualmente el algoritmo más rápido conocido para k-SAT en todos los valores de k. En un 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 mediante 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 ejecutan en FPGA . [29] [30] En 2016, Marijn Heule , Oliver Kullmann y Victor Marek resolvieron el problema de los triples pitagóricos booleanos 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 que 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 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 la imposibilidad de encontrar soluciones de torneos a prueba de estrategias . Otros autores utilizaron esta tecnología para demostrar nuevas imposibilidades sobre la paradoja de la no presentación , la monotonicidad 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 estratégica, eficiente y justa para la elección social fraccionada . [39]
los solucionadores SAT modernos a menudo pueden manejar problemas con millones de restricciones y cientos de miles de variables.
