Forma normal conjuntiva

Las siguientes fórmulas están en FNC:

1. ${\displaystyle \neg A\wedge (B\vee C)}$
2. ${\displaystyle (A\vee B)\wedge (\neg B\vee C\vee \neg D)\wedge (D\vee \neg E)}$
3. ${\displaystyle A\wedge B.}$

La última forma está en FNC porque puede ser vista como la conjunción de las dos cláusulas de literales ${\displaystyle A}$ y ${\displaystyle B}$. Esta fórmula es también una forma normal disyuntiva. Las siguientes fórmulas no están en FNC:

1. ${\displaystyle \neg (B\vee C)}$
2. ${\displaystyle (A\wedge B)\vee C}$
3. ${\displaystyle A\wedge (B\vee (D\wedge E)).}$

Cada fórmula puede ser el equivalente escrita como una fórmula en forma normal conjuntiva. En particular, este es el caso para los tres contraejemplos recién mencionados; que son, respectivamente, equivalentes a las siguientes tres fórmulas, que están en forma normal conjuntiva:

1. ${\displaystyle \neg B\wedge \neg C}$
2. ${\displaystyle (A\vee C)\wedge (B\vee C)}$
3. ${\displaystyle A\wedge (B\vee D)\wedge (B\vee E).}$

Cada fórmula proposicional puede convertirse en una fórmula equivalente que está en FNC. Esta transformación se basa en reglas sobre equivalencias lógicas: la doble negación, las leyes de De Morgan, y la distributividad.

Sin embargo, hay algunos casos en que dicha conversión puede producir un crecimiento exponencial del tamaño de la fórmula.

Por ejemplo, al convertir la siguiente fórmula:

${\displaystyle (X_{1}\wedge Y_{1})\vee (X_{2}\wedge Y_{2})\vee \dots \vee (X_{n}\wedge Y_{n}).}$

a FNC se obtiene una fórmula con ${\displaystyle 2^{n}}$ cláusulas:

${\displaystyle (X_{1}\vee \cdots \vee X_{n-1}\vee X_{n})\wedge (X_{1}\vee \cdots \vee X_{n-1}\vee Y_{n})\wedge \cdots \wedge (Y_{1}\vee \cdots \vee Y_{n-1}\vee Y_{n}).}$

Esta fórmula contiene ${\displaystyle 2^{n}}$ cláusulas; cada cláusula contiene o bien ${\displaystyle X_{i}}$ o ${\displaystyle Y_{i}}$ para cada ${\displaystyle i}$.

Existen transformaciones en FNC que evitan un crecimiento exponencial en el tamaño preservando la satisfacibilidad en lugar de equivalencia.[1][2] Estas transformaciones están garantizadas para aumentar solo linealmente el tamaño de la fórmula, pero introduce nuevas variables. Por ejemplo, la fórmula anterior puede ser transformada en FNC adicionando variables ${\displaystyle Z_{1},\ldots ,Z_{n}}$ como sigue:

${\displaystyle (Z_{1}\vee \cdots \vee Z_{n})\wedge (\neg Z_{1}\vee X_{1})\wedge (\neg Z_{1}\vee Y_{1})\wedge \cdots \wedge (\neg Z_{n}\vee X_{n})\wedge (\neg Z_{n}\vee Y_{n}).}$

Una traducción alternativa, la transformación Tseitin, incluye también las cláusulas ${\displaystyle Z_{i}\vee \neg X_{i}\vee \neg Y_{i}}$. Con estas cláusulas, la fórmula implica ${\displaystyle Z_{i}\equiv X_{i}\wedge Y_{i}}$; esta fórmula muchas veces se considera para "definir" ${\displaystyle Z_{i}}$ siendo un nombre para ${\displaystyle X_{i}\wedge Y_{i}}$.

