Forma normal conjuntiva (FNC): definición, ejemplo y equivalente en inglés
La forma normal conjuntiva (FNC) es un AND de cláusulas, cada cláusula un OR de literales. Es el formato de entrada de los solucionadores SAT, y toda fórmula tiene una FNC equivalente.
Una fórmula está en forma normal conjuntiva cuando es una conjunción de disyunciones de literales: (A OR B) AND (NOT A OR NOT B) lo es, con dos cláusulas. FNC es el nombre que da la lógica al producto de sumas. La conversión es la imagen de la de la FND: reescribir los operadores derivados, llevar las negaciones hasta las variables con De Morgan y después distribuir OR sobre AND. La FNC canónica, construida con maxtérminos, es única; las FNC más cortas no lo son.
El artefacto de esta página convierte A XOR B. La FNC del conversor es (A OR B) AND (NOT A OR NOT B), 2 cláusulas y 4 literales, por una eliminación del XOR: la primera cláusula dice que al menos una es verdadera, la segunda que no ambas. La FND de la misma fórmula es (A AND NOT B) OR (NOT A AND B), también 2 términos y 4 literales. La tabla de 4 filas se lee falso, verdadero, verdadero, falso, y la comprobación de satisfacible se cumple con el testigo A = FALSE, B = TRUE.
La FNC importa porque un solucionador SAT consume cláusulas: una vez que un problema está en FNC, la satisfacibilidad puede decidirse por propagación unitaria y resolución, y el propio motor recurre a un solucionador más allá de su límite exhaustivo. La FNC es también la forma natural de una lista de restricciones, donde cada cláusula es una regla que debe cumplirse. El término se confunde con la FND, su dual, y «forma normal» se toma a veces por simplificada, cosa que no es.
Ejemplo
f := A XOR B · salida
Comprobaciones exactas
Tabla de verdad (4 filas)
| # | A | B | f |
|---|---|---|---|
| 0 | FALSO | FALSO | FALSO |
| 1 | FALSO | VERDADERO | VERDADERO |
| 2 | VERDADERO | FALSO | VERDADERO |
| 3 | VERDADERO | VERDADERO | FALSO |
Lectura en lenguaje claro
Principiantef es verdadero exactamente cuando exactamente uno entre A y B es verdadero (no ambos).
En todos los demás casos, f es falso.
Sobre los operadores:
- XOR (O exclusivo) es verdadero cuando exactamente una de sus dos partes es verdadera.
Intermediof es verdadero exactamente cuando exactamente uno entre A y B es verdadero (no ambos).
En todos los demás casos, f es falso.
Avanzadof es verdadero exactamente cuando exactamente uno entre A y B es verdadero (no ambos) [disyunción exclusiva ⊕].
En todos los demás casos, f es falso.
Notación formal: A ⊕ B
Formas normales
Forma normal conjuntiva (FNC)
(A OR B) AND (NOT A OR NOT B)2 cláusulas, 4 literales · complete · Eliminación de XOR ×1
Forma normal disyuntiva (FND)
(A AND NOT B) OR (NOT A AND B)2 términos, 4 literales · complete · Eliminación de XOR ×1
El error habitual
Esperar que la FNC sea corta. Convertir una FND con k términos de dos literales cada uno puede producir 2 elevado a k cláusulas; el conversor se detiene en 4.096 términos y 20.000 literales e informa del límite en lugar de dar una forma incompleta. El método canónico o el respaldo por implicantes primos son la alternativa.
Preguntas
¿Una fórmula en FNC es automáticamente satisfacible?
No. (A) AND (NOT A) está en FNC y es una contradicción. La FNC es una forma, no un veredicto; decidir la satisfacibilidad de una FNC es exactamente el problema SAT.
Relacionado
Ejercicios
Véase también
- Forma normal disyuntiva (FND): definición, ejemplo y equivalente en inglés
- Cláusula: definición, ejemplo y equivalente en inglés
- Producto de sumas (POS): definición, ejemplo y equivalente en inglés
- Solucionador SAT: definición, ejemplo y equivalente en inglés
- Conversor a FNC y FND: formas normales conjuntiva y disyuntiva, mintérminos y maxtérminos
- Eliminación de XOR: A ⊕ B = A·B' + A'·B
Glosario
Generado a partir del motor de Tangibool, semántica tangibool-semantics/1, motor 1.0.0, compilación . Cada tabla, mapa, simplificación y veredicto de estas páginas lo calculó el motor de Tangibool al compilar el sitio, y cada afirmación la volvió a comprobar el mismo verificador exacto que usa la app. Los límites se indican donde aplican. © 2026 Foreranger LTD.