Learn how easy it is to sync an existing GitHub or Google Code repo to a SourceForge project!

## buddy-users

 [Buddy-users] A simple question about BuDDy From: Qin Yang - 2005-08-05 23:27:17 ```Dear Haim Cohen, I am a new user of BuDDy. To find all the satisfying assignments of a bdd, I find that "bdd_allsat()" is not enough for me. For example, bdd a = bdd_ithvar(0); bdd b = bdd_ithvar(1); bdd c = bdd_ithvar(2); bdd x = a & !b & c; x |= a & !b & !c; The satisfying assignments of x are [1,0,1] and [1,0,0]. However, "allsatHandler()" provides the assignment of [1,0,X] ('X' means notcare). Could you tell me if there is any interface that I can use to obtain all the unique assignments (not including 'X') similarly? Thanks a lot! Best Regards, Qin ____________________________________________________ Start your day with Yahoo! - make it your home page http://www.yahoo.com/r/hs ```
 Re: [Buddy-users] A simple question about BuDDy From: Alexandre Duret-Lutz - 2005-08-05 23:52:56 ```>>> "QY" == Qin Yang writes: QY> Dear Haim Cohen, QY> I am a new user of BuDDy. To find all the satisfying QY> assignments of a bdd, I find that "bdd_allsat()" is QY> not enough for me. For example, QY> bdd a = bdd_ithvar(0); QY> bdd b = bdd_ithvar(1); QY> bdd c = bdd_ithvar(2); QY> bdd x = a & !b & c; QY> x |= a & !b & !c; You can always extract one assignment using bdd_satoneset(), NAND it out of x, and iterate until x is false. bdd varset = a & b & c; while (x != bddfalse) { bdd one = bdd_satoneset(x, varset, bddtrue); x -= one; // ... do what you want with `one' ... } Surely that must be less effective that a bdd_allsat()-style interface: bdd_satoneset() and -= will both recurse into the BDD, on each iteration, while I assume bdd_allsat() does it only once. -- Alexandre Duret-Lutz ```
 [Buddy-users] Re: A simple question about BuDDy From: Haim Cohen - 2005-08-06 01:33:49 ```I recall I had to do something similar to get all the assignments... However, if you have many assignments and you need to get them all, I would say that you should reconsider your design. The whole idea of BDDs is that they are a compact representation of Boolean function. In your application, try to defer the processing of the assignment as long as you can, and always favor BDD operations on other data structures. Haim ----- Original Message ----- From: "Qin Yang" To: Cc: Sent: Friday, August 05, 2005 19:27 Subject: A simple question about BuDDy > Dear Haim Cohen, > > I am a new user of BuDDy. To find all the satisfying > assignments of a bdd, I find that "bdd_allsat()" is > not enough for me. For example, > bdd a = bdd_ithvar(0); > bdd b = bdd_ithvar(1); > bdd c = bdd_ithvar(2); > > bdd x = a & !b & c; > x |= a & !b & !c; > The satisfying assignments of x are [1,0,1] and > [1,0,0]. However, "allsatHandler()" provides the > assignment of [1,0,X] ('X' means notcare). Could you > tell me if there is any interface that I can use to > obtain all the unique assignments (not including 'X') > similarly? > > Thanks a lot! > > Best Regards, > Qin > > > > ____________________________________________________ > Start your day with Yahoo! - make it your home page > http://www.yahoo.com/r/hs > > ```