Verificação 29/03/2012

   # # # # # # # # # # # # #
  # Verificação Automatica  #
  # Prof. Sérgio Campos     #
  # notasdogarcia.blog.com  #
   # # # # # # # # # # # # #

  Lembrando das últimas aulas, BDD era um método de verificação formal, vamos discutir como ele faz para provar a veracidade de um conjunto de expressões:

  BDD - Binary Decision Diagrams

  Binary Decision Three

    é uma arvore que caminha com chaves binárias (que representam verdadeiro ou falso para variaveis diferentes) e cujas folhas representam um booleano.

  Voce consegue modelar essas arvores para representar expressões lógicas.

  O problema dessas arvores é que elas crescem de forma exponencial. Mas da pra evitar um pouco isso.
  Essas arvores tem uma quantidade imensa de redundancia.

  Voce pode então verificar que se todos os filhos de um certo nó são 0 então é se chegar nesse nó temos resultado 0.
  E podemos também encontrar sub-arvores identicas, e elminar essas arvores sobresalentes.

  Economizando espaço.

CONCEITO:
  Um BDD pode ser descrito recursivamente como um nó com dois filhos que se ligam a outros 2 BDDs de forma não ciclica.
  E onde seguindo os nós da raiz às folhas as variáveis aparecem de forma ordenada.
  (essa na verdade é a OBDD, ou seja Ordenate BDD)

  Seja a arvore: AB + C (A e B ou C)

  a
  |\
  | \
  |  b
  | / \
  |/   \
  c     1
  |\
  | \
  0  1

  Todos os nós a direita implicam em nó verdadeiro.

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

  Canonical Form Property
  // Canonico significa que só há uma forma de escrever.

  Bryant foi quem provou que que essas arvores com certas restrições tornam-se canonicas.
  Qual a vantagem disso?

  Lembra que eu sugeri encontrar sub-arvores identicas e eliminar as sobressalentes?
  Encontrar arvores isomorficas é um problema NP-Completo
  Porém se a representação for canonica basta voce seguir a partir da raiz e comparar nó a nó se as transições estão iguais.
  E se torna um programa barato.

  O algoritmo pra isso caminha de baixo para cima verificando:

  existem terminais duplicados (esse passo é bem obvio =P)? junte eles.
  existem não terminais duplicados? junte eles.
  existe redundancia (com 0 ou 1 o negocio vai pro mesmo lugar)? remova o nó =P e pronto.

  Bem essas comparações são muito baratas, assim voce pode dizer que comparar duas expressões booleanas seria em ordem n emfunção do tamanho do BDD

  Parece que resolvemos um problema NP-Completo! =P

  Mas obviamente tem um problema. Tranformar uma expressão booleana em um BDD é uma operação cara,
  porque porque dependendo da ordem das variáveis nas expressões booleanas o tamanho do BDD gerado pode crescer exponencialmente.

  E tem outro problema

  Determinar a ordem ótima é um problema NP-Completo

  E pra completar, existem problemas bem comuns que sabe-se que tem um BDD de tamanho exponencial para qualquer ordem das variáveis! =P
  Um deles é a multiplicação de acordo com o professor.
  // Grande problema =/

  A boa noticia segundo o professor é que ele ainda não viu outro problema alem da multiplicação que não pudessem ser expresos na forma de um BDD.
  Pois existem euristicas muito boas para resolver a ordem das variáveis.

  Essas euristicas funcionam bem, porque nos problemas que normalmente lidamos que são criados por humanos,
  as variaveis tendem a estar em uma ordem boa e não ter muiitas possibilidades.

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

  Dynamic Variable Ordering.

  Se voce trocar duas variaveis adjacentes de lugar em um BDD, o efeito é local, então voce não precisa mudar o resto da arvore do BDD.

  Assim voce pode sair trocando de um em um as variáveis e cálculando o tamanho esperado da BDD (que é algo barato segundo o professor)
  Assim voce consegue escolher a posição de A que o negocio fica menor =]. É uma boa euristica já que a troca local de variáveis é barata.

  Depois voce r epete o processo com as demais variáveis e assim por diante =].

  // Fim da aula.