search

msoos / cryptominisat

An advanced SAT solver
https://www.msoos.org
Other
824 stars 184 forks source link

Error: Variable Limit Exceeded in Large CNF #774

Open HariNarayana123 opened 2 weeks ago

HariNarayana123 commented 2 weeks ago

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 commented 2 weeks ago

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 commented 2 weeks ago

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 commented 2 weeks ago

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 commented 2 weeks ago

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 https://github.com/msoos/cryptominisat/issues/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 https://github.com/msoos/cryptominisat/issues/774#issuecomment-2469188825, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKF4OPZ7RZQLT7GBDBAFVD2AEVAZAVCNFSM6AAAAABRR7KJ76VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDINRZGE4DQOBSGU . You are receiving this because you are subscribed to this thread.Message ID: @.***>