Forma normal conjuntiva

En lógica booleana, una fórmula está en forma normal conjuntiva (CNF) o forma normal de cláusula si es una conjunción de uno 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 ORs. Como forma normal canónica, es útil en la demostración automatizada de teoremas y 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 sola cláusula, respectivamente. Como en la forma normal disyuntiva (DNF), los únicos conectores proposicionales que puede contener una fórmula en CNF son and, or y not. 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 automática de teoremas, la noción "forma normal de cláusula" a menudo se usa en un sentido más estricto, lo que significa una representación particular de una fórmula CNF como un conjunto de conjuntos de literales.

Ejemplos y no ejemplos

Todas las siguientes fórmulas en las variables ${displaystyle A,B,C,D,E}$, y ${displaystyle F}$ están en forma normal conjuntiva:

• ${displaystyle (Alor neg Blor neg C)land (neg Dlor Elor F)}$
• ${displaystyle (Alor B)land (C)}$
• ${displaystyle (Alor B)}$
• ${displaystyle (A)}$

Para la claridad, las cláusulas disyuntivas están escritas dentro de paréntesis arriba. En forma disyuntiva normal con cláusulas conjuntivas paréntesis, el último caso es el mismo, pero el siguiente al último es ${displaystyle (A)lor (B)}$. Las constantes verdadero y falso son denotados por el conjunto vacío y una cláusula que consiste en el disyunto vacío, pero normalmente están escritos explícitamente.

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

