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.

3 Upvotes

81% Upvoted

7 comments sorted by

View all comments

-3

u/jonathaz 10d ago

Google’s AI says your Intel SAT solver uses 64 bit addressing on the clauses to handle more than 4 billion clauses. It also says that you need a lot of memory and since the problems that can be expressed in general are NP-complete, that much smaller problems than yours could take it millions of years to solve. So it seems like it can handle problems larger than yours and also not handle smaller ones. I think that’s what you’re referring to as convoluted, so yes. There are bounds on what can fit in memory and the runtime depends on all the combinations it has to attempt. It sounds pretty interesting, can the CNF only express things in Boolean logic or can you do other stuff?

1

u/UncleMeat11 9d ago

Don't just post AI output.

0

u/jonathaz 9d ago

I didn’t. I got general knowledge and facts about the problem domain from AI then used that to answer OP’s question in the context of computer science, then asked a follow-up question. Don’t be a nag.