## buddy-users — Using the BuDDy library and BDDs in general

You can subscribe to this list here.

 2004 2005 2006 2008 2009 2010 2011 2012 2013 2014 Jan Feb Mar Apr May Jun Jul (2) Aug (3) Sep Oct Nov Dec Jan (1) Feb Mar Apr May Jun Jul Aug (3) Sep Oct Nov (1) Dec (1) Jan Feb Mar Apr (2) May Jun Jul Aug Sep Oct Nov (13) Dec Jan Feb Mar Apr May Jun Jul Aug Sep Oct Nov Dec (1) Jan Feb Mar Apr May Jun (1) Jul Aug Sep Oct Nov Dec Jan Feb (1) Mar Apr May (3) Jun Jul Aug Sep (1) Oct Nov Dec Jan (1) Feb Mar Apr (2) May Jun Jul Aug (1) Sep (1) Oct Nov Dec Jan Feb Mar (1) Apr May Jun Jul Aug Sep Oct Nov Dec Jan (1) Feb Mar Apr May Jun (1) Jul Aug Sep Oct Nov Dec Jan Feb (2) Mar Apr May Jun Jul Aug Sep Oct Nov Dec
S M T W T F S

1

2

3

4

5
(2)
6
(1)
7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

Showing 3 results of 3

 [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 > > ```
 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] 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 ```

Showing 3 results of 3