• ${displaystyle neg (Blor C)}$, ya que un OR está anidado dentro de un NO
• ${displaystyle (Aland B)lor C}$
• ${displaystyle Aland (Blor (Dland E)}$, ya que un Y 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:

• ${displaystyle (neg B)land (neg C)}$
• ${displaystyle (Alor C)land (Blor C)}$
• ${displaystyle (A)land (Blor D)land (Blor E). }$

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 doble negación, leyes de De Morgan y la ley distributiva.

Dado que todas las fórmulas proposiciones pueden convertirse en una fórmula equivalente en forma conjuntiva normal, las pruebas se basan a menudo en la suposición de que todas las fórmulas son CNF. Sin embargo, en algunos casos esta conversión al CNF puede llevar a una explosión exponencial de la fórmula. Por ejemplo, la traducción de la siguiente fórmula no-FNC en el FNC produce una fórmula con ${displaystyle 2^{n}$ cláusulas:

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

En particular, la fórmula generada es:

${be1}veecdotsveeveecdots vee X_{n}wedge (Y_{1}vee X_{2}veecdots vee X_{1}veevee$

Esta fórmula contiene ${displaystyle 2^{n}$ cláusulas; cada cláusula contiene cualquiera ${displaystyle X_{i}$ o ${displaystyle Y...$ para cada uno ${displaystyle i}$.

Existen transformaciones en la CNF que evitan un aumento exponencial del tamaño preservando la satisfiabilidad en lugar de la equivalencia. Estas transformaciones están garantizadas sólo para aumentar linealmente el tamaño de la fórmula, pero introducir nuevas variables. Por ejemplo, la fórmula anterior puede transformarse en CNF añadiendo 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}veeneg] }$

Una interpretación satisface esta fórmula sólo si al menos una de las nuevas variables es verdadera. Si esta variable es ${displaystyle Z_{i}$, entonces ambos ${displaystyle X_{i}$ y ${displaystyle Y...$ son verdaderos también. Esto significa que cada modelo que satisface esta fórmula también satisface al original. Por otro lado, sólo algunos de los modelos de la fórmula original satisfacen esta: ${displaystyle Z_{i}$ no se mencionan en la fórmula original, sus valores son irrelevantes para la satisfacción de ella, 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 equitativas pero no equivalentes.

Una traducción alternativa, la transformación de 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...$; esta fórmula se considera a menudo para "definir" ${displaystyle Z_{i}$ para ser un nombre ${displaystyle X_{i}wedge Y...$.

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 de cláusula de una fórmula lógica, que luego se puede usar para realizar una resolución de primer orden. En la demostración de teoremas automatizada basada en resolución, una fórmula CNF

${displaystyle (}$

${displaystyle l_{11}$

${displaystyle lor }$

${displaystyle ldots }$

${displaystyle lor }$

${displaystyle I_{1n_{1}}$

${displaystyle)}$

${displaystyle land }$

${displaystyle ldots }$

${displaystyle land }$

${displaystyle (}$

${displaystyle l_{m1}$

${displaystyle lor }$

${displaystyle ldots }$

${displaystyle lor }$

${displaystyle I_{mn_{m}}$

${displaystyle)}$

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

${displaystyle}$

${displaystyle}$

${displaystyle l_{11}$

${displaystyle}$

${displaystyle ldots }$

${displaystyle}$

${displaystyle I_{1n_{1}}$

${displaystyle}$

${displaystyle}$

${displaystyle ldots }$

${displaystyle}$

${displaystyle}$

${displaystyle l_{m1}$

${displaystyle}$

${displaystyle ldots }$

${displaystyle}$

${displaystyle I_{mn_{m}}$

${displaystyle}$

${displaystyle}$

.

Vea a continuación un ejemplo.

Complejidad computacional

Un conjunto importante de problemas de 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 variables k. 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; dualmente, convertir en CNF, preservando la validez, también es NP-difícil; por lo tanto, la conversión que conserva la equivalencia en DNF o CNF es nuevamente NP-difícil.

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 el CNF se puede convertir en una fórmula equisatisfecha en "kCNF (para k≥3) reemplazando cada conjunto con más de k variables ${displaystyle X_{1}vee cdots vee X_{k}vee cdots vee X_{n}$ por dos conjuntos ${displaystyle X_{1}vee cdots vee X_{k-1}vee Z}$ y ${displaystyle neg Zvee X_{k}cdots vee X_{n}$ con Z una nueva variable, y repetir tan a menudo como sea necesario.

Conversión desde lógica de primer orden

Para convertir lógica de primer orden a CNF:

1. Convert to negation normal form.
   1. Eliminate implications and equivalences: repeatedly replace ${displaystyle Prightarrow Q}$ with ${displaystyle lnot Plor Q}$; replace ${displaystyle Pleftrightarrow Q}$ with ${displaystyle (Plor lnot Q)land (lnot Plor Q)}$. Eventually, this will eliminate all occurrences of ${displaystyle rightarrow }$ and ${displaystyle leftrightarrow }$.
   2. Move NOTs inwards by repeatedly applying De Morgan's law. Specifically, replace ${displaystyle lnot (Plor Q)}$ with ${displaystyle (lnot P)land (lnot Q)}$; replace ${displaystyle lnot (Pland Q)}$ with ${displaystyle (lnot P)lor (lnot Q)}$; and replace ${displaystyle lnot lnot P}$ with ${displaystyle P}$; replace ${displaystyle lnot (forall xP(x))}$ with ${displaystyle exists xlnot P(x)}$; ${displaystyle lnot (exists xP(x))}$ with ${displaystyle forall xlnot P(x)}$. After that, a ${displaystyle lnot }$ may occur only immediately before a predicate symbol.
2. Standardize variables
   1. For sentences like ${displaystyle (forall xP(x))lor (exists xQ(x))}$ which use the same variable name twice, change the name of one of the variables. This avoids confusion later when dropping quantifiers. For example, ${displaystyle forall x[exists ymathrm {Animal} (y)land lnot mathrm {Loves} (x,y)]lor [exists ymathrm {Loves} (y,x)]}$ is renamed to ${displaystyle forall x[exists ymathrm {Animal} (y)land lnot mathrm {Loves} (x,y)]lor [exists zmathrm {Loves} (z,x)]}$.
3. Skolemize the statement
   1. Move quantifiers outwards: repeatedly replace ${displaystyle Pland (forall xQ(x))}$ with ${displaystyle forall x(Pland Q(x))}$; replace ${displaystyle Plor (forall xQ(x))}$ with ${displaystyle forall x(Plor Q(x))}$; replace ${displaystyle Pland (exists xQ(x))}$ with ${displaystyle exists x(Pland Q(x))}$; replace ${displaystyle Plor (exists xQ(x))}$ with ${displaystyle exists x(Plor Q(x))}$. These replacements preserve equivalence, since the previous variable standardization step ensured that ${displaystyle x}$ doesn't occur in ${displaystyle P}$. After these replacements, a quantifier may occur only in the initial prefix of the formula, but never inside a ${displaystyle lnot }$, ${displaystyle land }$, or ${displaystyle lor }$.
   2. Repeatedly replace ${displaystyle forall x_{1}ldots forall x_{n};exists y;P(y)}$ with ${displaystyle forall x_{1}ldots forall x_{n};P(f(x_{1},ldotsx_{n}))}$, where ${displaystyle f}$ is a new ${displaystyle n}$-ary function symbol, a so-called "Skolem function". This is the only step that preserves only satisfiability rather than equivalence. It eliminates all existential quantifiers.
4. Drop all universal quantifiers.
5. Distribute ORs inwards over ANDs: repeatedly replace ${displaystyle Plor (Qland R)}$ with ${displaystyle (Plor Q)land (Plor R)}$.

Como 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 (la regla de sustitución de alto nivel redexes en ${displaystyle {color {red} {text{red}}} {f}}} {f}}} {f}}} {f}}}}$):

${displaystyle forall x}$

${displaystyle (}$

${displaystyle forall y}$

${displaystyle mathrm {Animal} (}$

${displaystyle y}$

${displaystyle)}$

${displaystyle color {red}rightarrow }$

${displaystyle mathrm {Loves} (x,}$

${displaystyle y}$

${displaystyle)}$

${displaystyle)}$

${displaystyle rightarrow }$

${displaystyle (}$

${displaystyle exists }$

${displaystyle y}$

${displaystyle mathrm {Loves} (}$

${displaystyle y}$

${displaystylex)}$

${displaystyle)}$

${displaystyle forall x}$

${displaystyle (}$

${displaystyle forall y}$

${displaystyle lnot }$

${displaystyle mathrm {Animal} (}$

${displaystyle y}$

${displaystyle)}$

${displaystyle lor }$

${displaystyle mathrm {Loves} (x,}$

${displaystyle y}$

${displaystyle)}$

${displaystyle)}$

${displaystyle color {red}rightarrow }$

${displaystyle (}$

${displaystyle exists }$

${displaystyle y}$

${displaystyle mathrm {Loves} (}$

${displaystyle y}$

${displaystylex)}$

${displaystyle)}$

by 1.1

${displaystyle forall x}$

${displaystyle color {red}lnot }$

${displaystyle (}$

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

${displaystyle lnot }$

${displaystyle mathrm {Animal} (}$

${displaystyle y}$

${displaystyle)}$

${displaystyle lor }$

${displaystyle mathrm {Loves} (x,}$

${displaystyle y}$

${displaystyle)}$

${displaystyle)}$

${displaystyle lor }$

${displaystyle (}$

${displaystyle exists }$

${displaystyle y}$

${displaystyle mathrm {Loves} (}$

${displaystyle y}$

${displaystylex)}$

${displaystyle)}$

by 1.1

${displaystyle forall x}$

${displaystyle (}$

${displaystyle exists y}$

${displaystyle color {red}lnot }$

${displaystyle (}$

${displaystyle lnot }$

${displaystyle mathrm {Animal} (}$

${displaystyle y}$

${displaystyle)}$

${displaystyle color {red}lor }$

${displaystyle mathrm {Loves} (x,}$

${displaystyle y}$

${displaystyle)}$

${displaystyle)}$

${displaystyle)}$

${displaystyle lor }$

${displaystyle (}$

${displaystyle exists }$

${displaystyle y}$

${displaystyle mathrm {Loves} (}$

${displaystyle y}$

${displaystylex)}$

${displaystyle)}$

by 1.2

${displaystyle forall x}$

${displaystyle (}$

${displaystyle exists y}$

${displaystyle color {red}lnot }$

${displaystyle color {red}lnot }$

${displaystyle mathrm {Animal} (}$

${displaystyle y}$

${displaystyle)}$

${displaystyle land }$

${displaystyle lnot }$

${displaystyle mathrm {Loves} (x,}$

${displaystyle y}$

${displaystyle)}$

${displaystyle)}$

${displaystyle lor }$

${displaystyle (}$

${displaystyle exists }$

${displaystyle y}$

${displaystyle mathrm {Loves} (}$

${displaystyle y}$

${displaystylex)}$

${displaystyle)}$

by 1.2

${displaystyle forall x}$

${displaystyle (}$

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

${displaystyle mathrm {Animal} (}$

${displaystyle y}$

${displaystyle)}$

${displaystyle land }$

${displaystyle lnot }$

${displaystyle mathrm {Loves} (x,}$

${displaystyle y}$

${displaystyle)}$

${displaystyle)}$

${displaystyle lor }$

${displaystyle (}$

${displaystyle color {red}exists }$

${displaystyle color {red}y}$

${displaystyle mathrm {Loves} (}$

${displaystyle y}$

${displaystylex)}$

${displaystyle)}$

by 1.2

${displaystyle forall x}$

${displaystyle (}$

${displaystyle exists y}$

${displaystyle mathrm {Animal} (}$

${displaystyle y}$

${displaystyle)}$

${displaystyle land }$

${displaystyle lnot }$

${displaystyle mathrm {Loves} (x,}$

${displaystyle y}$

${displaystyle)}$

${displaystyle)}$

${displaystyle color {red}lor }$

${displaystyle (}$

${displaystyle color {red}exists }$

${displaystyle color {red}z}$

${displaystyle mathrm {Loves} (}$

${displaystyle z}$

${displaystylex)}$

${displaystyle)}$

by 2

${displaystyle forall x}$

${displaystyle exists z}$

${displaystyle (}$

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

${displaystyle mathrm {Animal} (}$

${displaystyle y}$

${displaystyle)}$

${displaystyle land }$

${displaystyle lnot }$

${displaystyle mathrm {Loves} (x,}$

${displaystyle y}$

${displaystyle)}$

${displaystyle)}$

${displaystyle color {red}lor }$

${displaystyle mathrm {Loves} (}$

${displaystyle z}$

${displaystylex)}$

by 3.1

${displaystyle forall x}$

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

${displaystyle exists y}$

${displaystyle (}$

${displaystyle mathrm {Animal} (}$

${displaystyle y}$

${displaystyle)}$

${displaystyle land }$

${displaystyle lnot }$

${displaystyle mathrm {Loves} (x,}$

${displaystyle y}$

${displaystyle)}$

${displaystyle)}$

${displaystyle lor }$

${displaystyle mathrm {Loves} (}$

${displaystyle z}$

${displaystylex)}$

by 3.1

${displaystyle forall x}$

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

${displaystyle (}$

${displaystyle mathrm {Animal} (}$

${displaystyle y}$

${displaystyle)}$

${displaystyle land }$

${displaystyle lnot }$

${displaystyle mathrm {Loves} (x,}$

${displaystyle y}$

${displaystyle)}$

${displaystyle)}$

${displaystyle lor }$

${displaystyle mathrm {Loves} (}$

${displaystyle g(x)}$

${displaystylex)}$

by 3.2

${displaystyle (}$

${displaystyle mathrm {Animal} (}$

${displaystyle f(x)}$

${displaystyle)}$

${displaystyle color {red}land }$

${displaystyle lnot }$

${displaystyle mathrm {Loves} (x,}$

${displaystyle f(x)}$

${displaystyle)}$

${displaystyle)}$

${displaystyle color {red}lor }$

${displaystyle mathrm {Loves} (}$

${displaystyle g(x)}$

${displaystylex)}$

by 4

${displaystyle (}$

${displaystyle mathrm {Animal} (}$

${displaystyle f(x)}$

${displaystyle)}$

${displaystyle color {red}lor }$

${displaystyle mathrm {Loves} (}$

${displaystyle g(x)}$

${displaystylex)}$

${displaystyle)}$

${displaystyle color {red}land }$

${displaystyle (}$

${displaystyle lnot mathrm {Loves} (x,f(x))}$

${displaystyle color {red}lor }$

${displaystyle mathrm {Loves} (g(x),x)}$

${displaystyle)}$

by 5

${displaystyle {}$

${displaystyle {}$

${displaystyle mathrm {Animal} (}$

${displaystyle f(x)}$

${displaystyle)}$

${displaystyle}$

${displaystyle mathrm {Loves} (}$

${displaystyle g(x)}$

${displaystylex)}$

${displaystyle }}$

${displaystyle}$

${displaystyle {}$

${displaystyle lnot mathrm {Loves} (x,f(x))}$

${displaystyle}$

${displaystyle mathrm {Loves} (g(x),x)}$

${displaystyle }}$

${displaystyle }}$

(clause representation)

Informalmente, la función Skolem ${displaystyle g(x)}$ puede ser pensado como ceder a la persona por quien ${displaystyle x}$ es amado, mientras ${displaystyle f(x)}$ cede el animal (si hay) que ${displaystyle x}$ no ama. La tercera última línea de abajo lee como "${displaystyle x}$ no ama al animal ${displaystyle f(x)}$, o si no ${displaystyle x}$ es amado ${displaystyle g(x)}$".

La segunda última línea de arriba, ${displaystyle (mathrm {Animal} (f(x))lor mathrm {Loves} (g(x),x)))land (lnot mathrm {Loves} (x,f(x)))lormat hrm {Loves} (g(x),x)})}$, es el CNF.

Notas