Tag Archives: Collaborative effort

Presentation at Hackito Ergo Sum

SAT, , , , ,

The HES’11 event was great: I had the pleasure of listening to some awesome presentations, and to meet some great people. The most interesting presentation from a non-technical point of view was the attacks at the automount feature of Linux, which everybody thinks is completely secure, but is in fact very flawed due to some buggy rendering libraries. It’s quite interesting that almost everyone thinks that their Linux installation is secure, when in fact if Linux was mainstream, viruses would be abound — but Linux is only a minor player, so malicious software is rarely written for it.

My presentation is available here. I tried mostly to demonstrate how SAT solvers work as an element of the technique that can most amply described as:

As the graphics show, the SAT solver is in fact only one player in this environment. As it turns out, it is the very last step after obtaining the cipher, creating equations describing the cipher, and converting the ANF equations into CNF. The best way to create equations from the original cipher is to use the excellent Sage Maths library for this, a tutorial of which is here. Then, the ANF created by Sage can be transcribed into CNF using, e.g. the anf2cnf tool by Martin Albrecht and me. Finally, the CNF must be solved with a SAT solver to recover the key of the cipher. This last step can be carried out by many SAT solvers, such as lingeling or MiniSat, but I prefer CryptoMiniSat, since I am the main developer for that SAT solver, and it is also very convenient to use in this domain due to some domain-specific advantages it has over other solvers. The middle two steps of the diagram are all automated by the Grain-of-Salt tool if you don’t want to use Sage, and it also contains some example ciphers, so you don’t even have to do step no. 1 in case you wish to work on one of multiple pre-defined industrial ciphers.

In case you are interested in the visualisations I used during my presentation, here is the set of tools I used. For the 3D visualisation, I used 3Dvis by Carsten Sinz — it’s a great tool to extract some structure from problems already in CNF. In case you still have the ANF, it contains more structure, though, and so it is more interesting to look at it that way. Unfortunately, that is rarely the case for typical SAT problems, and so one must often resort back to 3Dvis. For the example search tree, I used CryptoMiniSat 1.0 and gnuplot, and for the example real-time search, I used CryptoMiniSat 2.9.0, available from the same place. Unfortunately, CryptoMiniSat 2.9.0 cannot generate a search tree yet, but this eventually will be included, with time — especially if you join the effort of developing the solver. We are always looking forward to people joining in and helping out with various issues from graph generation to algorithm performance tuning, or even just some fun research.

CryptoMiniSat in SAT Competition’11

SAT, ,

I have submitted three versions of CryptoMiniSat to the 2011 SAT Competition, all available here. The releases are commonly called “Strange Night”, after the music track of the same name. Inside the archive you will find 5 binaries and a PDF description. The five binaries are made up of two single-threaded, two multi-threaded, and a unified single- and multi-threaded binary. This latter is called techdemo, as it is more of a technological demonstrator than anything else, and was developed in collaboration with George Katsirelos and Laurent Simon. All versions are collaborative, however, as they all have the hands of some people from the CryptoMiniSat development mailing list on them.

To be honest, I am not overly optimistic of these binaries, especially since I couldn’t get the 3.0 version of CryptoMiniSat ready for the competition, on which I have been working on the past two months. I have tried to backport some features to the 2.9.0 branch to make these releases, and so the resulting executables are pretty unstable. The techdemo version is a broken 3.0 release, as it is missing the signature feature of fully shared clauses between threads. Since I have finally obtained a 4-core CPU — with hyper-threading for 8 “independent” threads — I am all the more optimistic about a fully-shared scheme. The upcoming 3.0 release will be specifically made to work in multi-threaded environments, and will suffer if launched in single-threaded mode. This architectural decision was made because multi-threading nowadays no longer seems optional: it’s a must. On the CryptoMiniSat mailing list, some people are reporting performance on 64-core machines — optimising for single-threaded environment (and having multi-threading as an afterthought) in these times seems like a broken approach.

For those interested in the actual sourcecode of what has been submitted, everything is available from GIT, as usual:

  1. Strange Night1 – single-threaded
  2. Strange Night1 – multi-threaded
  3. Strange Night2 – single-threaded
  4. Strange Night2 – multi-threaded
  5. Tech Demo

Since these are pretty unstable, I wouldn’t use them in a production environment… happy bug-hunting ;)

Visiting Linz

SAT, ,

Lately I had the pleasure of visiting Linz, Armin Biere’s workplace, where I gave a quick talk on SAT solver architectures. To me, it was really interesting to think through that presentation — not because it was entirely new or exciting, but because it recapped on many issues that have been bothering me lately. Namely, that it’s difficult to make a really versatile SAT solver, because the low-level choices that must be made (e.g. watchlist scheme) determines so many things when one must make higher-level architectural decisions such as clause sharing or even something as simple as hyper-binary resolution. As for this latter, thanks to Armin Biere’s thoughts I have finally managed to realise why my hyper-binary resolution was so slow: I lately took the decision not to fully propagate binary clauses before propagating normal (i.e. larger) clauses, which meant that doing hyper-binary resolution was much slower as I had to re-calculate the binary graph. The fact of not fully propagating binary clauses before normal clauses seemed also to influence my much higher-level choice of using cached implications, as they (intuitively, and also in practice) help much more if binary clauses are not fully propagated before normal clauses. This latter influence is interesting to think through, as something this trivial shouldn’t — at least in principle — influence such a high-level decision.

