Considere a seguinte fórmula proposicional no formato clausal:
\{\neg \mathbf{a} \vee \mathbf{b} \vee \mathbf{c}\},\{\neg \mathbf{b} \vee \neg \mathbf{c} \vee \mathbf{a}\},\{\mathbf{a}\},\{\mathbf{b} \vee \mathbf{d}\},\{\neg \mathbf{c} \vee \mathbf{d} \vee \mathbf{c}\},\{\mathbf{b} \vee \neg \mathbf{d}\},\{\neg \mathbf{b} \vee \mathbf{d}\}
Se aplicarmos unit propagation a essa fórmula, quais das seguintes cláusulas permanecerão na fórmula resultante após a propagação?
a) \{\mathrm{b} \vee \mathrm{d}\}
b) \{\mathrm{c} \vee \vee \mathrm{d} \vee \mathrm{c}\}
c) \{\neg \mathrm{b} \vee \neg \mathrm{c} \vee \mathrm{a}\}
d) \{\mathrm{a}\}
e) \{\neg \mathrm{b} \vee \mathrm{d}\}

Passo 1

O enunciado nos dá a fórmula clausal
\{\neg a \vee b \vee c\},\;\{\neg b \vee \neg c \vee a\},\;\{a\},\;\{b \vee d\},\;\{\neg c \vee d \vee c\},\;\{b \vee \neg d\},\;\{\neg b \vee d\}
e pede para aplicar unit propagation. Vamos usar que, sempre que temos uma cláusula unitária \{L\}, atribuímos L=\text{verdadeiro}, eliminamos todas as cláusulas que contêm L e removemos de cada cláusula restante todas as ocorrências de \neg L.

Passo 2

Identificamos a cláusula unitária \{a\}. Logo atribuímos
a = \text{verdadeiro}.
Agora simplificamos a fórmula:
  • Qualquer cláusula que contenha a é satisfeita e, portanto, removida.
  • Em qualquer cláusula que contenha \neg a, removemos esse literal.
Das cláusulas originais: \{\neg a \vee b \vee c\} perde \neg a e vira \{b \vee c\}. \{\neg b \vee \neg c \vee a\} é satisfeita por a e some. \{a\} some por estar satisfeita.
As demais não contêm nem a nem \neg a e ficam inalteradas.

Passo 3

Após essa propagação obtemos a fórmula simplificada
\{b \vee c\},\;\{b \vee d\},\;\{\neg c \vee d \vee c\},\;\{b \vee \neg d\},\;\{\neg b \vee d\}.

Passo 4

Procuramos novas cláusulas unitárias: todas têm dois ou mais literais. Logo o processo para aqui.

Resposta

As cláusulas que permanecem (entre as da lista de alternativas) são:
a) \{b \vee d\}
b) \{\neg c \vee d \vee c\}
e) \{\neg b \vee d\}

Exercícios relacionados