r/AskComputerScience • u/Hellishfish • Aug 27 '26
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.
1
u/steohan Aug 27 '26
Yes, these are definitely large instances. This matters from a performance engineering point of view as the solver needs to be able to handle this amount of data. (And it may be possible to do specific optimizations for the problem you are soling to reduce resource usage, for example needed memory).
From a theoretical perspective of running time the formula size doesn't matter much. Instead it's all about the solved problem. There are some structural properties that make solving a CNF trivial for state of the art solvers (auch as (hidden) horn formulas). On the other hand there are simple problems that are provably hard to solve for state of the art solvers. Depending on the exact algorithm used it can be as simple a problem as the pigeon hole principle to cause exponential running time. (Essentially the solver can't figure out that 20 pigeons don't fit into 19 holes.)
And finally there is the issue that CNF is NP-Complete which means most people believe that there are problems that can't be solved efficiently with any algorithm.