> You'd probably use BDD in a SAT solver. Uhm, I'm not sure about that. Most state-of-the-art SAT solvers nowadays will rely on CDCL [0], which does not need B

> You'd probably use BDD in a SAT solver. 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 https://en.wikipedia.org/wiki/DPLL_algorithm [1]: https://link.springer.com/chapter/10.1007%2F978-3-030-51825-7_11 https://link.springer.com/chapter/10.1007%2F978-3-030-51825-... [2]: http://vmcaischool19.tecnico.ulisboa.pt/~vmcaischool19.daemon/wp/wordpress/wp-content/uploads/2019/01/jms-vmcai19-ws-slides.pdf http://vmcaischool19.tecnico.ulisboa.pt/~vmcaischool19.daemo...