Suponha que tem o seguinte conjunto de cláusulas: CNF={{1, -2}, {1, 3}, {-1, -2, -3}, {-1, -2, -3}, {-1, 2, 3}, {-1, -2, 3}} Aplique o DPLL, de modo a verificar se o conjunto de cláusulas pode ser satisfeito.

Resumo da Resposta

O conjunto de cláusulas fornecido é satisfatório, pois existe uma valoração lógica (modelo) que torna todas as cláusulas verdadeiras simultaneamente. Uma solução possível é atribuir Falso à variável 1, Falso à variável 2 e Verdadeiro à variável 3.

Análise Detalhada do Algoritmo DPLL

O algoritmo DPLL (Davis-Putnam-Logemann-Loveland) é um procedimento recursivo usado para decidir a satisfatibilidade de fórmulas na Forma Normal Conjuntiva (CNF). Ele combina eliminação de literais puros, propagação de unidade e busca em profundidade com retrocesso (backtracking).

1. Estado Inicial

Primeiro, listamos as cláusulas fornecidas no enunciado:

• C_1 = \{1, -2\}
• C_2 = \{1, 3\}
• C_3 = \{-1, -2, -3\}
• C_4 = \{-1, 2, -3\}
• C_5 = \{-1, 2, 3\}
• C_6 = \{-1, -2, 3\}

Não existem literais puros inicialmente (nenhuma variável aparece apenas com polaridade positiva ou apenas negativa em todas as cláusulas). Logo, iniciamos com a etapa de Ramificação (Splitting). Escolhemos a variável $1$ como ponto de partida.

2. Ramificação 1: Assumindo $1 = \text{Verdadeiro}$

Se definimos $1 = \text{True}$:

• As cláusulas contendo $1$ são satisfeitas e removidas: C_1 e C_2 desaparecem.
• O literal -1 torna-se Falso e é removido das cláusulas restantes (C_3, C_4, C_5, C_6).

As cláusulas simplificadas ficam:

• C'_3 = \{-2, -3\}
• C'_4 = \{2, -3\}
• C'_5 = \{2, 3\}
• C'_6 = \{-2, 3\}

Agora fazemos outra ramificação sobre a variável $3$.

• Caso 2.1: $3 = \text{Verdadeiro}$
• C'_5 e C'_6 são satisfeitas.
• C'_3 vira \{-2\} (Unidade \Rightarrow 2 = \text{False}).
• C'_4 vira \{2\} (Unidade \Rightarrow 2 = \text{True}).
• Contradição: $2$ não pode ser verdadeiro e falso ao mesmo tempo.
• Caso 2.2: $3 = \text{Falso}$
• C'_3 e C'_4 são satisfeitas.
• C'_5 vira \{2\} (Unidade \Rightarrow 2 = \text{True}).
• C'_6 vira \{-2\} (Unidade \Rightarrow 2 = \text{False}).
• Contradição: Novamente, conflito entre $2$ e -2.

Como ambos os raios falharam, assumimos $1 = \text{Verdadeiro}$ leva ao Insatisfatório. Devemos fazer backtracking.

3. Ramificação 2: Assumindo $1 = \text{Falso}$

Se definimos $1 = \text{False}$ (logo -1 = \text{True}):

• Todas as cláusulas que contêm -1 são automaticamente satisfeitas e removidas: C_3, C_4, C_5, C_6.
• Restam apenas as cláusulas C_1 e C_2. Como $1$ é Falso, removemos o literal $1$ delas.

As cláusulas restantes tornam-se:

• C''_1 = \{-2\}
• C''_2 = \{3\}

Aplicando Propagação de Unidade:

1. De C''_1 = \{-2\}, inferimos que $2$ deve ser Falso.
2. De C''_2 = \{3\}, inferimos que $3$ deve ser Verdadeiro.

4. Verificação Final

Testamos a valoração encontrada: \{1: \text{False}, 2: \text{False}, 3: \text{True}\}.

Todas as cláusulas foram satisfeitas sem conflitos.

Conclusão

O algoritmo DPLL conclui que o conjunto de cláusulas é satisfatório. A existência de pelo menos uma valoração que torna todas as cláusulas verdadeiras confirma essa conclusão.