Lógica Proposicional SAT e Custo Computacional O problema SAT Dada uma fórmula proposicional Determinar se é satisfazível = (a b) ( a b c) Problema de decisão Para n símbolos proposicionais, são necessárias 2n linhas numa tabela verdade e 2m+1 colunas a 0 0 b c 0 1 b 1 0 c 1 0 1 c 1 0 c 1 0 1 Aplicações Um “resolvedor de SAT” é a principal ferramenta computacional para: Em Inteligência Artificial: Em Projeto Automático de Componentes Eletrônicos: Programação em lógica Provadores de teoremas 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 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ãodeterministicamente 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) Resolvedores de SAT Davis-Puttnan DPLL Resolução Todas elas exigem que a fórmula esteja na forma normal conjuntiva Forma normal conjuntiva Uma fórmula está na forma normal conjuntiva (fnc ou CNF, em inglês) se é uma conjunção de disjunções de literais F é da forma F1 ^ F2 ^ ... ^ Fn, onde Fi é uma disjunção (da forma A1 v A2 v ... v An ) e Ai é um literal Ex: G=(PvQ) ^ (RvQvP) ^ (PvS) Algoritmos para obter CNF usando leis (repetidamente) 1 -Leis de eliminação 2 -Lei da negação (H) H 2 -Leis de De Morgan PQ = (PvQ) P Q = (P Q)^(Q P) (PvQ) = P ^ Q (P^Q) = P v Q 3 -Leis distributivas: F v (G^H) = (FvG) ^ (FvH) F ^ (GvH) = (F^G) v (F^H) (não usada para CNF) Notação na forma de conjuntos H=(PvQvR)^(PvQ)^(PvP) Representação na forma de conjuntos: H={[P,Q,R],[P,Q],[P]} Note que (PvQvR) = [P,Q,R] (PvP)=[P] Não é necessário representar duplicidade na forma de conjuntos Cláusulas e literais complementares Cláusula em lógica proposicional é uma disjunção de literais Usando a notação de conjuntos: C1=[P,Q,R], C2=[P,Q], C3=[P] Dois literais são complementares quando um é a negação do outro Resolvente de 2 cláusulas Supondo 2 cláusulas C1=[A1,..., An] e C2=[B1, ..., Bn], com literais complementares A, um conjunto de literais em C1, tal que -A, um conjunto de literais complementares a A, estão em C2 Resolvente de C1 e C2: Res(C1,C2)=(C1-A)U(C2- -A) Res(C1,C2) pode ser {} Resolvente vazio ou trivial Exemplo de resolvente C1=[P,Q,R] e C2=[P,R] Res (C1,C2) = [Q,R], que também é uma cláusula D1=[P,Q] e D2=[P,Q] Res (D1,D2) = {}, que também é uma cláusula Idéia básica em todos os algoritmos: Resolução Resolução de um par de cláusulas com exatamente UMA variável incompatível a + b + c’ + f g + h’ + c + f a + b + g + h’ + f E se tivermos mais de uma variável incompatível? Algoritmo de Davis Putnam M .Davis, H. Putnam, “A computing procedure for quantification theory", J. of ACM, Vol. 7, pp. 201-214, 1960 Escolher uma variável a cada iteração para resolução até elas acabarem INSAT se aparecer a cláusula vazia Descarta as cláusulas resolvidas depois de cada iteração (a + b + c)(b + c’ + f’)(b’ + e) (a + b) (a + b’) (a’ + c)(a’ + c’) (a + c + e)(c’ + e + f’) (a) (a’ + c)(a’ + c’) (a + e + f’) (c)(c’) SAT () INSAT Pode explodir a memória!!! Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 Decisão Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 b 0 Decisão Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 b 0 c 0 Decisão Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 b 0 c 0 a=0 (a + c + d) d=1 Conflict! Grafo de Implicação c=0 (a + c + d’) d=0 Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 b 0 c 0 a=0 (a + c + d) d=1 Conflict! Grafo de Implicação c=0 (a + c + d’) d=0 Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 b 0 c 0 Backtrack Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 b 0 c 0 1 Decisão Forçada a=0 (a + c’ + d) d=1 Conflict! c=1 (a + c’ + d’) d=0 Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 b 0 Backtrack c 0 1 Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 b 0 c 0 1 1 Decisão Forçada Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 b 0 1 c 0 c 1 0 a=0 Decisão (a + c’ + d) d=1 Conflict! c=0 (a + c’ + d’) d=0 Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 b 0 1 c 0 c 1 0 Backtrack Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 b 0 1 c 0 c 1 0 a=0 1 Decisão Forçada (a + c’ + d) d=1 Conflict! c=1 (a + c’ + d’) d=0 Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 b 0 1 c 0 c 1 0 1 Backtrack Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 1 b 0 1 c 0 c 1 0 1 Decisão Forçada Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 1 b 0 b c 0 0 Decisão 1 c 1 0 1 Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 1 b 0 b 1 c 0 0 c 1 a=1 0 1 (a’ + b + c) c=1 Conflito! b=0 (a’ + b + c’) c=0 Algoritmo DPLL (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) a 0 1 b 0 b 1 c 0 0 c 1 0 1 Backtrack Algoritmo DPLL a (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) 0 1 b 0 b 1 c 0 a=1 b=1 0 c 1 (a’ + b’ + c) 0 c=1 1 1 Decisão Forçada Algoritmo DPLL a (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) 0 1 b 0 b 1 c 0 a=1 b=1 0 1 c 1 (a’ + b’ + c) 0 c=1 1 (b’ + c’ + d) d=1 Algoritmo DPLL a (a’ + b + c) (a + c + d) (a + c + d’) (a + c’ + d) (a + c’ + d’) (b’ + c’ + d) (a’ + b + c’) (a’ + b’ + c) 0 1 b 0 b 1 c 0 a=1 b=1 0 1 SAT c 1 (a’ + b’ + c) 0 c=1 1 (b’ + c’ + d) d=1 Análise de DPLL e assorted… Podem ser usados para provar tanto satisfatibilidade quanto insatisfatibilidade Mas DPLL não faz busca exaustiva, então não prova insatisfatibilidade (e portanto conseqüência lógica) WalkSAT (método incompleto): Estado Inicial: sorteia valorações de variáveis pré-ordenadas Operador de busca: Pega uma cláusula ainda insatisfeita e um literal nela Sorteia uma valoração pro literal A cada passo, escolhe aleatoriamente entre as seguintes estratégias para pegar um literal: Pega o literal cujo sorteio resulta na maior redução no número de cláusulas insatisfeitas Pega um literal aleatório Métodos de Busca (GSAT, WSAT) Cost Local Minima Global minimum Solution Space Com Lógica de Predicados, o método mais popular é a resolução Prova por resolução Método por refutação Dadas uma fórmula H e Hc, a forma clausal associada a H Uma Prova de H por resolução é uma expansão fechada sobre Hc H é um teorema do sistema de resolução Exemplo de Prova por resolução H=((P1vP2vP3)^(P1P4)^(P2P4)^ (P3P4)) P4 Determinar Hc associada a H Hc=(((P1vP2vP3)^(P1P4)^(P2P4)^ (P3P4)) P4)) =(((P1vP2vP3)^(P1P4)^(P2P4)^(P3P4)) vP4) =(P1vP2vP3)^(P1vP4)^(P2vP4)^(P3vP4)^ P4 ={[P1,P2,P3],[P1,P4],[P2,P4],[P3,P4],[P4]} Agora, é só fazer a expansão por resolução! Exemplo de Prova por resolução (cont.) 1. [P1,P2,P3] 2. [P1,P4] 3. [P2,P4] 4. [P3,P4] 5. [P4] 6. [P2,P3,P4] 7. [P3,P4] 8. [P4] 9. {} Res(1,2) Res(3,6) Res(4,7) Res(5,8) Lógica de Predicados Sintaxe Alfabeto da Lógica de Predicados Símbolos de pontuação: (,) Símbolos de verdade: false, true Conjunto enumerável de símbolos para variáveis: x, y, z, w, x1, y1, x2, z2... Conjunto enumerável de símbolos para funções: f, g, h, f1, g1, f2, g2... Conjunto enumerável de símbolos para predicados: p, q, r, s, p1, q1, p2, q2... Conectivos proposicionais: ,v, , Termos São construídos a partir destas regras: Constantes e variáveis são termos (representam objetos) Se t1, t2, ..., tn são termos f é um símbolo de função n-ária, então f(t1, t2, ..., tn) também é um termo Exemplos de termos x, a (constante, função zero-ária) f(x,a) se e somente se f é binária g(y, f(x,a), c) se e somente se g é ternária +(9,10), -(9,5) interpretados como 10+9, 9-5 Notação polonesa h(x,y,z), considerada implicitamente como ternária Átomos São construídos a partir destas regras: O símbolo de verdade false é um átomo Se t1, t2, ..., tn são termos p é um símbolo de predicado n-ário então p(t1, t2, ..., tn) é um átomo Exemplos de átomos P (símbolo proposicional) Predicado zero-ário) p(f(x,a),x) se e somente se p é binário q(x,y,z) considerado implicitamente como ternário Ex: >(9,10), =(9,+(5,4)) interpretados como 10>9, 9=5+4 Interpretados como T Note os abusos de linguagem > e = são predicados + e – são funções Fórmulas São construídos a partir destas regras: Todo átomo é uma fórmula da Lógica de Predicados Se H é fórmula então (H) também é Se H e G são fórmulas, então (HvG) também é Se H é fórmula e x variável, então ((x)H) e ((x)H) são fórmulas Construção de fórmulas Átomos p(x), R e false ((p(x)) v R) Que equivale a (p(x) R) também fórmula ((x) p(x) R) Expressão = termo v fórmula Correspondência entre quantificadores ((x)H)= ((z)(H)) ((x)H)= ((z)(H))