En la lógica de primer orden, forma normal conjuntiva puede tomarse más para producir la forma normal clausal de una fórmula lógica, que se puede utilizar luego para realizar la resolución de primer orden. En una resolución basada en la provisión automatizada de teorema, una fórmula FNC

${\displaystyle (}$

${\displaystyle l_{11}}$

${\displaystyle \lor }$

${\displaystyle \ldots }$

${\displaystyle \lor }$

${\displaystyle l_{1n_{1}}}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \ldots }$

${\displaystyle \land }$

${\displaystyle (}$

${\displaystyle l_{m1}}$

${\displaystyle \lor }$

${\displaystyle \ldots }$

${\displaystyle \lor }$

${\displaystyle l_{mn_{m}}}$

${\displaystyle )}$

, con literales ${\displaystyle l_{ij}}$, es comúnmente representado como un conjunto de conjuntos

${\displaystyle \{}$

${\displaystyle \{}$

${\displaystyle l_{11}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle l_{1n_{1}}}$

${\displaystyle \}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle \{}$

${\displaystyle l_{m1}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle l_{mn_{m}}}$

${\displaystyle \}}$

${\displaystyle \}}$

.

Un importante conjunto de problemas en complejidad computacional incluye el encontrar asignaciones para las variables de una fórmula expresada como forma normal conjuntiva, de modo que la fórmula sea verdadera. El problema k-SAT es un problema computacional que consiste en encontrar una asignación satisfacible para una fórmula expresada en FNC tal que cada disyunción contenga la mayor cantidad de variables k posibles. El problema 3-SAT es NP-completo (así como cualquier otro problema k-SAT con k>2), mientras que el problema 2-SAT es resoluble en tiempo polinómico. Como consecuencia,[nota 1] la tarea de convertir una fórmula a una FND, preservando la satisfactibilidad, es NP-hard; dualmente, convertido en FNC, preservando satisfactilidad, también es NP-hard; por lo tanto la equivalencia preservando conversión en FND o FNC también es un NP-hard.

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

Una fórmula en FNC se puede convertir en una fórmula equisatisfiable en "kFNC" (para k> = 3) sustituyendo cada uno en conjunción con más de variables k ${\displaystyle X_{1}\vee \cdots \vee X_{k}\vee \cdots \vee X_{n}}$ por dos conjunciones ${\displaystyle X_{1}\vee \cdots \vee X_{k-1}\vee Z}$ y ${\displaystyle \neg Z\vee X_{k}\cdots \vee X_{n}}$ con una nueva variable ${\displaystyle Z}$, y repitiendo cuantas veces sea necesario.

Para convertir lógica de primer orden a FNC:[3]

1. Convertir a forma normal negativa.
   1. Eliminar implicaciones y equivalencias: sustituir reiteradamente ${\displaystyle P\rightarrow Q}$ con ${\displaystyle \lnot P\lor Q}$; sustituir ${\displaystyle P\leftrightarrow Q}$ con ${\displaystyle (P\lor \lnot Q)\land (\lnot P\lor Q)}$. Eventualmente, esto eliminará todas las apariciones de ${\displaystyle \rightarrow }$ y ${\displaystyle \leftrightarrow }$.
   2. Desplazar NOTs hacia el interior aplicando varias veces la ley de De Morgan. En concreto, sustituya ${\displaystyle \lnot (P\lor Q)}$ con ${\displaystyle (\lnot P)\land (\lnot Q)}$; reemplace ${\displaystyle \lnot (P\land Q)}$ por ${\displaystyle (\lnot P)\lor (\lnot Q)}$; reemplace ${\displaystyle \lnot \lnot P}$ por ${\displaystyle P;}$ reemplace ${\displaystyle \lnot (\forall xP(x))}$ por ${\displaystyle \exists x\lnot P(x)}$; ${\displaystyle \lnot (\exists xP(x)))}$ por ${\displaystyle \forall x\lnot P(x)}$. Después de eso, un ${\displaystyle \lnot }$ puede ocurrir solo inmediatamente antes de un símbolo de predicado.
