Problema de máxima satisfacibilidad

En la teoría de la complejidad computacional , el problema de máxima satisfacibilidad ( MAX-SAT ) es el problema de determinar el número máximo de cláusulas, de una fórmula booleana dada en forma normal conjuntiva , que pueden hacerse verdaderas mediante una asignación de valores de verdad a las variables de la formula. Es una generalización del problema booleano de satisfacibilidad , que pregunta si existe una asignación de verdad que haga verdaderas todas las cláusulas.

Ejemplo

La fórmula de la forma normal conjuntiva.

${\displaystyle (x_{0}\lor x_{1})\land (x_{0}\lor \lnot x_{1})\land (\lnot x_{0}\lor x_{1})\land (\lnot x_{0}\lor \lnot x_{1})}$

no es satisfactoria: no importa qué valores de verdad se asignen a sus dos variables, al menos una de sus cuatro cláusulas será falsa. Sin embargo, es posible asignar valores de verdad de tal manera que tres de cuatro cláusulas sean verdaderas; de hecho, toda asignación de verdad hará esto. Por tanto, si se da esta fórmula como un ejemplo del problema MAX-SAT, la solución al problema es la número tres.

Dureza

El problema MAX-SAT es OptP-completo, ^[1] y por lo tanto NP-difícil , ya que su solución conduce fácilmente a la solución del problema de satisfacibilidad booleano , que es NP-completo .

También es difícil encontrar una solución aproximada del problema que satisfaga una serie de cláusulas dentro de un ratio de aproximación garantizado de la solución óptima. Más precisamente, el problema es APX completo y, por lo tanto, no admite un esquema de aproximación en tiempo polinómico a menos que P = NP. ^{[2] [3] [4]}

MAX-SAT ponderado

De manera más general, se puede definir una versión ponderada de MAX-SAT de la siguiente manera: dada una fórmula conjuntiva en forma normal con pesos no negativos asignados a cada cláusula, encontrar valores de verdad para sus variables que maximicen el peso combinado de las cláusulas satisfechas. El problema MAX-SAT es un ejemplo de MAX-SAT ponderado donde todos los pesos son 1. ^{[5] [6] [7]}

Algoritmos de aproximación

1/2 aproximación

Asignar aleatoriamente cada variable para que sea verdadera con probabilidad 1/2 da una aproximación 2 esperada . Más precisamente, si cada cláusula tiene al menos k variables, entonces esto produce una aproximación (1 − 2 ^{− k} ). ^[8] Este algoritmo se puede desaleatorizar utilizando el método de probabilidades condicionales . ^[9]

(1-1/ e )-aproximación

MAX-SAT también se puede expresar utilizando un programa lineal entero (ILP). Fije una fórmula de forma normal conjuntiva F con variables x ₁ , x ₂ , ..., x _n , y sea C las cláusulas de F . Para cada cláusula c en C , sean S ⁺ _c y S ⁻ _c los conjuntos de variables que no se niegan en c y las que se niegan en c , respectivamente. Las variables y _x del ILP corresponderán a las variables de la fórmula F , mientras que las variables z _c corresponderán a las cláusulas. El ILP es el siguiente:

El programa anterior se puede relajar al siguiente programa lineal L :

El siguiente algoritmo que utiliza esa relajación es una aproximación esperada (1-1/ e ): ^[10]

1. Resuelva el programa lineal L y obtenga una solución O
2. Establezca la variable x como verdadera con probabilidad y _x donde y _x es el valor dado en O .

Este algoritmo también se puede desaleatorizar utilizando el método de probabilidades condicionales.

aproximación 3/4

El algoritmo de aproximación 1/2 funciona mejor cuando las cláusulas son grandes, mientras que la aproximación (1-1/ e ) funciona mejor cuando las cláusulas son pequeñas. Se pueden combinar de la siguiente manera:

1. Ejecute el algoritmo de aproximación 1/2 (desaleatorizado) para obtener una asignación de verdad X .
2. Ejecute la aproximación (desaleatorizada) (1-1/e) para obtener una asignación de verdad Y .
3. La salida entre X o Y maximiza el peso de las cláusulas satisfechas.

Esta es una aproximación de factor determinista (3/4). ^[11]

Ejemplo

sobre la fórmula

$${\displaystyle F=\underbrace {(x\lor y)} _{{\text{weight }}1}\land \underbrace {(x\lor \lnot y)} _{{\text{weight }}1}\land \underbrace {(\lnot x\lor z)} _{{\text{weight }}2+\epsilon }}$$

donde , la aproximación (1-1/ e ) establecerá cada variable en Verdadero con probabilidad 1/2 y, por lo tanto, se comportará de manera idéntica a la aproximación 1/2. Suponiendo que la asignación de x se elige primero durante la desrandomización, los algoritmos desrandomizados elegirán una solución con peso total , mientras que la solución óptima tiene peso . ^[12] ${\displaystyle \epsilon >0}$ ${\displaystyle 3+\epsilon }$ ${\displaystyle 4+\epsilon }$

Solucionadores

