Binary Decision Diagrams for sequences: definitions, properties and algorithms

Binary Decision Diagrams (BDDs) are a particular kind of graph for representing boolean functions. In particular they are rooted directed acyclic graphs, where every node represent a binary decision, or equivalently a branch on a certain boolean variable. There is a wide range of problems where BDDs are suitable because of what is called symbolic analysis. It’s possible in fact to encode the parameters of a system with boolean variables, and in general to encode a problem with a boolean function. Many flavours of decision diagrams exist in the literature. One of them, the Sequence BDD, has been used recently for representing sets of strings, with interesting results. The study of these kind of BDDs led to the discovery of new algorithms, mainly conceived for their reduction, that have been studied both theoretically and experimentally. In particular for this last purpose a small BDD package was developed. As a practical application, the problem of indexing substrings has been studied more in depth