Error: Variable Limit Exceeded in Large CNF

[HariNarayana123]

I am dealing with a large CNF problem. The header indicates 358,404,470 variables and 1,325,531,344 clauses. I've enabled the largemem option, but I'm encountering an error: "ERROR! Variable requested is far too large." This problem includes a significant number of XOR clauses, which is why I am using cryptominisat. Is there any way to solve problems of this size?

[a1880]

Cryptominisat has a hard-coded limit of 2^28 = 268,435,456 variables. See source code line 150 in dimacsparser.h.

Perhaps you can try to come up with some preprocessing to partition your problem into manageable pieces.

[HariNarayana123]

Thanks for the information. If the number of variables is below the hard-coded limit of 2^28 but there is still a large number of clauses, like 1,325,531,344, can this cause any memory issues even after enabling the largemem option?

[a1880]

358,404,470 is 2^28.41 and therefore beyond the limit.

The high number of clauses is problematic. I don't have CNF examples with more than 200,000 clauses.
Have a look at this related issue.

Unless you have a system of XOR equations which can be readily solved via Gaussian elimination, chances to find a solution appear to be rather slim. But this is just a gut feeling.

[msoos]

Hi, Thanks Alex for the answers! Regarding the problem: you need to think about how you encoded your problem. It's almost surely suboptimally encoded. Likely some quadratic encoding instead of a more tricky but linear or sub-linear encoding. I strongly suggest to look at your encoding and try encoding it better. No solver will be able to solve that thing the way it's encoded. Mate

…

On Tue 12. Nov 2024 at 05:24, Axel Kemper ***@***.***> wrote: 358,404,470 is 2^28.41 and therefore beyond the limit. The high number of clauses is problematic. I don't have CNF examples with more than 200,000 clauses. Have a look at this related issue <#537>. Unless you have a system of XOR equations which can be readily solved via Gaussian elimination, chances to find a solution appear to be rather slim. But this is just a gut feeling. — Reply to this email directly, view it on GitHub <#774 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKF4OPZ7RZQLT7GBDBAFVD2AEVAZAVCNFSM6AAAAABRR7KJ76VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDINRZGE4DQOBSGU> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>