All posts by msoos

Transitive OTF self-subsuming resolution

SAT, ,

The title may be a bit long, but its essence is very simple: we try to shorten learnt clauses. The basic idea was described in this post: there is a clause we just derived, e.g.

d V -e V f V g (1)

where d,e,f,g are binary variables, - is binary negation, and V is the binary OR operator. We can remove a literal from this using self-subsuming resolution with e.g. the 2-long clause:

f V -g (2)

removing g from clause (1). This has been achieved before using on-the-fly self-subsuming resolution. The trick we add now is the following. Let’s assume that clause (2) was not in the clause database. With the above technique, g would not be removed. However, if clauses:

f V a
-a V -g

are inside the clause database, we could, in fact, remove g, since the above two clauses, when we resolve them on a become:

f V -g

i.e. clause (2), what we have been searching for! So, how could we do this kind of reasoning efficiently? It turns out that this is not so difficult. We simply need to try to propagate -f using only the 2-long clauses. Then, we will reach -g through the intermediary, a.

Naturally, we can do the above recursive-propagation process not only for f but for all literals in the original clause (1), and then try to perform on-the-fly self-subsuming resolution, as before. There is only one catch: doing this kind of recursive propagation on all 2-long clauses for all literals in a clause is too time-consuming. So we only do it for clauses that are short: 5 literals or shorter. The results are in, and seem to indicate that transitive on-the-fly self-subsuming resolution with a limit of 5-long clauses is indeed viable:

The set of problems used were those of the SAT Competition 2009, and the time limit was 1500 seconds on some powerful machines — they are approx 2x as fast as those used in the competition. As you can see, transitive OTF self-subsuming resolution seems to pay off in terms of number of problem instances solved within a certain time limit. I have decided to add this feature to the upcoming CryptoMiniSat 2.6.1, which should be ready soon.

anf2cnf script released

SAT, , ,

I have finally managed to fix the script that converts ANF problems to CNF format in the Sage math system. The original script was having some problems that I blogged about. The new script has corrected most of the shortcomings of the original script, as well as added some textual help for the user.

For instance, the equations

sage: print two_polynoms
[x0*x1 + 1, x0*x1 + x1]

that last time required 13 clauses and 4 variables in CNF, now look like this:

sage: print anf2cnf.cnf(two_polynoms)
p cnf 3 6
c ------------------------------
c Next definition: x0*x1 + 1
3 0
c ------------------------------
c Next definition: x0*x1 + x1
3 -2 0
-3 2 0
c ------------------------------
c Next definition: monomial x0*x1
1 -3 0
2 -3 0
3 -1 -2 0

which is 1 variable and 7 clauses shorter than the original, not to mention the visually cleaner look and human-parseable output. The new script is available here. Hopefully, some of my enhancements included in the Grain-of-Salt package will be included in this script. The problem is mainly that Grain-of-Salt uses radically different data structures, and is written in a different programming language, so porting is not trivial.

anf2cnf hell in Sage

SAT, ,

There is an ANF (Algebraic Normal Form) to CNF (Conjunctive Normal Form) converter by Martin Albrecht in Sage. Essentially, it performs the ANF to CNF conversion that I have described previously in this blog entry. Me, as unsuspecting as anyone else, have been using this for a couple of days now. It seemed to do its job. However, today, I wanted to backport some of my ideas to this converter. And then it hit me.

Let me illustrate with a short example why I think something is wrong with this converter. We will try to encode that variable 0 and variable 1 cannot both be TRUE. This is as simple as saying x0*x1 = 0 in plain old math. In Sage this is done like this:

sage: B = BooleanPolynomialRing(10,'x')
sage: load anf2cnf.py
sage: anf2cnf = ANFSatSolver(B)
sage: polynom = B.gen(0)*B.gen(1)
sage: print polynom
x0*x1

So far, so good. Let’s try to make a CNF out of this:

sage: print anf2cnf.cnf([polynom])
p cnf 4 6
2 -4 0
3 -4 0
4 -2 -3 0
1 0
4 1 0
-4 -1 0

Oooops. Why do we need 6 clauses to describe this? It can be described with exactly one:

p cnf 2 1
-1 -2

This lonely clause simply bans the solution 1 = TRUE, 2 = TRUE, which was our original aim.

Let me just mention one more thing about this converter: it repeats definitions. For example:

sage: print two_polynoms
[x1*x2 + 1, x1*x2 + x1]
sage:  print anf2cnf.cnf(two_polynoms)
p cnf 4 13
2 -4 0
3 -4 0
4 -2 -3 0
1 0
4 0
2 -4 0
3 -4 0
4 -2 -3 0
1 0
4 2 1 0
-4 -2 1 0
-4 2 -1 0
4 -2 -1 0

Notice that clause 2 -4 0 and the two following it have been repeated twice, as well as the clause setting 1 to TRUE.

