From: SourceForge.net <noreply@so...>  20041005 12:52:15

Bugs item #1040620, was opened at 20041005 14:52 Message generated for change (Tracker Item Submitted) made by Item Submitter You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1040620&group_id=112658 Category: None Group: None Status: Open Resolution: None Priority: 5 Submitted By: Christophe Mauras (mauras) Assigned to: Nobody/Anonymous (nobody) Summary: Bug in bdd_appuni and in bdd_unique Initial Comment: It seems to me there is a bug in bdd_appuni and same in bdd_unique. These operations may not depend on variable order : Exists unique x0 such that (x0 or x1) = (x0 or x1)[x0\0] xor (x0 or x1)[x0\1] = x1 xor true = not x1 Exists unique x1 such that x0 or x1 = (x0 or x1)[x1\0] xor (x0 or x1)[x1\1] = x0 xor true = not x0 Here is the bug : Buddy reply 1 More simply : Exists unique x0 such that true = (true)[x0\0] xor (true)[x0\1] = true xor true = false Buddy reply 1 Please look at following code :  #include "bdd.h" #include "stdio.h" main(void) { bdd x0,x1,y0,y1,z0,z1,t; bdd_init (100,10); bdd_setvarnum(5); x0 = bdd_ithvar(0); x1 = bdd_ithvar(1); y0 = bdd_appuni(x0,x1,bddop_or,x0); printf("Result should be 1: 1 0 \n"); bdd_printtable(y0); printf("Good!\n\n"); y1 = bdd_appuni(x0,x1,bddop_or,x1); printf("Result should be 0: 1 0 \n"); bdd_printtable(y1); printf("Bad !\n"); z0 = bdd_unique(bdd_or(x0,x1),x0); printf("Result should be 1: 1 0 \n"); bdd_printtable(z0); printf("Good!\n\n"); z1 = bdd_unique(bdd_or(x0,x1),x1); printf("Result should be 0: 1 0 \n"); bdd_printtable(z1); printf("Bad !\n"); t = bdd_unique(bdd_true(), x0); printf("Result should be 0 \n"); bdd_printtable(z1); printf("Bad !\n"); bdd_done(); }  You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1040620&group_id=112658 
From: SourceForge.net <noreply@so...>  20050128 21:32:38

Bugs item #1040620, was opened at 20041005 05:52 Message generated for change (Comment added) made by joewhaley You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1040620&group_id=112658 Category: None Group: None >Status: Closed >Resolution: Later Priority: 5 Submitted By: Christophe Mauras (mauras) Assigned to: Nobody/Anonymous (nobody) Summary: Bug in bdd_appuni and in bdd_unique Initial Comment: It seems to me there is a bug in bdd_appuni and same in bdd_unique. These operations may not depend on variable order : Exists unique x0 such that (x0 or x1) = (x0 or x1)[x0\0] xor (x0 or x1)[x0\1] = x1 xor true = not x1 Exists unique x1 such that x0 or x1 = (x0 or x1)[x1\0] xor (x0 or x1)[x1\1] = x0 xor true = not x0 Here is the bug : Buddy reply 1 More simply : Exists unique x0 such that true = (true)[x0\0] xor (true)[x0\1] = true xor true = false Buddy reply 1 Please look at following code :  #include "bdd.h" #include "stdio.h" main(void) { bdd x0,x1,y0,y1,z0,z1,t; bdd_init (100,10); bdd_setvarnum(5); x0 = bdd_ithvar(0); x1 = bdd_ithvar(1); y0 = bdd_appuni(x0,x1,bddop_or,x0); printf("Result should be 1: 1 0 \n"); bdd_printtable(y0); printf("Good!\n\n"); y1 = bdd_appuni(x0,x1,bddop_or,x1); printf("Result should be 0: 1 0 \n"); bdd_printtable(y1); printf("Bad !\n"); z0 = bdd_unique(bdd_or(x0,x1),x0); printf("Result should be 1: 1 0 \n"); bdd_printtable(z0); printf("Good!\n\n"); z1 = bdd_unique(bdd_or(x0,x1),x1); printf("Result should be 0: 1 0 \n"); bdd_printtable(z1); printf("Bad !\n"); t = bdd_unique(bdd_true(), x0); printf("Result should be 0 \n"); bdd_printtable(z1); printf("Bad !\n"); bdd_done(); }  >Comment By: John Whaley (joewhaley) Date: 20050128 13:32 Message: Logged In: YES user_id=93687 The problem seems to be in the specification of "unique quantification". The implementation doesn't do what you might expect. To do what you would like seems like it would be a complicated algorithm. I'm not sure how it could be implemented efficiently. If you can come up with an algorithm to perform the operation on a BDD, I can change the bdd_unique implementation.  You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1040620&group_id=112658 
From: SourceForge.net <noreply@so...>  20050129 02:44:21

