I've always wondered how those can be performant at all compared to approaches like SAT.
BDD is for #P complete problems. IE: counting the number of solutions to an NP complete problem, like circuit analysis where having the total count of 1 output vs 0 output is useful.
#P complete is at least as difficult as NP complete.
--------
BDDs seem like they can be used with the easier NP complete space, especially for optimization problems. But it's a bit indirect, as BDDs kinda represent an entire search space rather than just one solution.
BDDs are useful in optimization, where having a dynamically updated efficient tree of all possible solutions (as currently understood by the algorithm), or at least an estimate of the search space, is useful.
I read a cool paper on restricted BDDs and relaxed BDDs, where one BDD overestimates all 'true' solutions, and the other underestimates all 'true'. Since they are estimates, they are bounded in space (and therefore bounded in time to process). The relaxed+restricted BDDs serve as search guides to some optimization problem in NP with reasonable efficiency.
Giving a better guide than previous guides (ie: arc consistency or path consistency have very little flexibility with regards to space taken up / time spent on the heuristic. But relaxed+restricted BDDs can achieve a similar guided heuristic effect with better controls over size and time).
This is an euphemism :)! It is quite likely that #P is way harder than NP as witnessed by Toda's Theorem https://en.wikipedia.org/wiki/Toda%27s_theorem
But even if you are only interested in satisfiability, it sometimes happened that OBDD-based solvers are more efficient than CDCL SAT-solver. Indeed, for some application, you need to have richer constraints than the clauses used in CNF formulas. For example, for circuit synthesis, you often need to represent parity constraints (parity(x1...xn) is true iff there are an even number of values set to 1). CNF encoding of such constraints are expensive and kill most of the clever stuff that CDCL solvers do, while representing a parity constraint is actually quite easy with an OBDD of size 2n.
BDDs obtain an exact count, and are among the most efficient algorithms for this problem.
"Counting" the solutions is closely related to "finding at least one solution". But they are fundamentally different. BDDs will be "less efficient at finding just one solution" compared to traditional SAT solvers. But SAT solvers are much less efficient at enumerating the entire solution space and/or finding exact counts.