Category Archives: SAT

Asymmetric branching

SAT,

Asymmetric branching is an algorithm that shortens CNF clauses in SAT Solvers. A clause, for instance v1 V v2 V v3 V v4 (where letters are binary variables and V represents binary OR) could possibly be shortened to v1 V v2 V v3. To find out if it can be, all we have to do is to put -v1,-v2 and -v3 into the propagation queue and then propagate. If we receive a conflict from the propagation engine, we can learn the clause v1 V v2 V v3, which (incidentally, though this was the point), subsumes the original clause, so we can simply remove variable v4 from the original clause.

Ok, so much for theory. Now comes the hard part: how do we do this such that it actually speeds up the solving? The problem is that asymmetric branching, when done on all possible clauses, is slow. However, its benefits could be large, since a shortened clause naturally leads a faster propagation and shorter resolution proofs thus less propagation need.

I have been experimenting in getting some benefit from asymmetric branching, and now it works extremely well for CryptoMiniSat. The trick I use, is that I first sort the clauses according to size, and only try to shorten with asymmetric branching the top couple of clauses. This ensures that the largest clauses are shortened first. Since the largest clauses contribute most the to size of the resolution proof and they are the slowest to propagate, this makes sense.

CryptoMiniSat tries to do asymmetric branching regularly, always for only a little while (~2 seconds). I believe this is useful, because as the amount of time the program has been trying to solve a problem increases, it makes sense that we have a bit more time to do things that could help resolve the problem faster. For instance, if CryptoMiniSat has been trying to solve a given problem for 30 minutes unsuccessfully with the standard clause-learning DPLL procedure in vain, we can allocate 2-3 seconds to possibly gain ~5-10% later. In the example case it can be assumed that since we haven’t been able to solve it for 30 minutes, probably we won’t solve it in the next 10 minutes, so gaining 5% on 10 minutes is 30 seconds, far more than the 2-3 seconds we invested.

The results with asymmetric branching with CryptoMiniSat are quite astounding. Using the 2009 SAT Competition benchmark set with an approximately correct timeout, CryptoMiniSat could normally solve 217 problems. With asymmetric branching, CryptoMiniSat can now solve 220 — a huge increase: last year, 16 solvers running in parallel could only solve 229 instances in total.

Edited to add (26/09/2010): Clause Vivification by Piette, Hamadi and Sais is a paper about the above described method, though with a number of key differences. The paper seems to advocate for a complete procedure, furthermore, it calls the conflict generation routine in certain cases. I believe that the above described way of carrying out this technique brings more tangible benefits, especially for larger problems.

(Updated: we need to branch on the inverse of the clause’s literals. Thanks to Vegard Nossum for spotting this)

Propagating faster

SAT, ,

Propagation (BCP) in SAT is the single most expensive operation. The algorithm essentially does the following:

while (queue_head < trail.size()) {
  Literal p = trail[queue_head];
  vector<Watch>& thiswatch = watches[p];
  for (i = thiswatch.begin(); i!=thiswatch[p].end(); i++) {
    confl = prop_confl(i->clause);
    if (confl != NULL) return confl;
  }
  queue_head++;
}

where the function prop_confl() executes the propagation or returns a conflict, if necessary.

The problem with the above function is that clauses come in all shapes and sizes. In CryptoMiniSat, there are two kinds of clauses, normal clauses and XOR clauses. Naturally, these need to be handled differently. Furthermore, if the clause’s size is small, it is more efficient to handle it differently. The way CryptoMiniSat has done this before was to have a separate “watches” for each of these. As you can guess, this is very suboptimal.

The new code in CryptoMiniSat now uses a different approach. Instead of having a watches_normal, watches_xor, watches_binary, and a for loop for each, we have one watches and one for loop, but this time, the struct Watch encodes the type of the watched clause. So our new BCP function is:

while (queue_head < trail.size()) {
  Literal p = trail[queue_head];
  vector<Watch>& thiswatch = watches[p];
  for (i = thiswatch.begin(); i!=thiswatch.end(); i++) {
    if (i->isBinary())
      confl = prop_confl_bin(i->clause);
    if (i->isNormal())
      confl = prop_confl_norm(i->clause);
    if (i->isXor())
      confl = prop_confl_xor(i->clause);
    if (confl != NULL) return confl;
  }
  queue_head++;
}

This new method reduces the jump-around that the processor otherwise would have done with all those separate for loops. It has an important drawback, though: it is now more complicated (and more expensive) to fully propagate binary clauses before any other clause. The original code had this:

while (queue_head < trail.size()) {
  bin_queue_head = queue_head;
  while(bin_queue_head < trail.size()) {
    Literal p = trail[bin_queue_head];
    vector<Watch>& thiswatch_bin = watches_bin[p];
    for (i = thiswatch_bin.begin(); i!=thiswatch_bin.end(); i++) {
      confl = prop_confl_bin(i->clause);
      if (confl != NULL) return confl;
    }
    bin_queue_head++;
  }
  Literal p = trail[queue_head];
  vector<Watch>& thiswatch = watches[p];
  for (i = thiswatch.begin(); i!=thiswatch.end(); i++) {
    confl = prop_confl(i->clause);
    if (confl != NULL) return confl;
  }
  queue_head++;
}