2. Estandarizar variables
   1. Para sentencias como ${\displaystyle (\forall xP(x))\lor (\exists xQ(x))}$ que utilice el mismo nombre de variable dos veces, cambiar el nombre de una de las variables. Esto evita confusiones posteriores al dejar cuantificadores para más tarde. Por ejemplo, ${\displaystyle \forall x[\exists yAnimal(y)\land \lnot Amores(x,y)]\lor [\exists yAmores(y,x)]}$ se renombra a ${\displaystyle \forall x[\exists yAnimal(y)\land \lnot Amores(x,y)]\lor [\exists zAmores(z,x)]}$.
3. Skolemizar la declaración
   1. Desplazar cuantificadores hacia el exterior: sustituir reiteradamente ${\displaystyle P\land (\forall xQ(x))}$ con ${\displaystyle \forall x(P\land Q(x))}$; reemplace ${\displaystyle P\lor (\forall xQ(x))}$ con ${\displaystyle \forall x(P\lor Q(x))}$; reemplace ${\displaystyle P\land (\exists xQ(x))}$ con ${\displaystyle \exists x(P\land Q(x))}$; reemplace ${\displaystyle P\lor (\exists xQ(x))}$ con ${\displaystyle \exists x(P\lor Q(x))}$. Estos reemplazos conservan la equivalencia, ya que el paso de normalización variable anterior se aseguró de que x no ocurre en P. Después de estos reemplazos, un cuantificador puede ocurrir solo en el prefijo inicial de la fórmula, pero nunca dentro de un ${\displaystyle \land }$, o ${\displaystyle \lor }$.
   2. Reemplazar repetidamente ${\displaystyle \forall x_{1}\ldots \forall x_{n}\;\exists y\;P(y)}$ con ${\displaystyle \forall x_{1}\ldots \forall x_{n}\;P(f(x_{1},\ldots ,x_{n}))}$, donde f es un nuevo símbolo de la función n-aria, la denominada "función de Skolem". Este es el único paso que conserva solamente satisfacibilidad en lugar de equivalencia. Se eliminan todos los cuantificadores existenciales.
4. Descartar todos los cuantificadores universales.
5. Distribuir ORs hacia adentro sobre ANDs: sustituir reiteradamente ${\displaystyle P\lor (Q\land R)}$ con ${\displaystyle (P\lor Q)\land (P\lor R)}$.

A modo de ejemplo, la fórmula que dice "Quien ama a todos los animales, es a su vez amado por alguien" se convierte en FNC (y posteriormente en forma de cláusula en la última línea) de la siguiente manera (resaltando regla de sustitución redichas con ${\displaystyle {\color {red}{\text{rojo}}}}$):

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \forall y}$

${\displaystyle Animal(}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \color {red}\rightarrow }$

${\displaystyle Amores(x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \rightarrow }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle Amores(}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \forall y}$

${\displaystyle \lnot }$

