search

OxiDD / oxidd

Concurrent decision diagram framework written in Rust
https://oxidd.net
Apache License 2.0
41 stars 5 forks source link

Iterating over all satisfying assignments for a ZBDD? #20

Open johnrudge opened 2 months ago

johnrudge commented 2 months ago

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 commented 2 months ago

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 commented 2 months ago

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