Tag Archives: binary clauses

How to bit-stuff pointers

SAT,

In my last post I have described a small problem I had regarding a C++ union that had to store a pointer and a value at the same time, plus an indicator that told us which of the two was active:

class WhatLeadHere {
public:
    bool wasPointer;
    union{Clause* pointer; uint32_t lit;};
};

Martin Maurer has wrote this enlightening email regarding this:

The Clause * pointer is [..] located at least on a 4 byte boundary (at least when not forced by e.g. #pragma). If it is not at least on a 4 byte boundary, CPU must (at least some of them) do two accesses: one lower DWORD, one upper DWORD, and merge both together, which reduces speed.

So the lower two bits are always zero :-) Why not move the “wasPointer” to lower two bits (i think you need only one, have one spare bit). Of course before accessing the “pointer” (Clause *), you must “and” the two lower bits back to zero.

He is perfectly right: the pointer will never be zero on the least significant bit (LSB), so setting that to “1” can be used as an indicator. This is a form of bit-stuffing. To check if it’s a pointer or a literal the following function can be used:

const bool WhatLeadHere::wasPointer() const
{
   return (lit&1);
}

As for storing lit, we need to right-shift it by one and set the LSB to 1. When lit is needed, we left-shift it to get back the original value. This is not a problem, since variables in SAT never use out the 32-bit space: there are rarely more than 10 million variables, so right-shifting this value will not lead to information loss.

Propagating binary clauses

SAT, ,

Binary clauses are somewhat special. They are clauses that look like:

-v1 or v20 = true
-v1 or v21 = true

which basically mean: if v1 is TRUE, then both v20 and v21 must be TRUE. We put these clauses into a special datastructure, that looks like this:

watchlist[-v1] = v20,v21, ...

This makes us all very happy, since this datastructure is very simple: just literals (negated or non-negated variables) one after the other, in a very trivial list. This makes the whole thing very compact, and very efficient.

The problem with such a list is that when v1 is indeed set to TRUE, then when we set the variables (e.g. v20,v21), we must record what set these variables to their new values. What usually is done is to simply record the pointer to the clause that does this. However, in the above datastructure, there are no clause pointers. The datastructure for GLUCOSE contained these pointers. I have lately been experimenting with removing these pointers. The tricky part is to update the conflict generation routine that examines the clauses and decisions that lead to a conflict. This routine must now automatically recognise that these binary clauses are special, and they are only 2-long: one part of them is the variable that got set, and the other part is the variable that set it. These two informations are available: watchlist[-v1] immediately tells us that literal -v1 set the variable, and the variable that got set is always known.

Armed with this logic, one would think that moving towards this all-new no-clause-pointers heaven is the way to go. However, apparently, this might not be so. This is quite astonishing, given that doing things without pointers should mean less cache-misses (since pointers are less likely to be resolved during conflict analysis). I consistently get worse speeds, though. I am guessing that the problem lies with the datastructure I use to store the information stating what lead to the setting of the variable. I use a very simple struct:

struct WhatLeadHere {
    bool wasPointer;
    union{Clause* pointer; Lit lit;};
};

where wasPointer is TRUE if a non-binary clause lead here (and we store the pointer), and FALSE if it was a binary clause (and we store the other literal). The union takes care of the rest: pointer is valid when wasPointer is TRUE and lit is valid when wasPointer is FALSE.

What is apparent in this datastructure is the following: we now store a 32/64 bit pointer plus we store a boolean. Right, so 42/72 bits of data? No. Data alignment in C++ means, that this datastructure will be aligned according to its largest member, so it will be aligned to 32/64-bit boundaries: this datastructure takes 128/64 bits to store on 32 and 64 bit architectures, respectively. Oops, we just doubled our demand of data writes!

There are some remedies, of course. We can simply pack:

#pragma pack(push)
#pragma pack(1)
struct WhatLeadHere {
    bool wasPointer;
    union{Clause* pointer; Lit lit;};
};
#pragma pack(pop)

which removes the memory burden of aligning to maximum size, and the actual size will really be 42/72 bits. But this reaises the overhead of accessing data inside this structure. Furthermore, I have been using a 32-bit mini-pointer on 64-bit architectures, which is a big hack, so it crumbles as soon as something as complicated as this comes up: so I am left with writing 72 bits instead of 32. This probably leads to the slowdowns. Oh well, I have got to work harder…

EDITED TO ADD: Next up, I will talk about some new ideas that let me solve 217 problems from the 2009 SAT Race within the original time limit. Remember that last year the best solver only solved 204.

The Obvious Child

SAT, ,

The new CryptoMiniSat 2.5.1, codenamed “The Obvious Child” has been released. It’s very close to the system that has been sent into the SAT Race’10. This version of CryptoMS is much better than any versions before: I finally corrected a lot of bugs that went into the 2.4.x series, and added new features to treat binary clauses.

The release name is the song title by Paul Simon. I am a fan of the 60’s for many reasons. It was the time when Laing wrote his first books, empathy was first scientifically demonstrated for animals, the days of I have a dream, the landing on the moon, and the take-off of Simon&Garfunkel.; Some interesting times, shall we say.

I probably will be working less on CryptoMiniSat from now on, instead concentrating on other things that I must do, such as publishing research papers on subjects that interest the scientific community. I will also be trying to play out in my mind how CryptoMiniSat will fare in the SAT Race. Of course I am hoping for the best, but I worked on the program for a mere 8 months, alone. Comparing this to some experts working on their solvers for multiple years in groups of 2-3, I really have no chance of winning. However, I am optimistic, as always: maybe I will get some good position in the rankings :)

Being dumb is part of the deal

SAT,

In my last post, I presented a fast and easy way to add binary clauses to the clause database of SAT solvers, and I conjectured that since the algorithm was so simple, there must be something wrong with it. I was, in fact, right. I ran a cluster experiment, and it turned out that adding all those binary clauses was slowing down the solving.

My first reaction was of course: how on Earth? Binary clauses are “good”: both MiniSat and Glucose try to amass these clauses as much as possible. So what can possibly be wrong? Well, redundant information, for a start. Let’s assume that we know that

A leads to B
B leads to C

If I now tell you that

A leads to C

it wouldn’t really help you. However, the algorithm I presented last time didn’t address this issue. It simply added a good number (though, luckily, not all possible) binary clauses that were totally redundant.

The trick of adding binary clauses is, then, to add as little as possible to achieve maximal graph connectivity. And, while we are at it, we can of course remove all redundant information like the one I presented above. Neither of these two are easy. I use the Monte-Carlo method to approximate the degree of vertexes for the first algorithm, and then sort vertexes according to their degrees when adding binary clauses. The second algorithm just needs a bit of imagination and a will to draw graphs on a piece of paper.

So, there is a point in being dumb: without the hands-on knowledge how binary clauses negatively affect problem solving, I would never have thought of developing such algorithms. The final algorithms take ~3-4 seconds to complete, add (fairly close to) the minimum number of clauses, remove all redundant clauses, and work like a charm.

There is only one thing to understand now: why does Armin Biere add hundreds of thousands of binary clauses? I seem to be able to achieve the same effect in a couple of thousand… Again, I must be dumb, and he must be doing something right. I am lost, again :(

EDITED TO ADD: You might enjoy this plot of PrecoSat236 vs. CryptoMiniSat 2.5.0beta1 on the SAT Competition instances of 2009.

I must be dumb

SAT, ,

Apparently, hyper-binary resolution is not easy. However, I have been reading the paper by Gershman and Strichman, and they make it sound like it’s the easiest thing of all — especially if you don’t do it the way they are doing it, of course.

Hyper-binary resolution is essentially very easy. Let’s say you have three clauses:

-a V b
-a V c
d V -b V -c

(where V is the binary OR, - is the binary negation, and each line must be satisfied)

If we set a=true and propagate this, then we get to the result that d=true. Which can be coded down as the clause:

-a V d

More interestingly, this new clause actually helps: if you only use the original 3 clauses, and you set d = false and propagate, nothing happens. However, if you add the new clause to the clause list, then a=false propagates automatically.

The way these kind of new binary clauses (like -a V d) could be found has been done before as follows:

  1. Build graph from binary clauses: literals are vertices and there are edges between vertices a and b if there is a binary clause -a V b
  2. Set a=true and propagate
  3. Check if every propagated fact can be reached starting from the vertex corresponding to a in the graph. If it cannot be reached, add the binary clause that represents the edge.

One can say that this algorithm works perfectly. But I am a lazy coder, and I don’t want to implement a graph library into CryptoMiniSat. What’s there to do then? Well, we can achieve the same thing with data structures already present in all modern solvers!

The trick to use is that binary clauses are propagated in a very different manner than normal clauses: they have their own watchlists, and propagating binary clauses is extremely fast. So, instead of trying to fiddle with some overoptimised graph library, we can simply write a routine, called propagateBin(), which only propagates binary clauses already inside the code. We then compare the propagate() and the results of propagateBin() and if something is missing, we add it.

In fact, implementing this algorithm using the above trick is trivial. No use of graph libraries, nothing to do really, just write a 20-line propagateBin(), which itself is just a copy-paste of the first couple of lines of propagate() . A very short side-note: it’s also very fast. We can find 100’000 binary clauses in less than 0.1 seconds. Here is the commit that implements this in CrptoMiniSat. I think it makes sense even for those unfamiliar with the code.

Finally, why am I dumb? Because there must be something amiss here. I can’t believe that people much more knowledgeable in the subject didn’t come up with this idea before. So, they must have, and probably already published it, or, the idea must be really bad, missing elements or is incomplete. If it is complete, however, then hyper-binary resolution is once and for all fast and efficient. Can’t wait for someone to prove me wrong.