msoos
commented
7 months ago Hi,
My suggestion is that you think about re-encoding your problem in a way that contains less clauses (but likely a lot more variables, and that's a GOOD THING). It will almost never finish running anyway if you don't. We could recompile that thing but it will likely never terminate. You almost surely need to add more variables so the problem can be encoded much more efficiently, and therefore solved more efficiently. Less variables is NOT equal to less solving time. In fact, often it's the exact opposite. You can restrict counting only to the variables that you are interested in by adding a like:
c p show 1 23 72 62 0Which will restrict counting over different solutions over these variables only. This is called projected counting, Then, you can freely add new variables to make the formula a lot smaller. Again, it will almost surely never be counted if you don't do this. So think about how it could be done.
Sorry, but I really can't help much. I will eventually publish a LARGEMEM binary (or you can compile one if you like), but almost surely it will not help, You need to re-think how you model problem. I suggest reading a few papers/examples of how other people modeled their problems, and taking ideas from that. Without that, it will never be counted.
Good luck. Sorry, I really can't help you much more than this,
Mate
I am getting a memory manager can't handle load error when processing a 3gb CNF file. The error message tells me to recompile with -DLARGEMEM=ON but i am not sure which binary i am supposed to recompile with this flag. I tried recompiling all 3 by adding the -DLARGEMEM=ON flag to the cmake command but i get a warning from cmake that the flag is not used for both arjun and approxmc.
Recompiling all 3 binaries (CMS, arjun and ApproxMC) still results in the same error. I can also see that in COMPILE_DEFINES when running ApproxMC that it does not see the DLARGEMEM flag.
Is there something that i am missing?