SAT solving with more than 2^32 clauses

10
votes

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.)

1
cinteger-overflowsat-solverssat
Maybe you can try a distributed SAT-solver. – John Coleman
Are these OSS? You could modify them to use 64b integers. – Jeff Hammond
@Jeff: yes, they are all open-source C or maybe C++, don't know how to tell the difference. – Dominik Peters
Doesn't matter. Integer types are the same :-) – Jeff Hammond
Building with 64-bit ints isn't likely to do much good in the end, because DPLL-based solvers are notoriously bad on really large SAT instances. Stochastic solvers are better but even among those I've never heard of one tackling a formula with over four billion clauses. – Kyle Jones

1 Answers

6
votes

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.