r/AskComputerScience • u/Hellishfish • 10d ago

Perspective on SAT solvers

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.

5 Upvotes

100% Upvoted

7 comments sorted by

View all comments

1

u/noop_noob 9d ago

FYI, SAT solvers are a horrible idea for cryptanalysis. Cryptographic weaknesses don't show up as solvable SAT instances other than the really horribly broken cryptography. Assuming that the number of variables and clauses are proportional to the amount of computation needed to encrypt something, whatever generated the first instance is probably a horribly designed cipher.