I have the pleasure to announce the to announce the first opam release of Snowflake : a Generic Symbolic Dynamic Programming framework interfacing WAP, RBTF and MLBDD.
One can use it to solve (possibly Quantified) CNF, (possibly parametrized) integer programming, asynchronous automata composition (although we did not try that one yet).
And by solve, we compute a representation of the full set of solution not just a single one[1], which is sometime useful.
Snowflake currently uses binary decision diagrams to reason symbolically, but other symbolic formalism could be used in their place.
Complex systems (either physical or logical) are usually structured and sparse, that is, they are build from individual components linked together, and any component is only linked to a rather small number of other components with respects to the size of the global system.
RBTF exploits this structure, by over-approximating the relations between components as a tree (called decomposition tree in the graph literature) each node of this tree being a set of components of the initial systems. Then, starting from leaves, each sub-system is solved and the solutions are projected as a new constraints on their parent node, this process is iterated until all sub-systems are solved. This step allows to condensate all constraints into a single sub-system and check their satisfiability. We call this step the Forward Reduction Process (FRP).
Finally, we can propagate all the constraints back into their initial sub-system by performing those same projection in the reverse direction. That is, each sub-system update its set of solution given the information from its parent then send the information to its children sub-systems (possibly none, if its a leaf). We call this step the Backward Propagation Process (BPP).
with the right set of parameters, one can also compute a single solution if one does not need more. ↩︎