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 x, y, z. Queremos que:
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 x,y,z 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
(x \lor y \lor z).

Passo 3

A condição “no máximo uma é verdadeira” diz que nenhuma dupla pode ser simultaneamente verdadeira, gerando as cláusulas
(\lnot x \lor \lnot y),\quad (\lnot x \lor \lnot z),\quad (\lnot y \lor \lnot z).

Passo 4

Unindo tudo, a fórmula em CNF fica
(x \lor y \lor z) \;\land\; (\lnot x \lor \lnot y)\;\land\; (\lnot x \lor \lnot z)\;\land\; (\lnot y \lor \lnot z).

Passo 5

O algoritmo DPLL procede assim:
  1. Aplica propagação unitária (unit propagation) e elimina literais puros (pure literal elimination).
  2. 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 x. Tentamos x = \text{true}.

Passo 7

Com x=\text{true}:
  • (x \lor y \lor z) fica satisfeita e é descartada.
  • (\lnot x \lor \lnot y) vira unitária (\lnot y), logo y=\text{false}.
  • (\lnot x \lor \lnot z) vira unitária (\lnot z), logo z=\text{false}.
  • A última cláusula (\lnot y \lor \lnot z) fica (\text{true}\lor\text{true}), satisfeita.
    Todas as cláusulas são satisfeitas, logo encontramos uma solução.

Resposta

A fórmula em CNF é
(x \lor y \lor z)\;\land\;(\lnot x \lor \lnot y)\;\land\;(\lnot x \lor \lnot z)\;\land\;(\lnot y \lor \lnot z).
Uma atribuição que satisfaz pelo DPLL é x=\text{true},\;y=\text{false},\;z=\text{false}.

Exercícios relacionados