I only (kind of) know BDDs because of their application to symbolic model checking. Moreover, I will be very low on details. So take this reply with a pinch of salt. Short answer: they're different.
BDDs allow for some formula manipulations that make it easy to devise "unbounded" model-checking (UMC) techniques (i.e., they can explore the full state space of a system).
On the other hand, if you are only interested in a bounded exploration of the state space (i.e., check only those states that are at most "k" steps far from the initial state), then you can usually unroll the transition relation, encode it as a CNF formula, and just feed it to a SAT solver. This approach is usually faster than BDDs.
To extend SAT solvers to the UMC case, you have to either devise some tricks to do the aforementioned formula transformations with a SAT solver too, or use the solver to find an inductive argument (if the system is safe up to k steps, it will be safe up to k+1 step, for any k). This is known as k-induction.
Seminal papers in this field include:
J. R. Burch et al., “Symbolic model checking: 10^20 states and beyond,” in LICS 1990. doi: 10.1109/LICS.1990.113767. (BDD-based symbolic model checking)
A. Biere et al., “Symbolic model checking without BDDs,” in TACAS 1999. doi: 10.1007/3-540-49059-0_14. (SAT-based bounded model checking)
K. L. McMillan, “Applying SAT methods in unbounded symbolic model checking,” in CAV 2002. doi: 10.1007/3-540-45657-0_19. (SAT-based unbounded model checking)
M. Sheeran et al., “Checking safety properties using induction and a SAT-Solver,” in FMCAD 2000. doi: 10.1007/3-540-40922-X_8. (k-induction)
BDDs allow for some formula manipulations that make it easy to devise "unbounded" model-checking (UMC) techniques (i.e., they can explore the full state space of a system). On the other hand, if you are only interested in a bounded exploration of the state space (i.e., check only those states that are at most "k" steps far from the initial state), then you can usually unroll the transition relation, encode it as a CNF formula, and just feed it to a SAT solver. This approach is usually faster than BDDs.
To extend SAT solvers to the UMC case, you have to either devise some tricks to do the aforementioned formula transformations with a SAT solver too, or use the solver to find an inductive argument (if the system is safe up to k steps, it will be safe up to k+1 step, for any k). This is known as k-induction.
Seminal papers in this field include:
J. R. Burch et al., “Symbolic model checking: 10^20 states and beyond,” in LICS 1990. doi: 10.1109/LICS.1990.113767. (BDD-based symbolic model checking)
A. Biere et al., “Symbolic model checking without BDDs,” in TACAS 1999. doi: 10.1007/3-540-49059-0_14. (SAT-based bounded model checking)
K. L. McMillan, “Applying SAT methods in unbounded symbolic model checking,” in CAV 2002. doi: 10.1007/3-540-45657-0_19. (SAT-based unbounded model checking)
M. Sheeran et al., “Checking safety properties using induction and a SAT-Solver,” in FMCAD 2000. doi: 10.1007/3-540-40922-X_8. (k-induction)