Hispanopedia Wiki
Articulo de referencia

Problema de máxima satisfacibilidad

En la teoría de la complejidad computacional , el problema de máxima satisfacibilidad ( MAX-SAT ) consiste en determinar el número máximo de cláusulas de una fórmula booleana da...

Hispanopedia WikiContenido en espanolLectura gratuita

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

Ejemplo

La fórmula de la forma normal conjuntiva

(incógnita0∨incógnita1)∧(incógnita0∨¬incógnita1)∧(¬incógnita0∨incógnita1)∧(¬incógnita0∨¬incógnita1){\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})}

La fórmula no es satisfacible: independientemente de los valores de verdad que 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 las cuatro cláusulas sean verdaderas; de hecho, cualquier asignación de valores de verdad lo logrará. Por lo tanto, si esta fórmula se presenta como un ejemplo del problema MAX-SAT, la solución es el número tres.

Dureza

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

También es difícil encontrar una solución aproximada del problema que satisfaga una serie de condiciones dentro de un coeficiente de aproximación garantizado respecto 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 polinomial a menos que P = NP. [ 2 ] [ 3 ] [ 4 ]

MAX-SAT ponderado

De forma más general, se puede definir una versión ponderada de MAX-SAT de la siguiente manera: dada una fórmula de forma normal conjuntiva 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 una instancia de MAX-SAT ponderado donde todos los pesos son 1. [ 5 ] [ 6 ] [ 7 ]

Algoritmos de aproximación

1/2-aproximación

Asignar aleatoriamente a cada variable la condición de verdadera con una probabilidad de 1/2 da como resultado una aproximación esperada de 2. Más precisamente, si cada cláusula tiene al menos k variables, entonces se obtiene una aproximación de (1 − 2 − k ). [ 8 ] Este algoritmo puede desaleatorizarse utilizando el método de probabilidades condicionales . [ 9 ]

(1-1/ e )-aproximación

MAX-SAT can also be expressed using an integer linear program (ILP). Fix a conjunctive normal form formula F with variables x1, x2, ..., xn, and let C denote the clauses of F. For each clause c in C, let S+c and S−c denote the sets of variables which are not negated in c, and those that are negated in c, respectively. The variables yx of the ILP will correspond to the variables of the formula F, whereas the variables zc will correspond to the clauses. The ILP is as follows:

The above program can be relaxed to the following linear program L:

The following algorithm using that relaxation is an expected (1-1/e)-approximation:[10]

  1. Solve the linear program L and obtain a solution O
  2. Set variable x to be true with probability yx where yx is the value given in O.

This algorithm can also be derandomized using the method of conditional probabilities.

3/4-approximation

The 1/2-approximation algorithm does better when clauses are large whereas the (1-1/e)-approximation does better when clauses are small. They can be combined as follows:

  1. Run the (derandomized) 1/2-approximation algorithm to get a truth assignment X.
  2. Run the (derandomized) (1-1/e)-approximation to get a truth assignment Y.
  3. Output whichever of X or Y maximizes the weight of the satisfied clauses.

This is a deterministic factor (3/4)-approximation.[11]

Example

On the formula

F=(x∨y)⏟weight 1∧(x∨¬y)⏟weight 1∧(¬x∨z)⏟weight 2+ϵ{\displaystyle F=\underbrace {(x\lor y)} _{{\text{peso }}1}\land \underbrace {(x\lor \lnot y)} _{{\text{peso }}1}\land \underbrace {(\lnot x\lor z)} _{{\text{peso }}2+\epsilon }}

where ϵ>0{\displaystyle \epsilon >0}, the (1-1/e)-approximation will set each variable to True with probability 1/2, and so will behave identically to the 1/2-approximation. Assuming that the assignment of x is chosen first during derandomization, the derandomized algorithms will pick a solution with total weight 3+ϵ{\displaystyle 3+\epsilon }, mientras que la solución óptima tiene peso4+ϵ{\displaystyle 4+\epsilon }. [ 12 ]

Lo último

El algoritmo de última generación se debe a Avidor, Berkovitch y Zwick, [ 13 ] [ 14 ] y su razón de aproximación es 0,7968. También proporcionan otro algoritmo cuya razón de aproximación se conjetura que es 0,8353.

Solucionadores

En los últimos años se han desarrollado muchos solucionadores exactos para MAX-SAT, y muchos de ellos se presentaron en la reconocida conferencia sobre el problema de satisfacibilidad booleana y problemas relacionados, la Conferencia SAT. En 2006, la Conferencia SAT organizó la primera evaluación de MAX-SAT, comparando el rendimiento de solucionadores prácticos para MAX-SAT, como ya lo había hecho anteriormente para el problema de satisfacibilidad pseudobooleana y el problema de la fórmula booleana cuantificada . Debido a su NP-dificultad, las instancias de MAX-SAT de gran tamaño generalmente no se pueden resolver de forma exacta, y a menudo es necesario recurrir a algoritmos de aproximación y heurísticas [ 15 ].

Se han presentado varios solucionadores a las últimas evaluaciones de Max-SAT:

  • Basado en ramificación y acotación : Clone, MaxSatz (basado en Satz ), IncMaxSatz, IUT_MaxSatz, WBO, GIDSHSat.
  • Basado en la satisfacibilidad: SAT4J, QMaxSat.
  • Basado en la insatisfacción: msuncore, WPM1, PM2.

