search

meelgroup / ganak

The first scalable probabilistic exact counter
MIT License
23 stars 6 forks source link

Incorrect model count in Ganak and SharpSAT #8

Closed Laakeri closed 3 years ago

Laakeri commented 3 years ago

I have found an instance with 87 variables and 25 clauses in which both Ganak and SharpSAT disagree with MiniCD2 (http://reasoning.cs.ucla.edu/c2d/), Cachet (https://www.cs.rochester.edu/u/kautz/Cachet/index.htm), and a model counter which I'm implementing from scratch. The instance is available in https://www.cs.helsinki.fi/u/tukotu/bug.cnf.

The output of Ganak and SharpSAT is 9674458629986262485827584 and the output of MiniCD2, Cachet, and my model counter is 9674458629986261412085760

I don't know if MiniCD2 and Cachet are independent implementations, but my implementation is independent from both of them and currently very simple, so therefore I believe that the bug is originating from SharpSAT, and Ganak has inherited it. I'm posting the issue here instead of SharpSAT repo because it seems that Ganak is being maintained unlike SharpSAT.

I have spend some time on trying to minify the bug instance, in particular, it is currently minimal in terms of removal of clauses.

Edit: Should be noted that I have also found instances in which Ganak and SharpSAT agree with my model counter, but MiniCD2 and Cachet disagree with them but agree with each other. So I'm not 100% confident that this is SharpSAT/Ganak bug.

Laakeri commented 3 years ago

I found that the bug is indeed in MiniCD2, Cachet, and in my implementation. Sorry for taking your time.

msoos commented 3 years ago

Hey, no worries! Thanks for the detailed analysis, seems like you are doing some good work! Keep it up :) Cheers,

Mate