Crie uma fórmula em CNF que representa o problema do exemplo abaixo e resolva-o usando o algoritmo DPLL:
Suponha que temos três variáveis booleanas
. Queremos que:
Pelo menos uma das variáveis seja verdadeira.
No máximo uma das variáveis seja verdadeira.
Pelo menos uma das variáveis seja verdadeira.
No máximo uma das variáveis seja verdadeira.
Passo 1
O enunciado apresenta três variáveis booleanas
e impõe duas condições: “pelo menos uma é verdadeira” e “no máximo uma é verdadeira”. O conteúdo é tradução para forma normal conjuntiva (CNF) e aplicação do algoritmo DPLL para encontrar uma atribuição satisfatível.
Passo 2
A condição “pelo menos uma é verdadeira” gera a cláusula
Passo 3
A condição “no máximo uma é verdadeira” diz que nenhuma dupla pode ser simultaneamente verdadeira, gerando as cláusulas
Passo 4
Unindo tudo, a fórmula em CNF fica
Passo 5
O algoritmo DPLL procede assim:
- Aplica propagação unitária (unit propagation) e elimina literais puros (pure literal elimination).
- Se não restar cláusula unitária ou puro, escolhe um literal não atribuído (splitting), testa um valor, e recursa.
Passo 6
Inicialmente não há cláusulas unitárias nem literais puros, então escolhemos o literal
. Tentamos
.
Passo 7
Com
:
-
fica satisfeita e é descartada. -
vira unitária , logo . -
vira unitária , logo . - A última cláusula
fica , satisfeita.
Todas as cláusulas são satisfeitas, logo encontramos uma solução.
Resposta
A fórmula em CNF é
Uma atribuição que satisfaz pelo DPLL é