Esta é uma pré-visualização de arquivo. Entre para ver o arquivo original
Clique para editar o estilo do título mestre Clique para editar o estilo do subtítulo mestre * * * Lógica Proposicional SAT e Custo Computacional * * * Conjuntos FOR: conjunto das fórmulas SAT: conjunto das fórmulas satisfazíveis INSAT: conjunto das fórmulas insatisfazíveis TAUT: conjunto das tautologias REFUT: conjunto das fórmulas refutáveis Refutável é toda fórmula H tal que exista pelo menos uma interpretação I[H]=F * * * Lema de pertinência Para H € FOR: H € SAT D H € INSAT H € INSAT D (H) € TAUT H € SAT D (H) € TAUT H € REFUT D H € TAUT H € REFUT D (H) € INSAT * * * Lema entre os conjuntos SAT, INSAT, TAUT, REFUT FOR TAUT SAT INSAT REFUT TAUT I REFUT = {} INSAT I SAT = {} SAT U REFUT = FOR TAUT U INSAT FOR SAT I REFUT = {} * * * O problema SAT Dada uma fórmula proposicional = (a b) ( a b c) Determinar se é satisfazível Problema de decisão Para n símbolos proposicionais, são necessárias 2n linhas numa tabela verdade e 2m+1 colunas * * * Aplicações Um “resolvedor de SAT” é a principal ferramenta computacional para: Em Inteligência Artificial: Programação em lógica Provadores de teoremas Em Projeto Automático de Componentes Eletrônicos: Teste e Verificação Síntese Escalonamento Planejamento … * * * Custo Computacional O custo (determinístico) de SAT é dito exponencial Não-determinísticamente, o custo de SAT cai para cerca de 2m+1 2m+1 é o número de sub-proposições, por indução m= no. de conectivos da fórmula Custo não-deterministicamente polinomial (NP) Testam-se apenas algumas linhas da tabela O no. de sub-fórmulas é sempre até 2 vezes o número de conectivos mais 1 * * * Complexidade Computacional Criação da classe de problemas NP-Completo S. A. Cook, The complexity of theorem proving procedures, Proceedings, Third Annual ACM Symp. on the Theory of Computing,1971, 151-158 Abordagem mais simples: B. Hayes, Can’t get no satisfaction, American Scientist, Vol. 85, nr. 2, Mar-Apr 1997, 108-112 * * * Complexidade Computacional (cont.) Algoritmos deterministicamente polinomiais: logarítmico, linear quadrático, cúbico (log n, n, n**2, n**3, …, n**500,…) Algoritmos exponenciais (ou não-deterministicamente polinomiais): 2**n,n**n,n**log n Algoritmos exponenciais são mais lentos que os polinomiais para valores altos de n Polinomiais são preferíveis! * * * Complexidade e SAT 1-SAT:linear (um literal por subfórmula) 2-SAT: linear (com fases) (x11 OR x12) AND (x21 OR x22) AND (x31 OR x32) AND… 3-SAT: NP-completo (x11 OR x12 OR x13) AND (x21 OR x22 OR x23) AND (x31 OR x32 OR x33) AND ... O problema são os conflitos, que diminuem a satisfabilidade! Não existe um algoritmo polinomial para todas as instâncias do problema SAT, a não ser que P = NP Vira deterministicamente polinomial quando as sentenças viram 2-SAT (no máximo 2 símbolos proposicionais por fórmula) Cláusula de Horn – 1-SAT (No máximo 1 símbolo proposicional positivo em todas as sub-fórmulas)