Forma normal conjuntiva - Conjunctive normal form

En lógica booleana , una fórmula está en forma normal conjuntiva ( CNF ) o en forma normal clausal si es una conjunción de una o más cláusulas , donde una cláusula es una disyunción de literales ; dicho de otro modo, es un producto de sumas o un AND de OR . Como forma normal canónica , es útil en la demostración automatizada de teoremas y en la teoría de circuitos .

Todas las conjunciones de literales y todas las disyunciones de literales están en CNF, ya que pueden verse como conjunciones de cláusulas de un literal y conjunciones de una cláusula única, respectivamente. Como en la forma normal disyuntiva (DNF), los únicos conectivos proposicionales que puede contener una fórmula en CNF son y , o , y no . El operador not solo se puede usar como parte de un literal, lo que significa que solo puede preceder a una variable proposicional o un símbolo de predicado .

En la demostración automatizada de teoremas, la noción " forma normal clausal " se usa a menudo en un sentido más estricto, es decir, una representación particular de una fórmula CNF como un conjunto de conjuntos de literales.

Ejemplos y no ejemplos

Todas las fórmulas siguientes en las variables y están en forma normal conjuntiva:

Para mayor claridad, las cláusulas disyuntivas están escritas entre paréntesis arriba. En forma normal disyuntiva con cláusulas conjuntivas entre paréntesis, el último caso es el mismo, pero el penúltimo es . Las constantes verdadero y falso se indican mediante la conjunción vacía y una cláusula que consta de la disyunción vacía, pero normalmente se escriben explícitamente.

Las siguientes fórmulas no están en forma conjuntiva normal:

  • , ya que un OR está anidado dentro de un NOT
  • , ya que un AND está anidado dentro de un OR

Cada fórmula se puede escribir de manera equivalente como una fórmula en forma normal conjuntiva. Los tres no ejemplos en CNF son:

Conversión a CNF

Cada fórmula proposicional se puede convertir en una fórmula equivalente que está en CNF. Esta transformación se basa en reglas sobre equivalencias lógicas : eliminación de la doble negación , leyes de De Morgan y ley distributiva .

Dado que todas las fórmulas proposicionales se pueden convertir en una fórmula equivalente en forma normal conjuntiva, las demostraciones a menudo se basan en el supuesto de que todas las fórmulas son CNF. Sin embargo, en algunos casos, esta conversión a CNF puede conducir a una explosión exponencial de la fórmula. Por ejemplo, la traducción de la siguiente fórmula que no es CNF a CNF produce una fórmula con cláusulas:

En particular, la fórmula generada es:

Esta fórmula contiene cláusulas; cada cláusula contiene una o para cada una .

Existen transformaciones en CNF que evitan un aumento exponencial de tamaño al preservar la satisfacibilidad en lugar de la equivalencia . Se garantiza que estas transformaciones solo aumentarán linealmente el tamaño de la fórmula, pero introducirán nuevas variables. Por ejemplo, la fórmula anterior se puede transformar en CNF agregando variables de la siguiente manera:

Una interpretación satisface esta fórmula solo si al menos una de las nuevas variables es verdadera. Si esta variable es , entonces ambos y también son verdaderos. Esto significa que todo modelo que satisface esta fórmula también satisface al original. Por otro lado, solo algunos de los modelos de la fórmula original satisfacen esta: dado que no se mencionan en la fórmula original, sus valores son irrelevantes para su satisfacción, lo que no es el caso en la última fórmula. Esto significa que la fórmula original y el resultado de la traducción son equisatisfactorios pero no equivalentes .

Una traducción alternativa, la transformación de Tseitin , incluye también las cláusulas . Con estas cláusulas, la fórmula implica ; a menudo se considera que esta fórmula "define" para ser un nombre .

Lógica de primer orden

En la lógica de primer orden, la forma normal conjuntiva se puede llevar más allá para producir la forma normal clausal de una fórmula lógica, que luego se puede usar para realizar una resolución de primer orden . En la demostración automatizada de teoremas basada en resolución, una fórmula CNF

, con literales, se representa comúnmente como un conjunto de conjuntos
.

Vea a continuación un ejemplo.

Complejidad computacional

