Problema de satisfacibilidad para fórmulas booleanas
La versión actual de la página aún no ha sido revisada por colaboradores experimentados y puede diferir significativamente de la versión revisada el 15 de junio de 2021; las comprobaciones requieren 3 ediciones .El problema de satisfacibilidad de fórmulas booleanas ( SAT , vyp ) es un problema algorítmico importante para la teoría de la complejidad computacional .
Una instancia de tarea es una fórmula booleana que consta solo de nombres de variables, paréntesis y operaciones ( AND ), ( OR ) y ( HE ). El problema es: ¿es posible asignar valores falsos y verdaderos a todas las variables que aparecen en la fórmula para que la fórmula se vuelva verdadera?
Según el teorema de Cook , probado por Stephen Cook en 1971, el problema SAT para fórmulas booleanas escritas en forma normal conjuntiva es NP-completo . El requisito de escribir en forma conjuntiva es esencial, ya que, por ejemplo, el problema del SAT para fórmulas presentadas en forma normal disyuntiva se resuelve trivialmente en tiempo lineal dependiendo del tamaño del registro de la fórmula (para que la fórmula sea satisfactoria, solo la presencia se requiere de al menos una conjunción que no contenga simultáneamente una negación para alguna variable ).
Redacción precisa
Para formular con precisión el problema de reconocimiento , se fija un alfabeto finito, con la ayuda del cual se especifican las instancias de lenguaje. Hopcroft , Motwani y Ullman en su libro Introducción a la teoría de autómatas , lenguajes y computación sugieren usar el siguiente alfabeto : .
Cuando se usa este alfabeto, los paréntesis y los operadores se escriben de forma natural, y las variables reciben los siguientes nombres: , según sus números en notación binaria .
Deje que alguna fórmula booleana , escrita en la notación matemática habitual, tenga la longitud de caracteres. En ella, cada ocurrencia de cada variable fue descrita por al menos un símbolo, por lo tanto, no hay más que variables en esta fórmula. Esto significa que en la notación propuesta anteriormente, cada variable se escribirá mediante símbolos. En este caso, toda la fórmula en la nueva notación tendrá la longitud de los caracteres, es decir, la longitud de la cadena aumentará un número polinomial de veces.
Por ejemplo, la fórmula tomará la forma .
Complejidad computacional
En un artículo de 1970 de Stephen Cook , se introdujo por primera vez el término " problema NP-completo " , y el problema SAT fue el primer problema para el que se demostró esta propiedad.
En la demostración del teorema de Cook, cada problema de la clase NP se reduce explícitamente a SAT. Después de la aparición de los resultados de Cook, se demostró la completitud de NP para muchos otros problemas. En este caso, la mayoría de las veces, para probar la completitud NP de un determinado problema, se da la reducción polinomial del problema SAT al problema dado, posiblemente en varios pasos, es decir, utilizando varios problemas intermedios.
Casos especiales del problema del SAT
Casos especiales importantes e interesantes del problema del SAT son:
- el problema de la satisfacibilidad de fórmulas booleanas en forma normal conjuntiva (SATCNF o VKNF) es un problema similar, con una condición impuesta a la fórmula: debe escribirse en forma normal conjuntiva ; también NP-completo ;
- problema de satisfacibilidad para fórmulas booleanas en forma normal k-conjuntiva (k-SAT o k-SAT) - problema de satisfacibilidad, siempre que la fórmula esté escrita en forma normal k-conjuntiva ; este problema es NP-completo para . Para resolver el problema, puedes usar el algoritmo probabilístico de Schoening ;
- el problema de satisfacibilidad para fórmulas booleanas en forma normal 2-conjuntiva tiene solución polinomial, es decir, pertenece a la clase P .
Solucionadores de CDCL
Uno de los métodos más efectivos para paralelizar tareas SAT son los solucionadores de CDCL (CDCL, English conflict-driven clausule learning ), basados en variantes no cronológicas del algoritmo DPLL [1] [2] .
Véase también
Notas
- ↑ Marques-Silva JP GRASP: Un algoritmo de búsqueda para la satisfacibilidad proposicional / JP Marques-Silva, KA Sakallah // IEEE Transactions on Computers. - 1999. - vol. 48, N° 5. - Págs. 506-521.
- ↑ Semenov A. A., Zaikin O. S. Algoritmos para construir conjuntos de descomposición para la paralelización de bloques grandes de problemas SAT. Serie "Matemáticas" 2012. V. 5, No. 4. S. 79-94
Enlaces
- La página web de los Concursos internacionales del SAT
- Sat Live es un sitio general sobre el SAT.
| Problemas NP-completos | |
|---|---|
| Problema de maximización del apilamiento (packing) |
|
| teoría de grafos teoría de conjuntos | |
| Problemas algorítmicos | |
| Juegos de lógica y rompecabezas. | |