Durante los últimos años se han desarrollado muchos solucionadores exactos para MAX-SAT, y muchos de ellos se presentaron en la conocida conferencia sobre el problema de satisfacibilidad booleana y problemas relacionados, la Conferencia SAT. En 2006, la Conferencia SAT organizó la primera evaluación MAX-SAT que compara el rendimiento de solucionadores prácticos para MAX-SAT, como lo ha hecho en el pasado para el problema de satisfacibilidad pseudobooleano y el problema de fórmula booleana cuantificada . Debido a su dureza NP, las instancias MAX-SAT de gran tamaño en general no pueden resolverse exactamente y, a menudo, es necesario recurrir a algoritmos de aproximación y heurísticas ^[13].

Hay varios solucionadores presentados a las últimas Evaluaciones Max-SAT:

• Basado en rama y límite : clon, MaxSatz (basado en Satz ), IncMaxSatz, IUT_MaxSatz, WBO, GIDSHSat.
• Basado en satisfacción: SAT4J, QMaxSat.
• Basado en insatisfacibilidad: msuncore, WPM1, PM2.

Casos especiales

MAX-SAT es una de las extensiones de optimización del problema de satisfacibilidad booleana , que es el problema de determinar si las variables de una fórmula booleana determinada se pueden asignar de tal manera que la fórmula se evalúe como VERDADERA. Si las cláusulas se restringen a tener como máximo 2 literales, como en 2-satisfactability , obtenemos el problema MAX-2SAT . Si se restringen a un máximo de 3 literales por cláusula, como en 3-satisfability , obtenemos el problema MAX-3SAT .

Problemas relacionados

Hay muchos problemas relacionados con la satisfacibilidad de fórmulas booleanas de forma normal conjuntiva.

• Problemas de decisión :
  • 2SAT
  • 3SAT
• Problemas de optimización, donde el objetivo es maximizar el número de cláusulas satisfechas:
  • MAX-SAT, y su correspondiente versión ponderada MAX-SAT ponderado
  • MAX- k SAT, donde cada cláusula tiene exactamente k variables:
    • MAX-2SAT
    • MAX-3SAT
    • MAXEkSAT
  • El problema de máxima satisfacibilidad parcial (PMAX-SAT) solicita el número máximo de cláusulas que pueden satisfacerse mediante cualquier asignación de un subconjunto determinado de cláusulas. El resto de cláusulas deberán cumplirse.
  • El problema de satisfacibilidad suave (soft-SAT), dado un conjunto de problemas SAT, solicita el número máximo de problemas que pueden satisfacerse con cualquier tarea. ^[14]
  • El problema de la mínima satisfacibilidad.
• El problema MAX-SAT se puede extender al caso donde las variables del problema de satisfacción de restricciones pertenecen al conjunto de reales. El problema consiste en encontrar el q más pequeño tal que la intersección relajada de las restricciones q no esté vacía. ^[15]

Ver también

• Problema de satisfacibilidad booleana
• Satisfacción de restricciones
• Teorías del módulo de satisfacción

enlaces externos

• http://www.satisfiability.org/
• https://web.archive.org/web/20060324162911/http://www.iiia.csic.es/~maxsat06/
• http://www.maxsat.udl.cat
• Puntos de referencia ponderados Max-2-SAT con soluciones óptimas ocultas
• Notas de la conferencia sobre la aproximación MAX-SAT

Referencias

1. M. Krentel (1988). "La complejidad de los problemas de optimización". Revista de Ciencias de la Computación y de Sistemas . 36 (3): 490–509. doi :10.1016/0022-0000(88)90039-6. hdl : 1813/6559 .
2. Mark Krentel. La complejidad de los problemas de optimización. Proc. de STOC '86. 1986.
3. Cristos Papadimitriou. Complejidad computacional. Addison-Wesley, 1994.
4. Cohen, Cooper, Jeavons. Una caracterización completa de la complejidad para problemas de optimización de restricciones booleanas. CP 2004.
5. Vazirani 2001, pag. 131.
6. Borchers, Brian; Furman, Judith (1 de diciembre de 1998). "Un algoritmo exacto de dos fases para problemas MAX-SAT y MAX-SAT ponderado". Revista de optimización combinatoria . 2 (4): 299–306. doi :10.1023/A:1009725216438. ISSN  1382-6905. S2CID  6736614.
7. Du, Dingzhu; Gu, junio; Pardalos, Panos M. (1 de enero de 1997). Problema de satisfacción: teoría y aplicaciones: taller DIMACS, 11 al 13 de marzo de 1996. American Mathematical Soc. pag. 393.ISBN​ 9780821870808.
8. Vazirani 2001, Lema 16.2.
9. Vazirani 2001, sección 16.2.
10. Vazirani 2001, pag. 136.
11. Vazirani 2001, Teorema 16.9.
12. Vazirani 2001, ejemplo 16.11.
13. Battiti, Roberto; Protasi, Marco (1998). "Algoritmos y heurísticas aproximadas para MAX-SAT". Manual de optimización combinatoria . págs. 77-148. doi :10.1007/978-1-4613-0303-9_2. ISBN 978-1-4613-7987-4.
14. Josep Argelich y Felip Manyà. Solucionadores exactos de Max-SAT para problemas demasiado restringidos. En Journal of Heuristics 12(4) págs. 375-392. Springer, 2006.
15. Jaulín, L.; Walter, E. (2002). "Estimación minimax no lineal robusta garantizada" (PDF) . Transacciones IEEE sobre control automático . 47 (11): 1857–1864. doi :10.1109/TAC.2002.804479.

• Vazirani, Vijay V. (2001), Algoritmos de aproximación (PDF) , Springer-Verlag, ISBN 978-3-540-65367-7