Algoritmo de Davis-Putnam
O Algoritmo de Davis-Putnam, criado por Martin Davis e Hilary Putnam, foi um dos pioneiros na área de checagem da satisfatibilidade de uma fórmula quando essa encontra-se na Forma Normal Conjuntiva (FNC). É uma forma de resolução em que cada variável é escolhida pelo fato de se poder resolver todas as cláusulas em que a mesma está contida na sua forma positiva com qualquer cláusula em que ela encontre-se em sua forma negada.
Funcionamento editar
Ao invés de procurar enumerar cada combinação possível de valorações para as variáveis, esse algoritmo utiliza técnicas de backtracking para reduzir o espaço de procura. A base do algoritmo é a seguinte: se um assinalamento parcial fizer uma cláusula ser avaliada para FALSO, esse assinalamento parcial não poderá ser parte de uma solução válida. O algoritmo procura identificar a não satisfatibilidade em um assinalamento parcial de forma que não haja necessidade de tentar outras variáveis ainda sem valor atribuído. Isso normalmente resulta em uma procura mais eficiente do que simplesmente enumerar cada uma das combinações possíveis de valoração. O algoritmo é recursivo e cria uma árvore de procura, atribuindo valores e dividindo o problema em problemas menores (Divisão e Conquista). O algoritmo funciona bem na média, chegando a resultados satisfatórios para alguns tipos de problemas, porém seu pior caso, como esperado, é exponencial.
Algoritmo editar
O algoritmo funciona como é mostrado a seguir:
- Para todas variáveis na fórmula
- Para todas cláusulas C contendo a variável e para todas cláusulas N contendo a negação da variável
- Resolva C e N e adicione o resultado à fórmula
- Remova de todas cláusulas originais a variável ou a negação da mesma
- Para todas cláusulas C contendo a variável e para todas cláusulas N contendo a negação da variável
Dois casos de parada:
- Um conjunto vazio de cláusulas é satisfatível
- Uma cláusula falsa é insatisfatível
Ideia do algoritmo editar
Em termos gerais a ideia do algoritmo é explicado como segue abaixo:
Considerando que:
- 0 = FALSE (falso)
- 1 = TRUE (verdadeiro)
1. Atribui-se 1 ou 0 para as variáveis que compõem pelo menos uma cláusula de uma única variável, de tal forma que essa cláusula seja 1;
2. Deve-se verificar se não há conflito, ou seja, se o valor da variável que torna uma cláusula verdadeira não deixa outra cláusula falsa;
3. Se ocorrer um conflito, o algoritmo deve ser interrompido, pois a fórmula não pode ser verdadeira;
4. Se não há conflito, as cláusulas com apenas uma variável que receberam o valor 1 são eliminadas da fórmula, pois o resultado não depende mais da mesma;
5. As cláusulas com mais de uma variável que possuem aquela variável que recebeu o valor 1 podem ser eliminadas caso não haja negação para a variável que possui valor 1;
6. Quando não existirem mais cláusulas com apenas uma variável, escolhe-se uma variável qualquer e atribui um valor qualquer, por exemplo 1, para ela;
7. Após a substituição da variável escolhida por 1, deve-se verificar novamente se existem cláusulas com apenas uma variável e também se não ocorreu conflito;
8. Se um conflito for encontrado, antes de terminar o processamento do algoritmo com falha, deve-se retornar o processamento até o ponto que a variável escolhida recebeu o valor 1 e atribuir agora o valor 0, ou seja, o valor que ainda não foi processado (Backtracking);
9. Verifica-se novamente se existem cláusulas com apenas uma variável e também se não ocorreu conflito;
10. Se um conflito for encontrado com o segundo valor da variável escolhida, deve-se terminar o processamento do algoritmo com falha, pois não existe valor dessa variável que satisfaça a fórmula;
11. Realiza-se esse procedimento até que todas as cláusulas possam ser eliminadas;
12. Se não foi encontrada nenhuma variável que gere falha no processamento do algoritmo, pode-se afirmar que a fórmula pode ser satisfeita, ou melhor, pode ter um resultado verdadeiro (igual a 1).
Exemplo editar
Seja a seguinte fórmula na forma normal conjuntiva:
Utilizando a regra de cláusulas unitárias, a heurística assume que vale , chegando a fórmula:
Ainda pela mesma regra, observamos que a cláusula contém e por isso eliminamos a cláusula ficando com:
Sabendo que eliminamos de chegando à fórmula:
Assumindo temos então recursivamente aplicando a regra da cláusula unitária, resolvemos o problema com o assinalamento e . Então dizemos que a fórmula é dita satisfeita.
Segue abaixo um esquema passo-a-passo do exemplo dado:
|
