adiar
adiar copied to clipboard
`bdd_pathcount`, `bdd_satcount`, and `zdd_size` can overflow in their output
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
-
Add the option to use double instead of uint64_t for a "non-exact" output.
-
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?
-
Use
boost::cpp_int
orboost::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
andtpie::merge_sorter
but not (yet) theirtpie::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.
- Alternatively to extending TPIE, we can add a fully bucketed levelized priority queue, and so abuse the fact that