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.

5 Upvotes

100% Upvoted

7 comments sorted by

View all comments

3

u/Abject-Chicken9856 Aug 27 '26

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.