xor clean consumes too much memory

[vlastikw]

After Executing strategy token: renumber [xor-clean] is started. While before that the solver consumed only about 2 GB memory suddenly it grows up until it consumes more than 16GB and crashes (or is killed).

Why? How can it be avoided. I assume this is not normal behavior and should be investigated. It happens also on smaller instance however I don't remember or don't have a better example right now. But point is it consumes 5x or more times memory than currently does.

Attached instance and output. It happens after 4 hours on my PC.

solver crashed.txt
e2VAR_12x12.cnf.zip

[msoos]

Sorry, I'll pick this up in the coming days, this is 100÷ an issue. I'll get back to you on Saturday, hopefully with a fix :) Mate

…

On Wed, Oct 28, 2020, 13:48 vlastikw ***@***.***> wrote: After Executing strategy token: renumber [xor-clean] is started. While before that the solver consumed only about 2 GB memory suddenly it grows up until it consumes more than 16GB and crashes (or is killed). Why? How can it be avoided. I assume this is not normal behavior and should be investigated. It happens also on smaller instance however I don't remember or don't have a better example right now. But point is it consumes 5x or more times memory than currently does. Attached instance and output. It happens after 4 hours on my PC. solver crashed.txt <https://github.com/msoos/cryptominisat/files/5451896/solver.crashed.txt> e2VAR_12x12.cnf.zip <https://github.com/msoos/cryptominisat/files/5451905/e2VAR_12x12.cnf.zip> — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#632>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKF4OICOGTNUGJ4BXKOVU3SNAHK7ANCNFSM4TCI2MTA> .

[vlastikw]

Hi,
I've tried --xor 0 or --renumber 0 but it won't help. It was even worse or the same. With --presimp it's much faster the memory allocation from 2GB to more than 16GB comes after 90 minutes.
I've tried cryptominisat 565 and it runs smoothly hours and generates more than 300 solutions with less than 2GB memory.

[msoos]

Wow, this is a weird instance :) Can you please do me a favour and check if setting -intree 0 --sls 0 helps? I am running massif right now, but that is about 3-5x slower than normal running so it'll take some time. Thanks!

[msoos]

Hi! So valgrind crashed on me overnight and decided not to dump the data while crashing :D My understanding is that it's the --sls 0 that will fix things. Can you please try? Thanks!

[vlastikw]

Hi,

I'm running it for you. I've tried --intree 0 and --sls 0 together and looks good. 500 sols after 3 hours output attached. But running with --presimp 1 to make it crashed sooner but it still runs. I let it run with only --sls 0 and let you know.
e2VAR_12x12.msoos.txt

[msoos]

Ah nice! so --intree 0 and --sls 0 is not eating memory and effectively is fixing the problem. That's great feedback! I'll try to check what that could mean. In the meanwhile if you can let me know what only giving --sls 0 does, that'd be great!

Thanks again,

Mate

[vlastikw]

Now it finished (crashed) also with --presimp 1 after 2 hours and in about the same place as without it after second inprocessing phase after first solution found. Output attached. Starting now --presimp 1 and --sls 0.

I thought it will be --intree 0 solving this with some cycle in the tree ;-) let's see if it's --sls 0.
e2VAR_12x12.msoos2.txt

[vlastikw]

So it looks like --sls 0 solved it, output attached. Interesting is the number of solutions returned after 2 hours.
-- presimp 1 -> 17 solutions then memory allocation issue => killed
--presimp 1 --sls 0 -> about 60 solutions i.e. 3x times more
--presimp 1 --sls0 --intree 0 -> about 500 solutions i.e. 8x more than --sls 0 and 25x more than without both. It's amazing speed up, of course only in this case. I will try to run more instances without sls and intree to see what happens. Actually it seems to me that only BVE (90%) and BVA(10%) is what matters the most.

Thank you for your help and fingers crossed with bug fixing.
e2VAR_12x12.msoos3.txt

[msoos]

Nice! So what is probably happening is that in-tree probing (i.e. intree) is generating a ton of binary clauses in your case and they are slowing things down. I wonder if this is a more generic issue, affecting other problem types, too. I know that intree probing is super-helpful in many-many cases, but perhaps the number of binary clauses it's generating should be limited (or there is a bug? that'd be weird). I'll look into it! Thanks for this, I'm glad things are faster now!

Cheers,

Mate