Utilize backtracking para determinar se as fórmulas \{\neg \mathbf{p} \vee \mathbf{q}, \mathbf{r} \vee \mathbf{p}\} são satisfazíveis. Enumere todos os passos que devem ser realizados.

Passo 1

O enunciado apresenta o conjunto de cláusulas proposicionais \{\neg p \vee q,\;r \vee p\}
e pede para determinar, por busca com backtracking (algoritmo DPLL sem heurísticas avançadas), se há uma atribuição de verdade que satisfaça todas as cláusulas.

Passo 2

Escolhemos a próxima variável livre, p, e tentamos primeiro a atribuição
p = \top.
Substituímos em cada cláusula:
  • \neg p \vee q vira \neg \top \vee q = q,
  • r \vee p vira r \vee \top = \top.
    Obtemos o conjunto simplificado
F_1 = \{\,q,\;\top\}.

Passo 3

Em F_1 aparece a cláusula unitária q. Usamos unit propagation e fixamos
q = \top.
Substituindo, ambas as cláusulas em F_1 tornam-se verdadeiras: \{q\} \to \{\top\} e já tínhamos uma \top. Logo não resta nenhuma cláusula não satisfeita.

Passo 4

Não há conflito (nenhuma cláusula vazia) e não há cláusulas pendentes. Portanto encontramos uma atribuição parcial consistente:
p = \top,\quad q = \top.
Como só restava r sem atribuição e não há cláusulas que o contenham sem já estarem satisfeitas, podemos dar a qualquer valor, por exemplo
r = \bot.

Passo 5

Como foi encontrada uma atribuição que satisfaz todas as cláusulas, o algoritmo termina sem precisar voltar (backtrack) para p = \bot.

Resposta

O conjunto de cláusulas é satisfatível. Um modelo é
p = \top,\quad q = \top,\quad r = \bot.

Exercícios relacionados