Utilize backtracking para determinar se as fórmulas
são satisfazíveis. Enumere todos os passos que devem ser realizados.
Passo 1
O enunciado apresenta o conjunto de cláusulas proposicionais
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.
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,
, e tentamos primeiro a atribuição
Substituímos em cada cláusula:
-
vira , -
vira .
Obtemos o conjunto simplificado
Passo 3
Em
aparece a cláusula unitária
. Usamos unit propagation e fixamos
Substituindo, ambas as cláusulas em
tornam-se verdadeiras:
e já tínhamos uma
. 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:
Como só restava
sem atribuição e não há cláusulas que o contenham sem já estarem satisfeitas, podemos dar a qualquer valor, por exemplo
Passo 5
Como foi encontrada uma atribuição que satisfaz todas as cláusulas, o algoritmo termina sem precisar voltar (backtrack) para
.
Resposta
O conjunto de cláusulas é satisfatível. Um modelo é