Symbolic boolean manipulation with ordered binary-decision diagrams
ACM Computing Surveys 24(3): 293-318