Forma normal conjuntiva

Origem: Wikipédia, a enciclopédia livre.

Na lógica booleana, uma fórmula está na forma normal conjuntiva (FNC) se é uma conjunção de cláusulas, onde uma cláusula é uma disjunção de literais. Sendo uma forma normal, a FNC é útil em provas automáticas de teoremas. Ela é similar à forma canônica de soma de produtos usada em teoria dos circuitos.

Toda conjunção de literais e toda disjunção de literais estão na FNC, já que elas podem ser vistas respecticvamente conjunções de cláusulas de um literal e conjunções de uma só cláusula, respectivamente. Assim como na forma normal disjuntiva (FND), os únicos conectivos proposicionais que uma fórmula na FNC pode conter são os operadores e, ou e não. O operador não pode ser usado apenas como parte de um literal, e portanto ele pode aparecer apenas na frente de variáveis proposicionais.

Por exemplo, todas as fórmulas seguintes estão na FNC:

$A \wedge B$

$\neg A \wedge (B \vee C)$

$(A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E)$

$(\neg B \vee C).$ :

Porém, as seguintes fórmulas não estão:

$\neg (B \vee C)$

$(A \wedge B) \vee C$

$A \wedge (B \vee (D \wedge E)).$

As três fórmulas acima são equivalentes respectivamente às três fórmulas seguintes que estão na forma normal conjuntiva:

$\neg B \wedge \neg C$

$(A \vee C) \wedge (B \vee C)$

$A \wedge (B \vee D) \wedge (B \vee E).$

Toda fórmula proposicional pode ser convertida para uma fórmula equivalente que está na FNC. Essa transformação é baseada em regras sobre equivalências lógicas: Lei da Dupla Negação, Leis de De Morgan, e a Distributividade.

Uma vez que todas as fórmulas lógicas clássicas podem ser convertidas em fórmulas equivalentes na forma normal conjuntiva, muitas demonstrações são baseadas na suposição de que todas as fórmulas estão na FNC. Contudo, em alguns casos, essa conversão para FNC pode levar a uma explosão exponencial da fórmula. Por exemplo, traduzindo a seguinte fórmula que não está na FNC para FNC, obtemos uma fórmula com $2 n$ cláusulas:

$(X_1 \wedge Y_1) \vee (X_2 \wedge Y_2) \vee \dots \vee (X_n \wedge Y_n).$

A seguinte fórmula é uma gramática formal para FNC:

1. <or> → ∨

2. <e> → ∧

3. <não> → ¬

4. <conjunção> → <disjunção>

5. <conjunção> → <conjunção> <ou> <disjunção>

6. <disjunção> → <literal>

7. <disjunção> → (<disjunção> <e> <literal>)

8. <literal> → <termo>

9. <literal> → <não><termo>

Onde <termo> é qualquer variável.

Existem tranformações das fórmulas na FNC que preservam a satisfatibilidade ao invés da equivalência e não produzem um aumento exponencial do tamanho. Tais transformações aumentam o tamanho da fórmula apenas por um fator linear, mas introduzem novas variáveis.

A forma normal conjuntiva pode ser levada adiante de modo a produzir a forma normal clausal de uma fórmula lógica, a qual é usada para se efetuar resolução de primeira ordem.

Um importante conjunto de problemas em complexidade computacional envolve encontrar atribuições para as variáveis de uma fórmula booleana expressa na Forma Normal Conjuntiva, tais que a fórmula seja satisfeita. O problema k-SAT é o problema de encontrar uma atribuição que satisfaça para uma fórmula booleana expressa na FNC, tal que cada disjunção contenha no máximo k variáveis. 3-SAT é NP-completo (assim como qualquer outro problema k-SAT com k>2), enquanto 2-SAT pode ser resolvido em tempo polinomial.