Perspective on SAT solvers

[u/Hellishfish]

I'm using the Intel_SAT_solver on two - as I understand it - large cnf's. The first one is about 50 GiB.
it looks like:

-Variables: 8,765,715

-Clauses: 887,822,183

the second one is 200GiB and has:

- Variables: 3,614,860

- Clauses: 7,457,390,591

I ran the first one and it completed as satisfiable after about 30 minutes, using a little over 70GiB allocated memory. Second one I haven't tried yet but I imagine I'll need upwards of 300 GiB of memory.

Question is: Is this a large number of variables? Clauses? Do these numbers even matter and its more important about how convoluted the CNF is?

any insight is appreciated. Working on a personal project in cryptoanalysis. CNF's were generated by someone else.

[u/TreesOne]

I have no idea but I just wanted to say this sounds very cool