Don't build the solver in the BDD

[aspiwack]

Building a BDD with the entire logic program (the bit which encodes the question: is this seed solvable?) is massively overkill.

What we want is only to know, for a given assignment, whether it is solvable or not, and put that value at the bottom of the bdd. Letting the logic program be part of the bdd (then extistentially quantify over the variables for the have and reach predicates) achieves that result. But also so, much, much, more. It will find all possible proofs. Of all assignments. At the same time. That's how I got trivial bits of logic take up to 20GB+ of memory before I killed them in frustration, long before they reach completion. That's why the current implementation is completely useless.

On the other hand, SAT solver, which have the precise same semantics, are stupidly fast. Among other things because they don't represent everything there is to know about the clauses in memory at the same time. So let's use one.

Game plan

To avoid recomputing stuff over and over again, let's use an incremental SAT solver.

When we are there, we can simply use the SAT solver as our main loop. Here is the plan:

1. Feed the logic program (and the goals) to the SAT solver
2. Obtain a model
3. Extract the values of the Assign variables in the model
4. Add (by taking the conjunction) the corresponding formula to the bdd. (if, say, the model says A is true, and B is false, and C is true, and D is undecided, the corresponding formula is A∧¬B∧C).
5. Add the negation of that formula to the (incremental) SAT solver (in the example that's ¬A∨B∨¬C). So that any further model is a different assignment.
6. Go back to 2, until there is no models left

The final bdd will represent all the logical assignments. We can build it directly in a zdd (the zdd for all possible assignements, with which we start, has exactly one node per possible assignment (that is #items*#locations), which is small enough, and I expect the size of a zdd to grow less rapidly in this case than a bdd's because many nodes will be set to 0 as we lose sharing).

We probably don't want to do the path-counting on the intermediate bdds, though. So we should make a final conversion, at the end, to count the paths.

[aspiwack]

Well, apart from the idle thought about intermediate forms, really, #3 solves this.

This is massively faster. Though, we may still be quite far away from being able to model the entire logic of alttp. As my example with a portion of the starting logic already takes 10s to resolve.