Proposta de um Algoritmo Polinomial para 3-SAT

-----------------------------------------------------------------------------

Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------

Título: Proposta de um Algoritmo Polinomial para 3-SAT
Palestrante: Maria Ângela Weiss
Data e Local: dia 21.05.07 às 16:00 hs
Local: Sala 242 - Bloco A - IME - USP

Resumo:


Desenvolvemos um método de tableau que consiste em um algoritmo baseado no classico KE-tableau. Nesse algoritmo, dado como input uma fórmula 3-SAT $\Psi$, temos como output, primeiramente um arranjo de literais prefixadas de $\Psi$ onde aparecem, como linhas verticais do output, apenas posssíveis ramos fechados de um tableau onde a regra de Bivalência foi aplicada nessas literais prefixadas.

Apresentamos também um algoritmo de resolução para decidir se esses arranjos de fato representam todos os possíveis ramos obtidos por Bivalência são fechados ou não, gerando como resposta $\Psi$ é válida ou $\Psi$ não é válida.

Esses dois algoritmos -- de construção dos arranjos e resolução -- provaram ser polinomiais e, no estágio de nossa pesquisa convidamos todos interesados nesse assunto a discutir, opinar e apontar possíveis falhas no processo.


Todos são benvindos