Casos especiales

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

Existen muchos problemas relacionados con la satisfacibilidad de las fórmulas booleanas en forma normal conjuntiva.

  • Problemas de decisión :
  • Problemas de optimización, cuyo objetivo es maximizar el número de cláusulas satisfechas:
    • MAX-SAT y la versión ponderada correspondiente, Max-SAT ponderada.
    • MAX- k SAT, donde cada cláusula tiene exactamente k variables:
    • El problema de satisfacibilidad máxima parcial (PMAX-SAT) busca el número máximo de cláusulas que pueden satisfacerse mediante cualquier asignación de un subconjunto dado de cláusulas. El resto de las cláusulas deben satisfacerse.
    • El problema de satisfacibilidad suave (soft-SAT), dado un conjunto de problemas SAT, pide el número máximo de esos problemas que pueden ser satisfechos por cualquier asignación. [ 16 ]
    • El problema de la satisfacibilidad mínima.
  • El problema MAX-SAT puede extenderse al caso en que las variables del problema de satisfacción de restricciones pertenecen al conjunto de los números reales. El problema consiste en encontrar el q más pequeño tal que la intersección q - relajada de las restricciones no sea vacía. [ 17 ]

Véase también

  • 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
  • Apuntes de clase sobre la aproximación MAX-SAT

Referencias

  1. ↑ M. Krentel (1988). "La complejidad de los problemas de optimización". Journal of Computer and System Sciences . 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 . Actas de STOC '86. 1986.
  3. ↑ Christos Papadimitriou. Complejidad computacional. Addison-Wesley, 1994.
  4. ↑ Cohen, Cooper, Jeavons. Una caracterización completa de la complejidad para problemas de optimización con restricciones booleanas . CP 2004.
  5. ↑ Vazirani 2001 , pág. 131.
  6. ↑ Borchers, Brian; Furman, Judith (1998-12-01). "Un algoritmo exacto de dos fases para problemas MAX-SAT y MAX-SAT ponderados". Journal of Combinatorial Optimization . 2 (4): 299– 306. doi : 10.1023/A:1009725216438 . ISSN 1382-6905 . S2CID 6736614 .  
  7. ↑ Du, Dingzhu; Gu, Jun; Pardalos, Panos M. (1997-01-01). Problema de satisfacibilidad: teoría y aplicaciones : Taller DIMACS, 11-13 de marzo de 1996. American Mathematical Soc. p. 393. ISBN   9780821870808.
  8. ↑ Vazirani 2001 , Lema 16.2.
  9. ↑ Vazirani 2001 , Sección 16.2.
  10. ↑ Vazirani 2001 , pág. 136.
  11. ↑ Vazirani 2001 , Teorema 16.9.
  12. ↑ Vazirani 2001 , Ejemplo 16.11.
  13. ↑ Avidor, Adi; Berkovitch, Ido; Zwick, Uri (2006). «Algoritmos de aproximación mejorados para MAX NAE-SAT y MAX SAT». Algoritmos de aproximación y en línea . Vol. 3879. Berlín, Heidelberg: Springer Berlin Heidelberg. pp. 27–40 . doi : 10.1007/11671411_3 . ISBN   978-3-540-32207-8.
  14. ↑Makarychev, Konstantin; Makarychev, Yury (2017). "Approximation Algorithms for CSPs". Drops-Idn/V2/Document/10.4230/Dfu.vol7.15301.287: 39 pages, 753340 bytes. doi:10.4230/DFU.VOL7.15301.287. ISSN 1868-8977.
  15. ↑Battiti, Roberto; Protasi, Marco (1998). "Approximate Algorithms and Heuristics for MAX-SAT". Handbook of Combinatorial Optimization. pp. 77–148. doi:10.1007/978-1-4613-0303-9_2. ISBN 978-1-4613-7987-4.
  16. ↑Josep Argelich and Felip Manyà. Exact Max-SAT solvers for over-constrained problems. In Journal of Heuristics 12(4) pp. 375-392. Springer, 2006.
  17. ↑Jaulin, L.; Walter, E. (2002). "Guaranteed robust nonlinear minimax estimation"(PDF). IEEE Transactions on Automatic Control. 47 (11): 1857–1864. doi:10.1109/TAC.2002.804479.
Lecturas relacionadas
6 articulos
Teoría de la complejidad computacionalEn la informática teórica y las matemáticas, la teoría de la complejidad computacional se centra en la clasificación de los problemas computacional...Fórmula proposicionalFórmula proposicionalEn lógica proposicional , una fórmula proposicional es un tipo de fórmula sintáctica que está bien formada . Si se dan los valores de todas las var...Forma normal conjuntivaEn lógica booleana , una fórmula está en forma normal conjuntiva ( CNF ) o forma normal clausular si es una conjunción de una o más cláusulas , don...Problema de satisfacibilidad booleanaProblema de satisfacibilidad booleanaEn lógica y ciencias de la computación , el problema de satisfacibilidad booleano (a veces llamado problema de satisfacibilidad proposicional y abr...Dureza NPDiagrama de Euler para conjuntos de problemas P , NP , NP-completos y NP-difíciles. El lado izquierdo es válido bajo el supuesto de que P≠NP , mien...NP-completitudNP-completitudEn la teoría de la complejidad computacional , un problema es NP-completo cuando: