Category Archives: SAT

Could monomials be handled natively from SAT solvers?

SAT,

I recently got a question that intrigued me:

I am new to this SAT solving world but I was wondering whether you thought considerable speedups were possible for crypto type problems (multivariate polys over GF(2)) by simply never converting the problem to cnf at all and thereby avoiding the combinatorial explosion that results in the conversion process. That is using the original xor formulation.

First of all, the question is a follow-up to xor-clauses: they implement XOR-s natively. Using them avoids a number of problems relating to the increase of variables. Why not implement monomials (i.e. “a*b” or “a*b*c”, where “*” is binary AND and variables are binary) natively? They are the only thing left to do. Personally, I am not overly optimistic about them, though. Let me got through some of my reasons here.

Firstly, the “exponential explosion” expressed in the question is in fact much less existent than people tend to think. The reason is that the intelligent variable activity heuristics, unit propagation, and conflict generation tend to take care of a lot of potential problems. Since the propagation of a variable will entail the propagation of many others (it depends, for crypto, around ~100), there is no real explosion, since there is not really 2^n, but more like 2^(n/100) combinations that need to be explored. This argumentation takes away some of the potential benefits that native monomials could bring.

The real problem, though, is the following. By moving monomials into cryptominisat and thus potentially speeding up the solving, conflict generation could become much more complex. So, if moving to an internal monomial representation entails making a mess of conflict generation, then using monomials internally may only make the solving slower.

Another reason that native monomials may not speed up solving so much, is that a lot of clauses inserted when converting monomials are binary clauses, which are extremely well dealt with in the CNF world — it would be hard to do it any better.

As a last, but very minor point, using monomials would increase the complexity of the program, which would mean not only a lot of man-hours lost debugging it, but also a loss of performance due to a (probably non-negligible) increase of instruction cache misses.

Oh well, so those are my reasons. I would be interested if someone has some comments on these, though.

CryptoMiniSat v2

SAT

Lately, I have been working a lot with CryptoMiniSat, to get it up and running for the 2010 SAT Race, held by Carsten Sinz. Getting CryptoMiniSat fast and bug-free has been a long and winding road. I can now understand the difficulty of choosing magic parameters that these SAT solvers make use of regularly. As I have added ~6000 lines of code to a codebase of ~1500, you can probably imagine the number of magic constants that I had to come up with. Worst of all, these constants interact in non-intuitive and sometimes in a fully “magical” manner.

To test my choice of magic constants, I have been running experiments on the Gird5000 project of French universities. It is quite easy to get access to Grid5000 if you work in a French university, and it is surprisingly easy to run experiments. On the other hand, interpreting the results of such experiments is not so easy :) However, CryptoMiniSat is coming along. On crypto examples I think we are unbeatable. When it comes to other examples, we are good, but we will see how the new MiniSat (yes, it’s coming!) and precosat will do. Apparently, the GLUCOSE people are also planning to enter the competition, so the race will be very interesting. Fingers are crossed that CryptoMiniSat will finish somewhere in the top 3 :)

There are some “secret” improvements that I have made the past couple of months, and there are some open secrets. I tried to incorporate the GLUCOSE restart heuristic, and XORs are automatically detected (XOR clauses are no longer neccessary, but they are of course supported!). This means that CryptoMiniSat is now a plug-and-play experience for all the crypto-folks. I have tested the solver with a good number of crypto problems, and the speedup relative to MiniSat is on the order of 2-50x, depending on the problem.

The new CryptoMiniSat will be released when the SAT Race starts and everyone’s executables have been freezed. I will then detail all the new features. Until then, let me just run a couple of more experiments on that cluster :)