Independent Set contains variables greater than numVars about arjun HOT 5 CLOSED

Hey,

Sorry again for the mess. If there were no variables in the independent set that were larger than the max_var, then the result would be identical. For the ones that did contain variables oob, you should re-run.

Sorry and thanks for pointing out this bug,

Mate

from arjun.

Hi,

I don't understand. None of the files you attached as "new" have any independent variables that are larger than the declared header. In more detail, you have attached a ZIP file with 4 CNFs in "new_cnfs" folder, all 4 of which have headers and c ind that are completely fine. None of the c ind seem to be larger than the declared number of variables.

Please either (1) be more specific of what's wrong, or (2) attach files that demonstrate the issue so I can reproduce and fix. To be clear, I am not questioning that there is a bug -- there unfortunately likely is a bug :( However, I can't seem to find it, and your files don't seem to show it. So something is off? Note that all the outputs you attached also miss the --renumber 0 flag that you said you added? See e.g.:

c executed with command line: ./arjun-1190e8a --input issues/ind-set_oob/original_cnfs/mc21_track1_122.cnf issues/ind-set_oob/new_cnfs/mc21_track1_122_arjun-1190e8a.cnf

or:

c executed with command line: ./arjun-43b17ef58-9bf1d82a7-64blinux-static --input issues/ind-set_oob/original_cnfs/mc2022_track1_023.cnf issues/ind-set_oob/new_cnfs/mc2022_track1_023_arjun-43b17ef58.cnf

Maybe you attached the wrong file? Something is off.

from arjun.

mc21_track1_122_arjun-1190e8a.cnf has the variable 758 (>740) in the independent support
mc2022_track1_023_arjun-43b17ef58.cnf has variables 46 47 49 50 (>36)
mc2022_track1_023_arjun-1190e8a.cnf has variables 46 47 49 50 (> 36)

mc21_track1_122_arjun-43b17ef58.cnf has no extra variables but I included it because there was a difference with respect to the newer commit 1190e8a (see first file above), and I thought showcasing this behavior might help with pinpointing and debugging the issue.

Yes, I have not used the "renumber 0" flag for these cases.

Please let me know if you need any more info,

Thanks,
Aditya

from arjun.

NICE CATCH! Thanks so much, I am completely idiotic. So this has now been fixed in CryptoMiniSat, commit 0183cc7ae52b3b41d70cf62d12d6b842f922bd36. The precautions I am now taking:

• Assert added to printing independent support, so if this happens again, it's an assert-fail, not some weird bug
• Independent support is now sorted, so it'll be obvious if something is wrong. Previously, it was "almost" sorted which is very annoying, and lead to me being blind.
• We are working on a fuzzer. You will see that there are some bugfixes in CMS and ApproxMC that found some bugs. Hopefully, we'll be fuzzing Arjun as well, which should lead to near-zero bugs

Thanks again, and sorry for my confusion above. I was blind. I hope this fixes it! If not, please re-open or open a new issue if it's a different bug. Thanks

Mate

from arjun.

Thanks a lot for the quick fix!

I had run a bunch of experiments with commit 1190e8a and most cnf files didn't have this issue. I was wondering if I can assume the independent supports for those files to be correct or if I should rerun all the experiments. Can you advise?

Thanks,
Aditya

from arjun.