Un conjunto importante de problemas en la complejidad computacional implica encontrar asignaciones a las variables de una fórmula booleana expresada en forma normal conjuntiva, de modo que la fórmula sea verdadera. El problema k -SAT es el problema de encontrar una asignación satisfactoria a una fórmula booleana expresada en CNF en la que cada disyunción contiene como máximo k variables. 3-SAT es NP-completo (como cualquier otro problema de k -SAT con k > 2) mientras que se sabe que 2-SAT tiene soluciones en tiempo polinomial . Como consecuencia, la tarea de convertir una fórmula en un DNF , preservando la satisfacibilidad, es NP-difícil ; doblemente , convertir a CNF, preservando la validez , también es NP-hard; por tanto, la conversión que conserva la equivalencia en DNF o CNF es de nuevo NP-hard.

Los problemas típicos en este caso involucran fórmulas en "3CNF": forma normal conjuntiva con no más de tres variables por conjunción. Los ejemplos de tales fórmulas que se encuentran en la práctica pueden ser muy grandes, por ejemplo, con 100.000 variables y 1.000.000 de conjunciones.

Una fórmula en CNF se puede convertir en una fórmula equisatisfactable en " k CNF" (para k ≥3) reemplazando cada conjunción con más de k variables por dos conjunciones y con Z una nueva variable, y repitiendo tantas veces como sea necesario.

Conversión de lógica de primer orden

Para convertir la lógica de primer orden a CNF:

  1. Convierta a la forma normal de negación .
    1. Eliminar implicaciones y equivalencias: reemplazar repetidamente con ; reemplazar con . Eventualmente, esto eliminará todas las apariciones de y .
    2. Mueva los NOT hacia adentro aplicando repetidamente la ley de De Morgan . Específicamente, reemplace con ; reemplazar con ; y reemplazar con ; reemplazar con ; con . Después de eso, a puede aparecer solo inmediatamente antes de un símbolo de predicado.
  2. Estandarizar variables
    1. Para oraciones como las que usan el mismo nombre de variable dos veces, cambie el nombre de una de las variables. Esto evita confusiones posteriores al descartar cuantificadores. Por ejemplo, se cambia el nombre a .
  3. Skolemize la declaración
    1. Mueva los cuantificadores hacia afuera: reemplace repetidamente con ; reemplazar con ; reemplazar con ; reemplazar con . Estos reemplazos preservan la equivalencia, ya que el paso de estandarización de variables anterior aseguró que no ocurra en . Después de estos reemplazos, un cuantificador puede ocurrir sólo en el prefijo inicial de la fórmula, pero nunca dentro de un , o .
    2. Reemplace repetidamente con , donde hay un nuevo símbolo de función -ary, una llamada " función Skolem ". Este es el único paso que conserva solo la satisfacibilidad en lugar de la equivalencia. Elimina todos los cuantificadores existenciales.
  4. Suelta todos los cuantificadores universales.
  5. Distribuya los OR hacia adentro sobre los AND: reemplace repetidamente con .

A modo de ejemplo, la fórmula que dice "Cualquiera que ama a todos los animales, a su vez es amado por alguien" se convierte en CNF (y posteriormente en forma de cláusula en la última línea) de la siguiente manera (resaltando la regla de reemplazo que se reexpresa en ):

por 1.1
por 1.1
por 1.2
por 1.2
por 1.2
por 2
por 3,1
por 3,1
por 3.2
por 4
por 5
( representación de cláusula )

De manera informal, se puede pensar en la función Skolem como ceder a la persona por quien es amado, mientras que cede al animal (si lo hay) que no ama. La tercera última línea de abajo se lee como " no ama al animal , o es amado por " .

La segunda última línea de arriba , es el CNF.

Notas

  1. ^ Peter B. Andrews, Introducción a la lógica matemática y la teoría de tipos , 2013, ISBN  9401599343 , p. 48
  2. ^ a b Inteligencia artificial: un enfoque moderno Archivado el 31 de agosto de 2017 en la Wayback Machine [1995 ...] Russell y Norvig
  3. ^ Tseitin (1968)
  4. ^ Jackson y Sheridan (2004)
  5. ^ dado que una forma de verificar la satisfacción de un CNF es convertirlo en un DNF , cuya satisfacción se puede verificar en tiempo lineal

Ver también

Referencias

enlaces externos