search

meelgroup / ganak

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

A potential bug with CNF Examples while using Ganak #28

Closed Annlean closed 6 months ago

Annlean commented 6 months ago

Hi! I recently encountered an issue while utilizing Ganak. I attempted to process two CNF files using Ganak. I set the timeout of running the model counter to 600 seconds. The origin.cnf file can be processed soon while the new.cnf file cannot stop withing 600 seconds. The two files differ by only one clause (origin.cnf is "64 -92 -5 -62 38 0" while new.cnf is "64 -92 -92 -5 -62 38 0") and produce completely opposite results. To assist the diagnosis, I conducted further tests: the critical clause "64 -92 -92 -5 -62 38 0" and the key variable "92" in new.cnf, which seem to be causing the timeout. I think Ganak may have a potential bug, and I hope this information can assist you to address the potential bugs. The two example files are attached here for your reference. Best regards,

Haiyan and Jifeng CSTAR group

Annlean commented 6 months ago

Hi, The bugs no longer exist in the new version of ganak, and the new ganak performs very well and is significantly faster. Thank you for your work! Thanks for your reply!

msoos commented 6 months ago

Glad to hear!

Annlean commented 6 months ago

There are still some problems with the current ganak version on Github. For example, "[2] 446164 segmentation fault (core dumped) ./ganak" will appear when running benchmarks/toy3.cnf. Looking forward you can update github after the latest ganak related work is completed.

msoos commented 6 months ago

As stated before, we are well aware of the issues with the GitHub version. I can fuzz it and generated millions of bugs. Please do not report any further bugs, until the github repo has been updated. Thanks for your patience.