Bugs item #1040620, was opened at 20041005 05:52 Message generated for change (Comment added) made by joewhaley You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1040620&group_id=112658 Category: None Group: None Status: Closed >Resolution: Fixed Priority: 5 Submitted By: Christophe Mauras (mauras) >Assigned to: John Whaley (joewhaley) Summary: Bug in bdd_appuni and in bdd_unique Initial Comment: It seems to me there is a bug in bdd_appuni and same in bdd_unique. These operations may not depend on variable order : Exists unique x0 such that (x0 or x1) = (x0 or x1)[x0\0] xor (x0 or x1)[x0\1] = x1 xor true = not x1 Exists unique x1 such that x0 or x1 = (x0 or x1)[x1\0] xor (x0 or x1)[x1\1] = x0 xor true = not x0 Here is the bug : Buddy reply 1 More simply : Exists unique x0 such that true = (true)[x0\0] xor (true)[x0\1] = true xor true = false Buddy reply 1 Please look at following code :  #include "bdd.h" #include "stdio.h" main(void) { bdd x0,x1,y0,y1,z0,z1,t; bdd_init (100,10); bdd_setvarnum(5); x0 = bdd_ithvar(0); x1 = bdd_ithvar(1); y0 = bdd_appuni(x0,x1,bddop_or,x0); printf("Result should be 1: 1 0 \n"); bdd_printtable(y0); printf("Good!\n\n"); y1 = bdd_appuni(x0,x1,bddop_or,x1); printf("Result should be 0: 1 0 \n"); bdd_printtable(y1); printf("Bad !\n"); z0 = bdd_unique(bdd_or(x0,x1),x0); printf("Result should be 1: 1 0 \n"); bdd_printtable(z0); printf("Good!\n\n"); z1 = bdd_unique(bdd_or(x0,x1),x1); printf("Result should be 0: 1 0 \n"); bdd_printtable(z1); printf("Bad !\n"); t = bdd_unique(bdd_true(), x0); printf("Result should be 0 \n"); bdd_printtable(z1); printf("Bad !\n"); bdd_done(); }  >Comment By: John Whaley (joewhaley) Date: 20050128 18:44 Message: Logged In: YES user_id=93687 Actually, I spoke too soon. I just implemented a correct bdd_unique and bdd_appuni. The trick is that the algorithm must determine when a quantified variable is skipped. When it is skipped, the result must be zero. (This is because conceptually the zero branch and one branch point to the same function, and therefore the xor is zero.) Note that unique quantification really says "Are there an odd number where this is true?" rather than "Is this true under exactly one?" If you are only quantifying out one variable, then the "odd" case is exactly the "one" case. But if you are quantifying multiple variables, then the behavior may be different than you would expect. I checked in an implementation in the copy of buddy in the JavaBDD repository and it passes the test cases. I'll backport it into buddy at some point.  Comment By: John Whaley (joewhaley) Date: 20050128 13:32 Message: Logged In: YES user_id=93687 The problem seems to be in the specification of "unique quantification". The implementation doesn't do what you might expect. To do what you would like seems like it would be a complicated algorithm. I'm not sure how it could be implemented efficiently. If you can come up with an algorithm to perform the operation on a BDD, I can change the bdd_unique implementation.  You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1040620&group_id=112658 