I have been trying to get around these problems lately. When ready, the new script will be made available, along with some HOWTO. It will have some minor shortcomings, but already, the number of clauses in problem descriptions have dramatically dropped. For example, originally, the description of an example problem in CNF contained 221’612 clauses. After minor corrections, the same can now be described with only 122’042 clauses. This of course means faster solving, cleaner and even human-readable CNF output, etc. Fingers are crossed for an early release ;)

Reinventing the wheel

SAT

I have lately been describing two techniques to speed up SAT solving: on-the-fly self-subsuming resolution, and an interesting way to apply asymmetric branching. It turns out, the first was already used in PrecoSat (by Armin Biere) under the name “strong minimization”, and the second was already published as Vivification by Piette, Hamadi and Sais. As far as I could tell, both optimisations bring tangible benefits to SAT solving. I have tried solving the problem instances of the 2009 SAT competition with and without both optimisations, and it turns out that using both is the fastest.

Of course I am at fault for not knowing that these techniques have been published before. Maybe both have been published in respected journals/conferences, but I don’t seem to have the capacity to read every journal and conference article. I think we can safely assume that this is true for most researchers. So are we forever destined to reinvent the wheel? Probably the only techniques that don’t need to be reinvented are those that have been demonstratively shown to work well. Such a technique is for example glue-clauses, or variable elimination (VE). Glucose, the solver based on glue-clauses had won the 2009 SAT competition, and VE in the SatELite preprocessor blew away the 2005 SAT competition. Similarly, xor clauses might end up in mainline SAT solvers due to the win of CryptoMiniSat (even though I think that win was due to far more than just that).

This leads us to a somewhat dim conclusion, however: useful, but small techniques might get lost forever (if they are not reinvented). This is sad, because lots of small techniques bring about lots of improvements in the end, especially if they work together. For example, both techniques mentioned above lead to smaller clauses, which in turn lead to more binary and tertiary clauses. These binary and tertiary clauses lead in turn to increased solving speed due to modern solvers which keep both of them natively in the watchlists. So, as the technology changes, the smallish benefits that some techniques gave might increase due to the technical advancements that have been made since.

FPGA programming and SAT

SAT, ,

I have lately been trying to implement a cryptographic protocol (CryptoGPS) on an FPGA. First impressions are that VHDL is a difficult language, but once understood, it’s not all that difficult to work with it. It took me ~2 weeks to get a hold on the language, but now it feels relatively easy to program in it. I have been looking forward to getting down and dirty with FPGAs, because it’s one of my long-term goals to somehow integrate SAT solvers with FPGAs.

SAT solvers are extremely versatile tools that can resolve a number of very complex issues with relative ease. FPGAs are also extremely versatile (essentially,  they are reprogrammable hardware), and are very fast. Making once piece out of these two is like merging Batman with Superman. The trick is, of course, how to merge them? The problem with merging is that FPGAs are typically very good at executing a (preferably small) set of instructions over and over again on a relatively small dataset, while SAT solvers usually deal with large datasets, and execute an excruciatingly complex set of instructions on them over and over again.

I think a way to resolve this issue could be to use the FPGA as a sort of oracle for the SAT solver. The solver is running on a normal computer and at the same time it is connected to an FPGA that awaits its orders. The SAT solver regularly extracts a small set of constraints from its constraint database, sends it to the FPGA, which tries every possible combination of the variables, and sends back the result to the SAT solver. While the FPGA works its wonders, the SAT solver could be executing the normal SAT procedure, and regularly process the incoming data from the FPGA.

The FPGA could simply try every single combination of every variable setting on the clauses it received, and return compact information such as: “variable 5 must be TRUE” or “there is no solution”. More complex return values, such as “variable 10 is always equal to variable 2” could be returned, but it would make for a more complex VHDL design, leading to an overall slowdown. The simplier the logic, the more we can fit on a given FPGA, which means more parallelisation, and therefore a speedier solution overall. Since the number of variables in the clauses will be limited (checking for 30 is already at least 2^30 operations), we could store the clauses as constant-length double-bitfields in the FPGA, and use a bitmask for the current variable settings. This could allow for massively parallelised evaluation of clauses.

On the SAT solver side, we need some guiding principles along which to pick the constraints for the FPGA. The usual suspects could be constraints that contain the most active variables, for example. More complex metrics could minimise the number of variables inside the constraints while maximising the number of small constraints they are present in. Other metrics could perhaps concentrate on the current restart branch of the SAT solver, and try to ask the FPGA to prove that below a certain decision level, the current branch cannot contain a solution — this way, we could backjump using the data from the FPGA.

Would this architecture work? I think its performance would depend on whether there is any compact information that the FPGA could extract from the clauses sent to it. This depends on whether there are small “cores” in the problem that contain compact information, and whether we can extract these cores. The existence of such information-rich cores depend on many things. The clauses/variable ratio is one such metric, another would be the number of symmetries in the problem: the more symmetries, the less compact information can be extracted. Cryptographic problems come to my mind when seeing these criteria. They usually have a very high clauses/variables ratio and rarely, if ever, contain symmetries.