Add Pseudo Boolean Constraints (bdd_pbc and zdd_pbc)

[SSoelvsten]

In 797f542 , we removed the bdd_counter and zdd_sized_set functions because they were a nightmare to maintain and seemed like a fringe usecase. A more generalized version though is in fact useful (see Additional Context below)!

"Simple" Pseudo-Boolean Constraint

The most bare-bones function would be:

bdd bdd_pbc(const generator<pair<bdd::label, int>> &xas, const predicate<int> &p);

Here, we create the BDD for the value of the weighted linear sum, a₁ x₁ + a_n x_n, to satisfy the predicate p. For example, the old bdd_counter used weights a_i = 1 and predicate p = i -> {i == t}.

An alternative version of the same, using cost_function from #430

bdd bdd_pbc(const cost_function &as, const generator<bdd::label> &xs, const predicate<int> &p);

If one can do random-access on xs and recursively construct the BDD, then the pseudocode is very simple

bdd bdd_pbc(const int n, const int v,
            const cost_function &as, const generator<bdd::label> &xs, const predicate<int> &p)
{
  if (n== xs.size()) { return p(v); }
  const bdd f = bdd_pbc(n+1, v/*+0*/, as, xs, p);
  const bdd t = bdd_pbc(n+1, v+as(n), as, xs, p);
  return bdd_ite(xs[n], t, f);
}

Yet, in Adiar this is not as simple; since BDDs are not part of a common forrest, each call to bdd_ite is not O(1) time. Instead, it creates an entire O(N) copy of the subtrees. Neither can we create it bottom-up as the old bdd_counter, since we do not know what subtrees need to be reached. Instead, this requires a new top-down time-forward processing algorithm who's output can be reduced afterwards. This top-down algorithm unfolds the recursion level-by-level with priority queues.

Advanced Pseudo-Boolean Constraint

Above, we only think about linear constraints. Yet, some variables may want to do something when the variable is false. Or, one may very much want to do modulo arithmetic. Both of these things can probably be encoded into the weights and the predicate at the cost of having a much larger intermediate result.

So, we want to also provide the following version of the interface for those cases.

bdd bdd_pbc(const generator<bdd::label> &xs,
            const function<pair<int,int>(bdd::label_t, int)> &op,
            const predicate<int> &p);

Additional Context

Jaco van de Pol just found great use for this function in his symbolic game solving. Additionally, we can in fact encode an entire ILP with BDDs this way! This is a great feature in addition to the one in #430 .

The use-case for the advanced version comes from Randal E. Bryant's work with BDD-based SAT solving extended with pseudo-boolean constraints.