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.
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.
[0]: https://en.wikipedia.org/wiki/DPLL_algorithm
[1]: https://link.springer.com/chapter/10.1007%2F978-3-030-51825-...
[2]: http://vmcaischool19.tecnico.ulisboa.pt/~vmcaischool19.daemo...