4 ms·

Is it easier to use BDD instead of SAT solvers?

lou1306 6y ago
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)
dragontamer 6y ago
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.
- lou1306 6y ago
  > 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...
abecedarius 6y ago
BDDs are simple and predictable provided you know that the variable ordering that you're using will compactly encode your problem. A SAT solver might not be as predictable (though I don't have the experience to say how big this issue is in practice). A BDD can also efficiently answer questions like "how many ways can you satisfy this formula?" (subject to the same caveat about problem suitability).
- UncleMeat 6y ago
  > BDDs are simple and predictable provided you know that the variable ordering that you're using will compactly encode your problem. Sadly, variable ordering is NP-Hard. This is brutal for static analysis applications where BDDs seem like they are going to save the world but often end up crushing dreams.

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)

dragontamer 6y ago

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.

lou1306 6y ago
> 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...

abecedarius 6y ago

BDDs are simple and predictable provided you know that the variable ordering that you're using will compactly encode your problem. A SAT solver might not be as predictable (though I don't have the experience to say how big this issue is in practice). A BDD can also efficiently answer questions like "how many ways can you satisfy this formula?" (subject to the same caveat about problem suitability).

UncleMeat 6y ago
> BDDs are simple and predictable provided you know that the variable ordering that you're using will compactly encode your problem. Sadly, variable ordering is NP-Hard. This is brutal for static analysis applications where BDDs seem like they are going to save the world but often end up crushing dreams.