adiar icon indicating copy to clipboard operation
adiar copied to clipboard

`bdd_pathcount`, `bdd_satcount`, and `zdd_size` can overflow in their output

Open SSoelvsten opened this issue 3 years ago • 0 comments

Our current examples do not show this problem, but the bdd_pathcount and bdd_satcount functions can potentially output values much larger than 264-1. There are three possible solutions

  1. Add the option to use double instead of uint64_t for a "non-exact" output.

  2. Use a fixed-width unsigned integer that is std::trivially_copyable. This could be with a fixed width of 1024 bits. This effectively postpones the problem to 21024 number of paths and satisfiable solutions.

    • Should the number of bits then be chosen at compile-time?
  3. Use boost::cpp_int or boost::gmp_int. These support any arbitrary number of bits. This means, that unlike in (1) and (2) we do not just delay when the problem happens.

    To this end, we need to create a custom serialize and deserialize function for these variable-length entities needed. TPIE already supports a lot of this out-of-the-box when it comes to tpie::file_stream and tpie::merge_sorter but not (yet) their tpie::priority queue. So, we would need to first add support for such non-trivial elements in a priority queue.

    • Alternatively to extending TPIE, we can add a fully bucketed levelized priority queue, and so abuse the fact that tpie::merge_sorter already supports variable sized elements.

SSoelvsten avatar Jun 07 '21 06:06 SSoelvsten