Almost the same types of restricted branching programs (or binary decision diagrams BDDs) are considered in complexity theory and in applications like hardware verification. These models are read-once branching programs (free BDDs) and certain types of oblivious branching programs (ordered and indexed BDDs with k layers). The complexity of the ... more >>>

Computational complexity is concerned with the complexity of solving problems and computing functions and not with the complexity of verifying circuit designs. The importance of formal circuit verification is evident. Therefore, a framework of a complexity theory for formal circuit verification with binary decision diagrams is developed. This theory is ... more >>>

An increasing number of results in graph theory, combinatorics and theoretical computer science is obtained with the help of computers, e.g. the proof of the Four Colours Theorem or the computation of certain Ramsey numbers. Binary decision diagrams, known as tools in hardware verification and computer-aided design, are used here ... more >>>

Linear Transformed Ordered Binary Decision Diagrams (LTOBDDs) have been suggested as a generalization of OBDDs for the representation and manipulation of Boolean functions. Instead of variables as in the case of OBDDs parities of variables may be tested at the nodes of an LTOBDD. By this extension it is possible ... more >>>

Many BDD (binary decision diagram) models are motivated by CAD applications and have led to complexity theoretical problems and results. Motivated by applications in genetic programming Krause, Savick\'y, and Wegener (1999) have shown that for the inner product function IP$_n$ and the direct storage access function DSA$_n$ all functions which ... more >>>

Branching programs are a well-established computation model for Boolean functions, especially read-once branching programs have been studied intensively. Exponential lower bounds for deterministic and nondeterministic read-once branching programs are known for a long time. On the other hand, the problem of proving superpolynomial lower bounds for parity read-once branching programs ... more >>>

Free binary decision diagrams (FBDDs) are graph-based data structures representing Boolean functions with a constraint (additional to binary decision diagrams) that each variable is tested at most once during the computation. The function EAR_n is the following Boolean function defined for n x n Boolean matrices: EAR_n(M)=1 iff the matrix ... more >>>