Use DPLL para verificar se a fórmula abaixo é satisfazível:
(\neg p \vee \neg q \vee r) \wedge(\neg p \vee q \vee \neg r) \wedge(\neg p \vee q \vee r) \wedge(p \vee \neg q \vee r) \wedge(p \vee q \vee r)

Passo 1

Resumindo, queremos verificar se a seguinte fórmula em CNF é satisfazível usando o algoritmo DPLL:
(\neg p \vee \neg q \vee r)\wedge(\neg p \vee q \vee \neg r)\wedge(\neg p \vee q \vee r)\wedge(p \vee \neg q \vee r)\wedge(p \vee q \vee r).
O DPLL faz, nessa ordem: eliminação de literais puros, propagação de unidades e, se necessário, divisão (splitting) escolhendo uma variável e atribuindo-lhe \text{true} ou \text{false}.

Passo 2

Procuramos literais puros (que aparecem só positivamente ou só negativamente).
  • p aparece em \neg p e em p.
  • q aparece em \neg q e em q.
  • r aparece em \neg r e em r.
    Não há literais puros, então não eliminamos nada.

Passo 3

Procuramos cláusulas unitárias (tamanho 1): não há.
Portanto aplicamos splitting. Escolhemos a variável p e primeiro tentamos
p = \text{true}.

Passo 4

Com p = \text{true}, todas as cláusulas que contenham o literal p ficam satisfeitas e são removidas. As três cláusulas restantes são:
(\neg q \vee r),\quad (q \vee \neg r),\quad (q \vee r).

Passo 5

Na nova fórmula não há literais puros nem cláusulas unitárias, então fazemos splitting em q. Primeiro tentamos
q = \text{true}.

Passo 6

Com q = \text{true}, a cláusula \neg q \vee r reduz-se a r,
enquanto as outras duas ficam satisfeitas. Logo sobra a cláusula unitária r.
Aplicamos unit propagation definindo
r = \text{true}.

Passo 7

Atribuindo r = \text{true}, todas as cláusulas se tornam satisfeitas. Encontramos assim um modelo que satisfaz toda a fórmula.

Resposta

A fórmula é satisfazível. Por exemplo,
p = \text{true},\quad q = \text{true},\quad r = \text{true}.

Exercícios relacionados