TR95-042 Authors: Beate Bollig, Ingo Wegener

Publication: 14th September 1995 11:27

Downloads: 2872

Keywords:

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 based on read-once projections.

For many problems it is determined whether and how they are related with

respect to read-once projections.

It is proved that multiplication can be reduced to squaring but

squaring is not a read-once projection of multiplication.

This perhaps surprising result is discussed.

For most of the common binary decision diagram models of polynomial size

complete problems with respect to read-once projections are described.

But for the class of functions with polynomial-size free binary decision

diagrams (read-once branching programs) no complete problem with respect

to read-once projection exists.