search

meelgroup / ganak

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

Sampling set with Sym Ganak #14

Closed Exeloz closed 3 years ago

Exeloz commented 3 years ago

Pardon me if this is an intended behavior, but I was exploring the branch symganak and found that the sampling sets written in a cnf file didn't work as I would expect. More precisely, if a sampling set is written using the notation c ind V1 V2 ... Vn 0, more than 2^n solutions can be returned.

Here is a small example:

p cnf 46 64
c ind 1 2 3 4 5 6 7 8 9 10 0
-6 -39 0
-7 -39 0
-6 -7 40 0
-38 -40 0
-8 -38 39 0
-8 -40 0
-9 38 0
-7 -44 0

Using the solver crytominisat, I obtain a total of 704 solutions, which is the same number indicated by ganak. However, symganak indicates a total of 7971459301376 solutions, which is largely over 2^10.

Since the Readme.md for the symganak branch does not feature information about Projected Model Counting, I expect that this behavior is already known. I'm still writing this issue since symganak clearly reads the sampling set and output informations about it while being executed.

smsharma1 commented 3 years ago

Hi @Exeloz, As of now, Symganak does not support projected model counting. If you use the symmetric component caching feature which is under a flag you will get the following msg in the output: ``Warning! The sampling set is present but projected model counting is turned off"

Please refer to the script run_sym_ganak.sh for more details. Thanks!

msoos commented 3 years ago

@smsharma1 I believe it would be best to fix the code by exiting with an error, rather than printing a warning. Most people don't read warnings, heck I don't read warnings. It's important to "hard fail" in case of potential confusion, or things could go very wrong. I strongly suggest we error out and give instructions e.g. how to remove the sampling set.

smsharma1 commented 3 years ago

Thanks for the suggestion Mate.

Hi @Exeloz, Thanks for reaching out with your query. Symganak will now error out if symmetric component caching is used and a sampling set is present in the input file. If symmetric component caching is not used Symganak will give a correct projected model count. Please take a look at the recent changes and let me know if you face any difficulties.

Regards, Shubham

Exeloz commented 3 years ago

Thank you for your answers! I'm quite sorry for the delay, we have a new addition to the family that need some attention. If any problem happen, I will notify. Thanks!