ECCC-Report TR95-042https://eccc.weizmann.ac.il/report/1995/042Comments and Revisions published for TR95-042en-usThu, 14 Sep 1995 11:27:23 +0200
Paper TR95-042
| Read-once Projections and Formal Circuit Verification with Binary Decision Diagrams |
Beate Bollig,
Ingo Wegener
https://eccc.weizmann.ac.il/report/1995/042Computational 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.
Thu, 14 Sep 1995 11:27:23 +0200https://eccc.weizmann.ac.il/report/1995/042