4 ms·

I've always wondered how those can be performant at all compared to approaches like SAT.

fcholf 4y ago
This is not the same goal as SAT. SAT looks for one satisfying assignment while OBDD tries to represent the full set of satisfying assignment in a factorized way to be analyzed later. For example, trying to count the number of satisfying assignment using a vanilla SAT-solver would be quite bad as you would end up generating every assignment while OBDD can sometimes take advantage of factorizing some part of the input. But even if you are only interested in satisfiability, it sometimes happened that OBDD-based solvers are more efficient than CDCL SAT-solver. Indeed, for some application, you need to have richer constraints than the clauses used in CNF formulas. For example, for circuit synthesis, you often need to represent parity constraints (parity(x1...xn) is true iff there are an even number of values set to 1). CNF encoding of such constraints are expensive and kill most of the clever stuff that CDCL solvers do, while representing a parity constraint is actually quite easy with an OBDD of size 2n.
- freemint 4y ago
  There are also sat solvers which do (approximate) solution counting. It is just that all these pointers seems so cache unfriendly ... But thank you for your insight
  - dragontamer 4y ago
    See the paper "The Number of Knight's Tours Equals 33,439,123,484,294 | Counting with Binary Decision Diagrams" by Martin Lobbing and Ingo Wegener. Bonus points, this occurred in the 80s, when computers only had kilobytes of memory (not even MBs). So... yeah, BDDs are an incredibly powerful technique. BDDs obtain an exact count, and are among the most efficient algorithms for this problem. "Counting" the solutions is closely related to "finding at least one solution". But they are fundamentally different. BDDs will be "less efficient at finding just one solution" compared to traditional SAT solvers. But SAT solvers are much less efficient at enumerating the entire solution space and/or finding exact counts.
  - fcholf 4y ago
    I would be curious to know examples of SAT solvers you have in mind for approximate counting. The only tools I am aware of for approximate counting are dedicated to this task (and usually use SAT solvers as oracles under the hood).
