That's like asking if using hashmaps are easier than using a database.
You'd probably use BDD in a SAT solver. BDDs grossly cut down on the storage requirements of your variables and their possible "true/false" states... while almost all SAT-based math (union, intersection, etc. etc.) remains efficient.
BDDs aren't the only datastructure (ex: a B-Tree could beat a HashSet in a Database). But BDDs are a very, very good data-structure for SAT.
Uhm, I'm not sure about that. Most state-of-the-art SAT solvers nowadays will rely on CDCL [0], which does not need BDDs. A recent paper [1] is quite clear on that:
> The Conflict-Driven Clause Learning (CDCL) solvers form the core of the algorithms for solving the Boolean satisfiability problem (SAT).
There is a huge slide deck [2] which contains (in the first part) a lot of details about modern SAT solving. Highly recommended reading for those interested.
You'd probably use BDD in a SAT solver. BDDs grossly cut down on the storage requirements of your variables and their possible "true/false" states... while almost all SAT-based math (union, intersection, etc. etc.) remains efficient.
BDDs aren't the only datastructure (ex: a B-Tree could beat a HashSet in a Database). But BDDs are a very, very good data-structure for SAT.