Segmentation fault

[vlastikw]

bugCMS.zip
Hi, attached instance which causes error.

If running with first row c ind (which is VAR variables for me) it fails. I've tried version 580x64 (static release from git) and it fails quickly after 548K conflicts. I've tried newest version 5114 then. It failed after many days output attached after 191315K conflicts.

But if I run the instance with 580x64 with indicators from the second row c ind (which is BAR variables for me) it provides first solution after 83429K conflicts. My guess is that with VAR indicators it allocates too much memory suddenly but not sure cannot test it. It must be some bug. Can you please have a look and provide feedback?

bugCMS.zip

[capiman]

Perhaps you can run it with

gdb --args executablename arg1 arg2 arg3

"run" to start it, you should see output of CMS

When you hit the segfault it stops and gives you a prompt.
There you can enter "bt" for backtrace, which give you last function/method calls till reaches the segfault.

[capiman]

E2 like "Eternity II"?

[msoos]

Hi,

Thanks for the bug report! I am a bit confused why you have c ind line. It's used only in case you are using CryptoMiniSat to count solutions via the --maxsol XYZ parameter or are using the CNF in ApproxMC or UniGen. Do you need it for something?

I am independently looking at the bug, since it's a bug either way. I'm just curious why you have the c ind, maybe it's not needed and could be a quick fix for you?

Thanks again for the bug report,

Mate

[vlastikw]

Hi Mate, "c ind" is very useful feature (nice to have to read it from external file) because I have 3 sets of independent variables - two of original vars and the rest are auxiliary variables from AMO constraint. If you search for more solutions after each solution is found and banned if auxiliary variables are not excluded all variables are again added to the search space and thus preprocessing must be done again which wastes time and all progress done before. And if I don't exclude auxiliary variables it counts solutions which are not "different" because they have same all original variables. It depends on how PB constraints are encoded into SAT CNF clauses. Yes it is eternity two like puzzle i.e. edge matching which is very hard even for 8000 variables so I'm testing different solvers after each SAT race to see the performance and progress. I'd like to provide some benchmark set for next competition. Thank you Vlasta ne 12. 2. 2023 v 22:30 odesílatel Mate Soos ***@***.***> napsal:

…

Hi, Thanks for the bug report! I am a bit confused why you have c ind line. It's used only in case you are using CryptoMiniSat to count solutions via the --maxsol XYZ parameter or are using the CNF in ApproxMC or UniGen. Do you need it for something? I am independently looking at the bug, since it's a bug either way. I'm just curious why you have the c ind, maybe it's not needed and could be a quick fix for you? Thanks again for the bug report, Mate — Reply to this email directly, view it on GitHub <#710 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ANIOX3XEDTWIOLABJ77VI6LWXFI7DANCNFSM6AAAAAAUY2KPX4> . You are receiving this because you authored the thread.Message ID: ***@***.***>