Use DPLL para verificar se a fórmula abaixo é satisfazível:
Passo 1
Resumindo, queremos verificar se a seguinte fórmula em CNF é satisfazível usando o algoritmo DPLL:
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
ou
.
Passo 2
Procuramos literais puros (que aparecem só positivamente ou só negativamente).
-
aparece em e em . -
aparece em e em . -
aparece em e em .
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 e primeiro tentamos
Portanto aplicamos splitting. Escolhemos a variável
Passo 4
Com
, todas as cláusulas que contenham o literal
ficam satisfeitas e são removidas. As três cláusulas restantes são:
Passo 5
Na nova fórmula não há literais puros nem cláusulas unitárias, então fazemos splitting em
. Primeiro tentamos
Passo 6
Com
, a cláusula
reduz-se a
enquanto as outras duas ficam satisfeitas. Logo sobra a cláusula unitária
Aplicamos unit propagation definindo
enquanto as outras duas ficam satisfeitas. Logo sobra a cláusula unitária
Aplicamos unit propagation definindo
Passo 7
Atribuindo
, 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,