Iterating over all satisfying assignments for a ZBDD?

[johnrudge]

Thank you for the oxidd package! I'm sorry if I've missed this somewhere, but is it possible to iterate over all satisfying assignments for a ZBDD with oxidd? I'm using the python interface, and I can see the function ZBDDFunction.pick_cube which can be used to give me a satisfying assignment, but nothing that seems to allow me to iterate over all satifying assignments. It would be great to have something like ZBDDFunction.pick_cube_iter that would give an iterator (python generator) that can be used to loop over all satisfying assignments.

[nhusung]

There is no simple function for iterating over all cubes of a function yet. Since you mention ZBDDFunction.pick_cube (and not the recently added symbolic version), I assume you want the cubes as lists over bool|None and not as ZBDDs, right? I’m currently working on a paper and the deadline is coming close, but afterwards I can implement that.

[johnrudge]

Thanks for the reply! Yes, that's right. I'm viewing the ZBDD as describing a set of sets, and I want to iterate through the individual sets in a for loop, similiar to what can be done with setset in graphillion https://github.com/takemaru/graphillion/blob/20d54642bec34398da962c7308e5b25f08ef3452/graphillion/setset.py