Autores

1963
242,837
1964
242,837

Informações:

Publicações do PESC

Título
Avaliação do Problema de Ordenação em Diagramas de Decisão Binária
Linha de pesquisa
Algoritmos e Combinatória
Tipo de publicação
Dissertação de Mestrado
Número de registro
Data da defesa
21/2/2001
Resumo

Diagramas de Decisão Binária (BDDs) têm se mostrado uma ferramenta essencial no processo de verificação automática de sistemas. A solução de uma grande classe de problemas de interesse prático recai na utilização de BDDs. Quando é imposta uma ordenação às variáveis que descrevem o sistema, o BDD passa a ser denominado BDD ordenado (OBDD). Os OBDDs têm como característica essencial o fato de representar unicamente cada função tornando viável a verificação de sistemas.

O tamanho de um OBDD pode variar muito de acordo com a ordenação de suas variáveis. Encontrar uma boa ordenação de variáveis é fundamental para manipulação de funções Booleanas. Nosso estudo é baseado em informações sobre a topologia de circuitos combinacionais para se obter um limite superior para o tamanho de um OBDD. A partir da descrição do circuito é construído um grafo de representação do circuito. A estimativa do tamanho do OBDD é feita sem que seja necessária a sua construção. Dada uma ordenação qualquer, estima-se através de cortes no grafo de representação do circuito, um limite superior para cada nível do OBDD. Utilizamos esta estimativa juntamente com um método de reordenação de variáveis (sifting), de modo a obter uma boa ordenação que viabilize a aplicação de métodos pré-existentes de reordenação de variáveis.

Além disso, utilizamos esta nova ordenação para verificar a eficácia deste método para estimar o tamanho do OBDD resultante. Os resultados mostram que para a maioria dos exemplos utilizados a ordenação sugerida com a utilização da estimativa, reduz o tamanho dos OBDDs. Em alguns casos esta redução é bastante significativa.

Abstract

Binary Decision Diagrams (BDDs) play an important rol1 in Lhe process of automatic system verification. The solution to a large class of practical problems involves the use of BDDs. When an order is imposed on the variables that describe the system, the BDD is called an ordered BDD (OBDD). An essential property of OBDDs is the fact that they uniquily represent each function, thus enabling the systems verification process. The size of an OBDD can vary a lot according to the order imposed on its variables. It becomes crucial to find a good ordering for an OBDD in order to manipulate Boolean functions.

Our study is based on topological information of combinational circuits, which is used to obtain an upper bound for the size of an OBDD. We map the circuit onto a graph whose nodes have a one-to-one correspondance with the gates of the circuit. Cuts on this circuit are used to obtain an estimate for the size of the OBDD without requiring the OBDD to be actually built.

This estimate can be used along with a reordering technique in order to obtain good initial orders (without ever constructing the OBDD), thus enabling the application of pre-exhisting variable ordering methods.

This new ordering is also compared to the initial order given, in order to assess the goodness of our estimation method. The experimental results show that in most cases the proposed ordering results in smaller OBDDs. n some cases it results in a more pronounced reduction in size.

Arquivo
Topo