Advanced Satisfiability Functions

[SSoelvsten]

In order of complexity:

• [ ] bdd_satcountln: The number of satisfiable assignments can be very large (even larger than 2⁶⁴ at times). Hence, the BDD package BuDDy also provides this function, that outputs the logarithm of the number of satisfiable assignments.

  This should be possible to achieve with a new policy for the count algorithm.

• [ ] bdd_satone: Gives you some (unspecified) assignment. This could be a faster variant of the bdd_satmin and bdd_satmax as it stops early on the first arc to the 1 terminal.

• [ ] bdd_satall / zdd_elems : Currently, we only provide functions to obtain the lexicographically smallest or largest assignment. Hence, we are still missing this function, which given a callback function, iterates over all satisfying assignments.

  To output all assignments in in lexicographical order.

  • [ ] Support switching direction in file_stream and levelized_file_stream.
  • [ ] Use an I/O efficient stack to traverse all assignments. This stack could store the tpie::file_stream position for a faster return to a parent.

  But, that may cost up to O(N/B) I/Os per satisfying assignment. Question is, whether we can traverse them faster (in practice, at least) by bunching processing the ones physically close together.

• [ ] bdd_satrnd / zdd_rndelem: Provides a random satisfying assignment. The question then is, how can one ensure a uniform distribution over all outputs? Notice, one cannot just do a coin-flip at each node, since the number of true assignments for each may be different. Is it possible to do something without the need for meta information on each node?

  It might be possible to compute a weight on each node (somewhat like the Dijkstra algorithm in #430) with the number of in-going assignments? If so, one can start at the true terminal, roll the dice between 0 and weight(true) and pick some parent n. This is then repeated at n for all of its parents until the root has been reached.

• [ ] bdd_satshortest: Provides the satisfying assignment with the fewest non-DON'T CARE evaluations; this corresponds to the shortest path in the BDD to true. To compute it, one needs to modify the Dijkstra-like algorithm in #430 .

All of these also have a cube variant ( as to-be implemented in #454 ).