comfypotato 4y ago
Second paragraph of 382 of http://facta.junis.ni.ac.rs/eae/fu2k73/7wille.pdf http://facta.junis.ni.ac.rs/eae/fu2k73/7wille.pdf mentions how SAT solvers create BDD. I’m not super familiar with using the proofs of unsat from a solver, but I think it’s basically the BDD that shows there is no satisfying assignment.
- fcholf 4y ago
  Well this is true but CDCL SAT solvers do not materialize this BDD and they stop as soon as they find a satisfying assignment. If they do not find any satisfying assignment, they do not return the BDD as unsat proof but roughly the list of learnt clause. If these clauses have been learnt using vanilla CDCL solver technique, one can check from this that the formula is indeed unsat. See the (D)RAT proof format (check e.g., references listed for this tool https://www.cs.utexas.edu/~marijn/drat-trim/ https://www.cs.utexas.edu/~marijn/drat-trim/).
UncleMeat 4y ago
BDDs have been widely used in static analysis. They can be incredibly powerful but have an enormous weakness - their exponential reduction in size depends in large part on the term ordering and computing optimal term orderings is NP-Complete. Various systems have been developed to use ML to propose effective term orderings but my experience has been that performance is so finicky that you cannot actually rely on tools like BDDBDDB to back up industrial systems because of this.
- sitkack 4y ago
  Aren't BDDs used extensively in hardware synthesis?
dragontamer 4y ago
SAT is for NP complete problems. BDD is for #P complete problems. IE: counting the number of solutions to an NP complete problem, like circuit analysis where having the total count of 1 output vs 0 output is useful. #P complete is at least as difficult as NP complete. -------- BDDs seem like they can be used with the easier NP complete space, especially for optimization problems. But it's a bit indirect, as BDDs kinda represent an entire search space rather than just one solution. BDDs are useful in optimization, where having a dynamically updated efficient tree of all possible solutions (as currently understood by the algorithm), or at least an estimate of the search space, is useful. I read a cool paper on restricted BDDs and relaxed BDDs, where one BDD overestimates all 'true' solutions, and the other underestimates all 'true'. Since they are estimates, they are bounded in space (and therefore bounded in time to process). The relaxed+restricted BDDs serve as search guides to some optimization problem in NP with reasonable efficiency. Giving a better guide than previous guides (ie: arc consistency or path consistency have very little flexibility with regards to space taken up / time spent on the heuristic. But relaxed+restricted BDDs can achieve a similar guided heuristic effect with better controls over size and time).
- fcholf 4y ago
  > #P complete is at least as difficult as NP complete. This is an euphemism :)! It is quite likely that #P is way harder than NP as witnessed by Toda's Theorem https://en.wikipedia.org/wiki/Toda%27s_theorem https://en.wikipedia.org/wiki/Toda%27s_theorem

This is not the same goal as SAT. SAT looks for one satisfying assignment while OBDD tries to represent the full set of satisfying assignment in a factorized way to be analyzed later. For example, trying to count the number of satisfying assignment using a vanilla SAT-solver would be quite bad as you would end up generating every assignment while OBDD can sometimes take advantage of factorizing some part of the input. But even if you are only interested in satisfiability, it sometimes happened that OBDD-based solvers are more efficient than CDCL SAT-solver. Indeed, for some application, you need to have richer constraints than the clauses used in CNF formulas. For example, for circuit synthesis, you often need to represent parity constraints (parity(x1...xn) is true iff there are an even number of values set to 1). CNF encoding of such constraints are expensive and kill most of the clever stuff that CDCL solvers do, while representing a parity constraint is actually quite easy with an OBDD of size 2n.

freemint 4y ago
There are also sat solvers which do (approximate) solution counting. It is just that all these pointers seems so cache unfriendly ... But thank you for your insight
- dragontamer 4y ago
  See the paper "The Number of Knight's Tours Equals 33,439,123,484,294 | Counting with Binary Decision Diagrams" by Martin Lobbing and Ingo Wegener. Bonus points, this occurred in the 80s, when computers only had kilobytes of memory (not even MBs). So... yeah, BDDs are an incredibly powerful technique. BDDs obtain an exact count, and are among the most efficient algorithms for this problem. "Counting" the solutions is closely related to "finding at least one solution". But they are fundamentally different. BDDs will be "less efficient at finding just one solution" compared to traditional SAT solvers. But SAT solvers are much less efficient at enumerating the entire solution space and/or finding exact counts.
- fcholf 4y ago
  I would be curious to know examples of SAT solvers you have in mind for approximate counting. The only tools I am aware of for approximate counting are dedicated to this task (and usually use SAT solvers as oracles under the hood).

comfypotato 4y ago

Second paragraph of 382 of http://facta.junis.ni.ac.rs/eae/fu2k73/7wille.pdf http://facta.junis.ni.ac.rs/eae/fu2k73/7wille.pdf mentions how SAT solvers create BDD. I’m not super familiar with using the proofs of unsat from a solver, but I think it’s basically the BDD that shows there is no satisfying assignment.

fcholf 4y ago
Well this is true but CDCL SAT solvers do not materialize this BDD and they stop as soon as they find a satisfying assignment. If they do not find any satisfying assignment, they do not return the BDD as unsat proof but roughly the list of learnt clause. If these clauses have been learnt using vanilla CDCL solver technique, one can check from this that the formula is indeed unsat. See the (D)RAT proof format (check e.g., references listed for this tool https://www.cs.utexas.edu/~marijn/drat-trim/ https://www.cs.utexas.edu/~marijn/drat-trim/).

UncleMeat 4y ago

BDDs have been widely used in static analysis. They can be incredibly powerful but have an enormous weakness - their exponential reduction in size depends in large part on the term ordering and computing optimal term orderings is NP-Complete. Various systems have been developed to use ML to propose effective term orderings but my experience has been that performance is so finicky that you cannot actually rely on tools like BDDBDDB to back up industrial systems because of this.

sitkack 4y ago
Aren't BDDs used extensively in hardware synthesis?

dragontamer 4y ago

SAT is for NP complete problems. BDD is for #P complete problems. IE: counting the number of solutions to an NP complete problem, like circuit analysis where having the total count of 1 output vs 0 output is useful. #P complete is at least as difficult as NP complete. -------- BDDs seem like they can be used with the easier NP complete space, especially for optimization problems. But it's a bit indirect, as BDDs kinda represent an entire search space rather than just one solution. BDDs are useful in optimization, where having a dynamically updated efficient tree of all possible solutions (as currently understood by the algorithm), or at least an estimate of the search space, is useful. I read a cool paper on restricted BDDs and relaxed BDDs, where one BDD overestimates all 'true' solutions, and the other underestimates all 'true'. Since they are estimates, they are bounded in space (and therefore bounded in time to process). The relaxed+restricted BDDs serve as search guides to some optimization problem in NP with reasonable efficiency. Giving a better guide than previous guides (ie: arc consistency or path consistency have very little flexibility with regards to space taken up / time spent on the heuristic. But relaxed+restricted BDDs can achieve a similar guided heuristic effect with better controls over size and time).

fcholf 4y ago
> #P complete is at least as difficult as NP complete. This is an euphemism :)! It is quite likely that #P is way harder than NP as witnessed by Toda's Theorem https://en.wikipedia.org/wiki/Toda%27s_theorem https://en.wikipedia.org/wiki/Toda%27s_theorem