Entender a propagação de unidades do algoritmo DPLL

O que é a Propagação de Unidades?

A propagação de unidades é uma técnica de simplificação usada no algoritmo DPLL para fórmulas em Forma Normal Conjuntiva (CNF). Ela identifica e resolve cláusulas que contêm apenas um literal (chamadas de cláusulas unitárias), atribuindo um valor verdadeiro a essa variável.

Como Funciona o Processo?

1. Identificação: Procure por cláusulas com apenas um literal. Por exemplo, a cláusula {-2} é unitária.
2. Atribuição: Atribua o valor verdadeiro ao literal. Se a cláusula é {-2}, então x2 = falso (ou ¬x2 = verdadeiro).
3. Simplificação: Remova todas as cláusulas que contêm o literal atribuído como verdadeiro (pois a cláusula já está satisfeita) e remova o literal oposto das cláusulas restantes (pois ele é falso).
4. Repetição: Continue o processo até não haver mais cláusulas unitárias.

Aplicação ao Exemplo Anterior

No conjunto de cláusulas fornecido:

• A cláusula C3 = {-2} é unitária → atribui x2 = falso.
• Isso simplifica as outras cláusulas: remove C3 e o literal -2 de C6 (que se torna {-3}).
• Agora, C6 se torna unitária ({-3}) → atribui x3 = falso.
• Mas a cláusula C5 = {2, 3} exige que x2 = verdadeiro ou x3 = verdadeiro. Como x2 = falso e x3 = falso, temos uma contradição.

Análise

• Cláusulas unitárias são essenciais para reduzir o espaço de busca.
• A propagação de unidades pode revelar insatisfatibilidade rapidamente, como no exemplo.
• Se não houver contradição, o processo continua até que todas as cláusulas sejam satisfeitas ou reste apenas cláusulas não unitárias para divisão (backtracking).

Conclusão

A propagação de unidades é uma etapa gulosa e eficiente do DPLL que simplifica a fórmula CNF ao atribuir valores a variáveis críticas. No exemplo, ela expôs a insatisfatibilidade ao forçar x2 = falso e x3 = falso, conflitando com a cláusula C5.