${\displaystyle Animal(}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle Amores(x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\rightarrow }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle Amores(}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

por 1.1

${\displaystyle \forall x}$

${\displaystyle \color {red}\lnot }$

${\displaystyle (}$

${\displaystyle {\color {red}{\forall y}}}$

${\displaystyle \lnot }$

${\displaystyle Animal(}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle Amores(x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle Amores(}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

por 1.1

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle \color {red}\lnot }$

${\displaystyle (}$

${\displaystyle \lnot }$

${\displaystyle Animal(}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle Amores(x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle Amores(}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

por 1.2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle \color {red}\lnot }$

${\displaystyle \color {red}\lnot }$

${\displaystyle Animal(}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle Amores(x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle Amores(}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

por 1.2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle Animal(}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle Amores(x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \color {red}\exists }$

${\displaystyle \color {red}y}$

${\displaystyle Amores(}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

por 1.2

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle Animal(}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle Amores(x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle (}$

${\displaystyle \color {red}\exists }$

${\displaystyle \color {red}z}$

${\displaystyle Amores(}$

${\displaystyle z}$

${\displaystyle ,x)}$

${\displaystyle )}$

por 2

${\displaystyle \forall x}$

${\displaystyle \exists z}$

${\displaystyle (}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle Animal(}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle Amores(x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle Amores(}$

${\displaystyle z}$

${\displaystyle ,x)}$

por 3.1

${\displaystyle \forall x}$

${\displaystyle {\color {red}{\exists z}}}$

${\displaystyle \exists y}$

${\displaystyle (}$

${\displaystyle Animal(}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle Amores(x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle Amores(}$

${\displaystyle z}$

${\displaystyle ,x)}$

por 3.1

${\displaystyle \forall x}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle (}$

${\displaystyle Animal(}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle Amores(x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle Amores(}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

por 3.2

${\displaystyle (}$

${\displaystyle Animal(}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle \color {red}\land }$

${\displaystyle \lnot }$

${\displaystyle Amores(x,}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle Amores(}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

por 4

${\displaystyle (}$

${\displaystyle Animal(}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle Amores(}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

${\displaystyle )}$

${\displaystyle \color {red}\land }$

${\displaystyle (}$

${\displaystyle \lnot Amores(x,f(x))}$

${\displaystyle \color {red}\lor }$

${\displaystyle Amores(g(x),x)}$

${\displaystyle )}$

por 5

${\displaystyle \{}$

${\displaystyle \{}$

${\displaystyle Animal(}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle ,}$

${\displaystyle Amores(}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

${\displaystyle \}}$

${\displaystyle ,}$

${\displaystyle \{}$

${\displaystyle \lnot Amores(x,f(x))}$

${\displaystyle ,}$

${\displaystyle Amores(g(x),x)}$

${\displaystyle \}}$

${\displaystyle \}}$

(cláusula de representación)

Informalmente, la función skolem ${\displaystyle g(x)}$ puede ser pensado como dando a la persona por quien es amado ${\displaystyle x}$, mientras que ${\displaystyle f(x)}$ se obtiene el animal (si los hay) que ${\displaystyle x}$ no ama. La tercera última línea contando desde abajo se lee como "${\displaystyle x}$ no ama al animal ${\displaystyle f(x)}$, o bien ${\displaystyle x}$ es amado por ${\displaystyle g(x)}$".

La segunda última línea de arriba, ${\displaystyle (Animal(f(x))\lor Amores(g(x),x))\land (\lnot Amores(x,f(x))\lor Amores(g(x),x))}$, es la FNC.

• Forma normal algebraica
• Forma normal disyuntiva
• Cláusula de Horn
• Algoritmo Quine–McCluskey

1. ya que una manera de comprobar una FNC por satisfactibilidad es convertirla en DNF, la satisfactibilidad de la misma se puede comprobar en el tiempo lineal

• Paul Jackson, Daniel Sheridan: Clause Form Conversions for Boolean Circuits. In: Holger H. Hoos, David G. Mitchell (Eds.): Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10–13, 2004, Revised Selected Papers. Lecture Notes in Computer Science 3542, Springer 2005, pp. 183–198
• G.S. Tseitin: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Structures in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics (translated from Russian), pp. 115–125. Steklov Mathematical Institute (1968)

• Hazewinkel, Michiel, ed. (2001), «Conjunctive normal form», Encyclopaedia of Mathematics (en inglés), Springer, ISBN 978-1556080104.
• Conversión de fnc a fnd usando computación grid (en inglés)
• Conversión de fnc a fnd usando computación grid en paralelo (en inglés)
• Esta obra contiene una traducción derivada de «Conjunctive normal form» de Wikipedia en inglés, concretamente de esta versión, publicada por sus editores bajo la Licencia de documentación libre de GNU y la Licencia Creative Commons Atribución-CompartirIgual 4.0 Internacional.