Problema da Satisfatibilidade Booleana

EscoEscola de Engenharia Elétrica Mecânica e de Computação - EMC             Universidade Federal de Goiás - UFG[pic 1]

Solucionando o Problema da Satisfabilidade Booleana por Meio de Algoritmo Genético

Alunos:   

Henrique Santos Dias -124349

Igor Ferreira da Silva Nunes -124350

Welton Aristides Silva -124368

Professor:

Msc. Leonardo Afonso Amorim

Disciplina: 

Inteligência Computacional

Sumário

1.Introdução        

2.Procedimentos        

2.1 Implementação Polinomial        

2.2 Implementação Utilizando Algorítimo Genético        

3.Resultados Obtidos        

4.Conclusão        

5.Referências        

Solucionando o Problema da Satisfabilidade Booleana por Meio de Algorítimo Genético

Henrique Santos Dias, Igor Ferreira Nunes da Silva e Welton Aristides Silva, EMC, UFG

Resumo—Exploramos a resolução de problemas 3-Sat complexos, confrontando o desempenho que um algoritimo genético obteve em relação à busca exaustiva pela solução e, feito isto, discutimos detalhes de como o algoritmo genético foi construído e como sua lógica de funcionamento pode contribuir para otimizar a solução desse tipo de problema.

Palavras Chave—Satisfabilidade Booleana, Algoritimos Genéticos, NP-completo, NP-difícil, Computação Evolutiva, Busca Exaustiva.

————————————————

• Na ocasião desta produção, os autores cursam o 8° período do curso de graduação em Engenharia de Computação da Escola de Engenharia Elétrica, Mecânica e de Computação - Universidade Federal de Goiás
• Este artigo é parte do estudo de algoritimos genéticos, da disciplina de Inteligência Computacional, sendo que as aulas são ministradas e o artigo orientado pelo professor msc. Leonardo Afonso Amorim, do Instituto de Informática – Universidade Federal de Goiás  

——————————   ◆   ——————————

1        Introdução

N

a teoria da complexidade computacional, o problema de satisfatibilidade booleana (SAT) ­ analisado por Stephen Cook em 1971 ­ foi o primeiro problema identificado como pertencente à classe de complexidade NP­completo. Ele consiste em verificar se existe pelo menos uma atribuição de valores para um conjunto de variáveis de uma fórmula booleana na forma normal conjuntiva (FNC) no formato 3­SAT, onde cada cláusula é composta por exatamente 3 literais, tal que tornem a fórmula verdadeira:1

Exemplo:

(p1 OU p2 OU ¬p3) E (¬p1 OU p2 OU p3) E (¬p1 OU ¬p2   OU p3) E (p1 OU ¬p3 OU p4)

Nesse Contexto, algoritmos genéticos (que processam estruturas representativas para o valor dos literais de uma expressão, e medem a qualidade dessas estruturas baseados em uma rotina que encara essas estruturas como valores numéricos e as aplica em uma função matemática)2 podem ser utilizados como uma abordagem promissora na tentativa de resolver o problema heuristicamente  mas Cook também havia mostrado que um problema 3-SAT também é um problema NP-difícil e portanto algoritmos genéticos também levarão tempo exponencial para chegar à solução.3 

Além disso, outro aspecto que podemos considerar do problema da satisfatibilidade booleana é que, frequentemente, podemos encontrar literais peculiares na expressão cujo valor impactam a solução final de maneira mais incisiva: se um literal p1 aparece uma única vez na expressão pode-se fixar seu valor de forma a tornar a cláusula inteira satisfazível, podemos levar isso em consideração como métrica para escolher os genes de uma população inicial que tem maior possibilidade de ser a solução final,4 apesar de outros trabalhos onde a aleatoriedade da população inicial contribuiu para otimizar o algoritmo.5 

Este trabalho estará organizado da seguinte forma: Na Secção 2 apresentaremos as características (estruturas de dados, rotinas, e detalhes, problemas que possam ter ocorrido durante as implementações, e a expectativa de como deverão se comportar) das duas formas como o problema foi abordado:

• Busca exaustiva pela resposta de expressões 3-SAT que não utiliza nada da computação evolutiva;
• E Um programa que utiliza uma heurística para definir uma boa população inicial e depois utiliza técnicas elementares de algoritmos genéticos para a mesma finalidade.

Posteriormente, na secção 3, publicaremos os resultados empíricos de cada abordagem, analisando e confrontando com sua própria expectativa, cada uma delas separadamente, e uma com a outra.

Feito isto, a secção 4 consistirá em extrapolar as comparações para outros trabalhos, já consagrados na literatura, procurando entender as diferenças entre nossos resultados e o de outros autores.

Finalmente, constarão na secção 6: conclusão e possibilidades de trabalho futuro.

2.Procedimentos

Abordamos o problema das duas diferentes formas utilizando a linguagem JAVA. As tecnologias utilizadas para implementação de nossas abordagens foram:

-IDE Eclipse para desenvolvedores Java Web. Versão 4.5.1

-Java Virtual Machine Versão 8, Atualização 65

-Sistema Operacional Windows 7

Seja uma expressão no formato 3-Sat, podemos expressar as soluções utilizando cadeias de caracteres (constituídas de zeros e uns em sequência), convencionamos que cada caracter corresponde a um símbolo da expressão, na ordem em que foi sequenciada e desta maneira: 1 significa verdadeira para o símbolo, em toda a expressão e 0 falso.

...