Since there are no separate watchlists for binary clauses anymore, we are required to go through all clauses all the time in the first for loop, or we can simply skip the first loop. The disadvantage of this is that some variables could have possibly been set by binary clauses may now be set by non-binary clauses, which leads to a possibly increased number of literals in the resulting learnt clause — since the incoming arcs into the conflict will likely contain more clauses that are larger than 2-long.

Stats on CryptoMiniSat’s development

SAT, ,

I have just discovered the gitstats tool, and quickly put together a set of statistics on the development of CryptoMiniSat, the SAT solver I have been working on lately. I have been using the GIT repository for most of my work on CryptoMiniSat, doing ~2000 commits since its inception, so it gives a good picture of how things evolved, and how I usually work. Firstly, the hours I usually work:

I basically work almost as much at midnight as I do at midday. The afternoon is clearly the most active and practically useful part of my day. Next, the graph to show which days I work the most:

Essentially, I worked as much on CryptoMiniSat during Sunday as I did during Monday or Friday. Saturday was the day I must have been the most fed up with development. Finally, the number of commits by months:

The 2nd and 3rd months of 2010 was a struggle because of the SAT and PoS deadlines. I tried to put together a credible research paper, which finally got accepted at PoS. During the 6th and 7th months of 2010 I was mostly looking forward to the results of the SAT Race, so I wasn’t developing so much.

Winning the SAT Race

Personal, SAT

The software I developed, CryptoMiniSat 2.5 won the SAT Race of 2010. It is a great honour to win such a difficult race, as there were 19 other solvers submitted from 9 different countries.

Thinking back and trying to answer the question why CryptoMiniSat won, I think there are no clear answers. Naturally, I put immense effort into it, but that is only one part of the picture. Other important factors include those who supported me: my fiancée, the PLANETE project of INRIA, and in particular Claude Castelluccia and my colleagues here in Paris, the LIP6 team and my professor here, Jean-Charles Faugere. As with all randomised algorithms, luck played a good part of winning, too.

In all of this, it is interesting to note that I never had a colleague who worked in or even near the field of SAT: both the PLANETE and the LIP6 team use SAT solvers only as a means to an end, not as an end in itself. In other words, I had to get this far mostly alone. To be honest, I think this is one of the reasons I had won, too: there probably is too much misunderstanding in SAT that everybody takes for granted. Since I never really talked with anyone about their understanding of the subject (I only read papers, which state facts), I had a white paper in front of me, which I could fill with my own intuitions, without being lead by those of others. Naturally, this means that I have probably stepped into a large number things that are widely understood to be wrong, but at the end, it seems that I must have also made some good steps, too.

As for the bad steps I have made (and of which I am aware of), I had copied the subsumption algorithm from SatElite, which the authors of MiniSat told me was a bad move, since its self-subsuming resolution is slow. I had in fact observed this, but I thought it was a fact of life. Alas, it isn’t. Other errors I have made include a non-portable pointer-shortening which shortens pointers to 32 bits when using 64-bit architectures (Armin Biere’s lingeling does this right), and a wrong clause-prefetching code that Norbert Manthey put me right about. I have also conceptually misunderstood the possible impact of variable elimination on the difficulty of resolving an instance, a grave mistake that Niklas Sörensson put me right about.

As for the good steps, I think I have made a couple of them. Firstly, I have put the 2009 SAT paper we wrote with my colleagues to its natural conclusion: including XOR clauses and partial XOR reasoning into the innermost parts of the solver. Secondly, I have used the community to its fullest potential: CryptoMiniSat was used by the constraint solver STP far before the SAT Race began, and it was distributed to a number of highly skilled individuals who made use of it and gave feedback. Sometimes I got very negative feedbacks (these were the most valuable), which highlighted where and why the solver was failing. Thirdly, I have tried to take advantage of the academic environment I work in: I have tried to read the relevant papers, used the clusters provided by the French universities to carry out experiments, and generally took my time (rarely an option in industry) to get things right instead of rushing out a solver.

The 2010 SAT Conference

Personal, SAT,

I am currently at the SAT 2010 conference, in Edinburgh. It is my second SAT conference, but the first one where I finally have a chance to know who is who. I had a chance to talk to some great researchers. For instance, I talked to (in no particular order) Armin Biere (author of PrecoSat and Lingeling), Niklas Een, Niklas Sörensson (authors of MiniSat — new version is out, btw), Marijn Heule (author of the march_* set of solvers), Matti Järvisalo (one of the authors of Blocked Clause Elimination), the author of MiraXT, and many others. It’s really a great place to meet up people and get a grasp on what SAT is really about. It’s also a great way to understand the motivation behind certain ideas, and to hear the problems encountered by others.

For instance, I now know that bugs, about which I have already written a blog post about is a problem that comes up for nearly everyone, and tackling them is one of the most difficult things for the developers. I have also finally understood the reason behind the MiniSat Template Library (MTL), which I’ve always found odd: it re-implements many things in the STL (the Standard Template Library), which I have always found unnecessary. Although the reasons are now clear (better control, easier debugging, less memory overhead), I think I will still replace it with STL. I have also had a chance to talk to the kind reviewer who did such an extensive review of my paper, which was quite an enlightening discussion. If you are interested in SAT, I encourage you to attend next year: there are usually some workshops associated with the conference, where it is easier to have a paper accepted: e.g. this year, a Masters student got his quite interesting paper (long version) accepted, and I am sure he has benefited a lot from it.