SAT solving with more than 2^32 clauses

Question

I'm trying to solve a big CNF formula using a SAT solver. The formula (in DIMACS format) has 4,697,898,048 = 2^32 + 402,930,752 clauses, and all SAT solvers I could find are having trouble with it:

• (P)lingeling reports that there are "too many clauses" (i.e. more clauses than the header line specifies, but this is not the case)
• CryptoMiniSat4 & picosat claim to read the header line as saying 402,930,752 clauses which are 2^32 too few
• Glucose seems to parse 98,916,961 clauses and then reports to have solved the formula as UNSAT using simplification, but this is unlikely to be correct (an initial segment of the formula this short is very likely to be SAT).

Is anyone aware of a SAT solver that can handle files this large? Or is there something like a compiler switch that can sidestep this sort of behaviour? I believe all solvers are compiled for 64bit linux. (I'm a bit of a noob when it comes to handling numbers this big, sorry.)

Answer 1

I'm the developer of CryptoMiniSat. In most cases where the CNF is so huge, the issue is not the SAT solver but that the translation of the original problem into CNF wasn't done carefully enough. I assume you didn't write that CNF by hand -- you had a problem which you translated to CNF using an automated tool.

The act of translating a problem into CNF is called encoding and it has a huge literature in academia. It's a whole topic to itself, or more appropriately, whole topics to themselves. Please see the research papers on Constraint Programming (CP), Pseudo-boolean constraints (PB), ANF-to-CNF translation techniques (see crypo workshops/conferences) and electronic circuit encoding (search for AIG, Tseitin encoding and its variants and look at the references). These are the big topics but there are many others. Taking a peek at these will reduce your CNF by at least 3 orders of magnitude, probably more.