Also thanks to Armin Biere, I have managed to grasp a better understanding of lingeling and its superior watchlist scheme. Some of the architectural elements of lingeling’s watchlist scheme are really interesting, and when they get published I will definitely port some of them to CryptoMiniSat. It seems to use much less space, and stores information in a more cache-friendly manner, aiding the processor in its job. A related, interesting pointer that I have learnt is this paper that originally introduced blocking literals, but also talks about a range of other ideas that can help. All in all, it was great to visit Linz and the group of Armin Biere, as I have managed to learn a lot from him and his colleagues.

CryptoMiniSat 2.9.0 released

SAT,

After a long break, CryptoMiniSat 2.9.0 has finally been released. The Windows executables need this to work, and the Linux binaries need a recent (>=2.6.26) kernel version. The program has evolved substantially since the last release — more than half of its codebase has been changed. It now works in multi-threaded mode, and uses lazy cached implications for all sorts of interesting purposes from simple transitive on-the-fly self-subsuming resolution to very efficient literal dependency analysis. Currently, the program solves ~225 problems from the 2009 SAT Competition examples given the same time and similar computing power. This is a nice improvement over other SAT solvers such as MiniSat (205), PrecoSat (210) or lingeling (207).

Intensive testing has been carried out on this version of the program, to the extent of finding and identifying a new and unknown gcc bug affecting all gcc versions 4.5.0 and later. Many have played part in finding this and other bugs, including, but not limited to, Martin Maurer, Vegard Nossum, Oliver Kullmann, Robert Aston, and others. This release has been made possible thanks to them.

I hope this version of the code will be useful to many, not only end users but also researchers. In fact I decided to release this version (relatively) early to let researchers merge their changes for the upcoming SAT Competition 2011. I am very interested in any and all versions of CryptoMiniSat that will be submitted to the competition. In case you personally want to change it and find something difficult to understand, just drop a mail to the nowadays very active development mailing list. With this release, I can confidently say that CryptoMiniSat is becoming not only a programming project but also a community. If you feel like you could contribute, or you are simply interested in what is going on, join us.

As for the technical details, the new CryptoMiniSat uses OpenMP for mutli-threading which means it is fully platform-independent. During multi-threading we share unitary and binary clauses between threads — the latter is checked for redundancy using lazy cached implications. We use implicit binary clauses, which don’t help as much in terms of memory as I have hoped, but they help immensely for certain operations, in particular with subsumption checks. Literal dependencies are now calculated using the lazy cached implications and the dominating literal with the largest tree is selected as dominant literal for all literals: when picking variables, we pick the dominating literal 50% of the time instead of the original literal. Variable elimination heuristics have also been highly tuned thanks to the much better at-hand statistics due to implicit binary clauses.

Unfortunately, this version doesn’t offer all the things I wanted it to offer: multi-threaded library interface, extended resolution, distributed solving through MPI, unified restart strategy, and others. All of these (except MPI), and more are however available from the public GIT repository. They work relatively stable, but have a terrible speed: the version with all of these only solves ~214 problems from those above. Therefore, I will personally submit version 2.9.0 to the SAT Competition unless some grave bug is found inside. I might also submit a corrected version of the upcoming 3.0.0 release as well, but as it usually takes a month to tune the solver, and I am currently very busy with some great projects at my new workplace, so a 3.0.0 version probably won’t happen until the deadline.

I hope you will enjoy this new version of CryptoMiniSat! In case of questions, problems or bugs, please contact either me, or the development mailing list and join in to collaborate :)

Open source software? Free software?

SAT, ,

Today I attended the Open World Forum conference here in Paris. Basically, it’s a business-oriented conference to do networking for folks in the free/open source industry. Some of the panelists were sometimes really boring, such as the “French Secretary of State responsible for the Digital Economy” who seemed to have deeply confused “free as in speech” and “open source” software — a grave mistake by my book. The panelist, who knew the difference of course, regularly overemphasised the use of “open source” software, but the notion of “free as in speech” was lost, and mentioned rarely, with the notable exception of the Red Hat folks. With the release of CryptoMiniSat, which I explicitly released under a free software licence, GPLv3, I of course disagreed.

The highlight of the conference for me was meeting the current Debian Leader, Stefano Zacchiroli, and researcher Roberto Di Cosmo. I have been using Debian for a very long time, and I always wanted to contribute. However, the best way to contribute is always with your expertise, which for me is SAT solvers. So, I approached Stefano with the idea of configuration management in Debian (dpkg), for which CryptoMiniSat would be a good fit, I think: complex package dependencies could be resolved with ease using CryptoMiniSat. If included in dpkg, CryptoMiniSat could take the prize of the most deployed SAT solver away from SAT4J, which currently holds this title due to its inclusion in the Eclipse development package. Fingers crossed… and lots of work is ahead.