BDDs have been widely used in static analysis. They can be incredibly powerful but have an enormous weakness - their exponential reduction in size depends in la

BDDs have been widely used in static analysis. They can be incredibly powerful but have an enormous weakness - their exponential reduction in size depends in large part on the term ordering and computing optimal term orderings is NP-Complete. Various systems have been developed to use ML to propose effective term orderings but my experience has been that performance is so finicky that you cannot actually rely on tools like BDDBDDB to back up industrial systems because of this.