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/Abject-Chicken9856]

Those are definitely large instances in practical SAT-solving terms, especially the second formula with more than 7 billion clauses. However, the number of variables and clauses alone does not determine how difficult an instance will be.

The structure of the CNF can matter even more. For example, solvers may handle a very large formula quickly if propagation, preprocessing, or learned clauses simplify it effectively. On the other hand, a smaller formula can be extremely difficult if it has a structure that forces extensive search.

It is also worth looking at factors such as:

• Clause-to-variable ratio
• Distribution of clause lengths
• Amount of redundancy
• Whether the formula is satisfiable or unsatisfiable
• How much unit propagation and preprocessing can reduce it

Your first result is a good example: around 30 minutes for a formula of that size suggests the solver was able to exploit useful structure. For the second instance, memory usage may increase substantially, but runtime and memory will not necessarily scale proportionally with file size.

[u/TreesOne]

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

[u/steohan]

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.

[u/noop_noob]

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.

[u/jonathaz]

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?

[u/UncleMeat11 → u/jonathaz]

Don't just post AI output.

[u/jonathaz → u/UncleMeat11]

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.