Propagating faster | Wonderings of a SAT geek

# Propagating faster

July 26, 2010 SAT BCP, binary clauses, Optimisation msoos

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.