Tools that I often use

Personal,

I used to use Perl a lot in the old days. Martin Albrecht, through the sage mathematics software, showed me Python. I first really hated Python. But then, I realised I can simply type away in it, as in C++, but without all the hassle of C++. I saw a little of AWK once, and I got madly in love with it — when it comes to simple scripts like counting numbers printed by programs, AWK is unbeatable. I use grep a lot, and recently I realised how great a combination grep and wc (a very dumb utility that counts lines/words) are. For instance, I can simply do: “grep “s SAT” *.output | wc -l” to find how many problems have been solved by CryptoMiniSat. I am also finding myself using grep and AWK together to create shell scripts that I run later. For example, I can do: “ls *.cnf | awk ‘{print “./cryptominisat ” $1 ” > ” $1.output” }’ > script.sh” which, when executed, solves all CNF files in the directory, and generates a *.cnf.output file for each, containing the output of CryptoMiniSat. An interesting utility in UNIX is ulimit, with which can limit the memory and time (and stack, etc.) usage of a process. Putting a “ulimit -t 10000” at the beginning of our “script.sh” we can simply limit CryptoMiniSat to 10000 seconds for each instance.

As for failures in terms of the tools I use, I can probably list a few. I tried very hard to learn Haskell, a purely functional language, but I simply couldn’t fully wrap my head around it. Haskell bothered me, because it seems so intuitive, yet it is so hard to master. I haven’t yet got around learning sage, either, even though I think Martin Albrecht is doing a great service to the community by coordinating it. I hope one day CryptoMiniSat will be used inside it, though :)

My connection with the boost library is a love-hate relationship. I think boost is just amazing: it lets me program with the least amount of effort, creating a program that is less error-prone, more robust and multi-platform. However, at the same time, many programmers avoid it like the plague, for multiple reasons. Firstly, the library changes so often that something you wrote just two months ago might not compile with the new boost. Secondly, it’s a nuisance to have dependencies in the code. Thirdly, compilation times can increase significantly e.g. with the Spirit parser. I don’t agree with the second argument, since boost as a dependency isn’t significant and it saves on a lot of debugging time, and the third argument is becoming moot due to gcc 4.5. But the first argument has, actually, hit me too, and it is very unpleasant.

216

SAT,

216. I am quite proud of this number. It’s the number of instances CryptoMiniSat2 can solve from the 292 problem instances of the SAT Race’09, given roughly the same amount of time and computing resources as the solvers of 2009. Last year’s winner could solve only 204. Total solving time of CryptoMiniSat for the 216 instances was 217’814 sec, in comparison to 180’345 sec (for 12 less instances) of last year’s winner. The distribution of SAT and UNSAT for CryptoMiniSat is 85 SAT and 131 UNSAT instances solved. With this performance, it would have won all three tracks of the competition (SAT, UNSAT and SAT+UNSAT) last year.

Of course, this performance doesn’t mean much in terms of the 2010 SAT Race. I would like to have CryptoMiniSat be in the top three, but who knows what other solvers are capable of. Also, I only tested on these 292 instances — there could be some grave bugs and regressions on other types of instances. I will try to test on a larger number of instances, just to see if there are some grave regressions, but I am not very good at finding bugs. However, the STP team has been great at finding bugs: they have found 3 major ones until now. Unfortunately, I am convinced there are many more.

What bugs me the most about CryptoMiniSat is that I am totally incapable of doing AIG (And-Inverter Graphs). It seems great, and some good researchers of SAT (e.g. Armin Biere, Niklas Een) are proficient in it — but to me it’s completely impenetrable. I wanted to buy a book from Amazon on Electronic Design Automation, and I wanted to read through all what Biere wrote on this topic, but I need someone to guide me. However, I simply don’t know anyone in person who knows AIG. My ignorance of AIG is a real shame, and I just feel like being stupid. I really do.

A great essay on security in the cyberworld

Personal,

I just read this paper on cybersecurity by Daniel E. Geer, and I was very impressed. Unfortunately I haven’t heard from the author yet, but I regularly used to read the blog of Bruce Schneier, and this essay basically puts the same ideas into perspective.

I have found the essay to be very interesting, and very thought-provoking. It shows very well that security in the cyber (or cyber-connected) world is very difficult to attain. There are no simple solutions. I personally think that security in the real world (not only the cyber world) is also very difficult to obtain, and unfortunately politicians tend to go the easy way, and simply bend in front of the will of the people by implementing “security measures” that in the end don’t help much (if at all) in terms of security, but reassure the people. An example of this is the ban of liquids on airplanes, while cockpits in Europe are still not reinforced — the former doesn’t achieve much but is very visible (and so is more of a security theater), while the latter would be much less visible, but also much more effective. Also to note, that the former takes a lot of man-power to implement, and inconveniences the users (thus taking their time, too), while the latter would be relatively cheap.

The mentality that leads us to believe that bombing is more of a threat is that most people expect planes to be blown up, while hijacking is most only an afterthought. This serious mistake is probably a psychological effect, as most people tend to remember visually colourful incidents more, and Hollywood has made use of the “blow-up” effect too much, etching it into the brains of most people, even decision-makers. However, it is important to remember, that most serious problems in airports and airplanes were carried out through the use of arms other than bombs: to take a trivial example, no planes used in 9/11 were bombed. As a side-note, reinforced cockpits would have prevented all of 9/11, and European cockpits are still not reinforced, but my toothpaste is always taken away — a serious defect, I say.

The dates of the SAT Race 2010 have been announced!

SAT

The dates of the SAT Race 2010 have been announced! The deadline is the end of April, so I have to get CryptoMiniSat bug-free by then.

I have decided to merge the code into STP, the Simple Theorem Prover made by some MIT researchers, among them Vijay Ganesh, with whom I have have worked quite a lot during the final months of 2009. Hopefully, with the help of the STP team, CryptoMiniSat will be bug-free by the end of this month, and through testing in STP, fine-tuning of options will be carried out. There are 16 new modules in the solver, and all have heuristic cut-offs, which have to be tuned. Naturally, I tried to use sensible defaults, but problems can vary widely, and different problems need different cut-offs. For instance, if the number of clauses is very low, even O(m^2) algorithms can be executed, while if the number of clauses is extremely large, e.g. 100’000, it might take too much time even to execute O(m*log(m)) algorithms.

If you are interested in the new CryptoMiniSat, all you need to do is to observe the developments in STP. I will also make the unstable executables accessible from this blog, through links, whenever I have a new version. Fingers crossed for a correct and fast CryptoMiniSat!

On research in general

Personal, SAT

I am not sure I am qualified to talk about research in general, but I will try to do my best.

To me, it seems that the research community of any given topic is pretty small. The reason for this is many-fold. Firstly, I suspect that the number of qualified individuals willing to work for a relatively small pay (but with many benefits, like flexible schedule, less stress, etc.) is relatively small. Secondly, any given topic usually reaches a maturity level where the subdomains are very clear, and it is very difficult to say anything reasonably good about a subdomain that one is not acquainted with. For instance, Knuth’s books are brilliant, but even he (someone who is like a semi-god in computer science) acknowledges that he simply cannot be an authority on all the topics covered in the 4th volume of his series. (BTW I just bought Vol4F0 and Vol4F1, wainting for amazon to ship now).

Since the research community is small, everyone gets to know one another. This is great since it helps collaboration, but it also might backlash against newcomers (PhD students), and against people generally not well-acquainted with the field, but who genuinely have good ideas that they wish to publish. I guess it’s a difficult integration process, that gets all the more difficult because it rarely happens that someone can simply stay in the same specific subfield for his entire research career. And even if someone stays in the same field, the field may change so much over time, attracting researchers from many distinct research domains, that even an “oldboy” can feel detached from his/her own topic after a while.

Research that deals with practical things is even more fast-moving than other kinds of research. Just a couple of years ago, research on botnets didn’t exist, yet now it seems it is a very rapidly evolving research domain. SAT solvers – I believe – also fall into the category of practical research. Year after year the solvers evolve so much that trying to compare two solvers with only 1-2 years of difference in their release dates seems nonsensical. This is great because there is a lot of “buzz” going on, but at the same time, it feels like a race against time: inspiring at first, but tiring at the end.

Very theoretical domains rarely have this speed of change. For instance, last year at the SAT’09 conference, I saw Stephen Cook, the person who basically invented the notion of NP completeness (I felt honoured just to be in the same room with him, I must say). Although SAT has changed a lot in the past years (many new applications, e.g. cryptography), but the fundamental problem didn’t change – therefore, he never had the ground taken from under him. The ground sure moved, but he still masters it, I am sure.

Oh well, legends. I met Shamir twice. Very kind person. Also, I met Daniel J. Bernstein at EUROCRYPT’09. He looked somewhat shorter and younger than I imagined, and I liked his openness. I met Lenstra at CCC’08. I was so shocked it was him, I couldn’t even say hello – very embarrassing. He was very friendly, and seemed much younger than his official age would suggest. I really want to meet Knuth, but I guess that might have to wait… forever, maybe. Unless I somehow manage to visit Stanford one day, in which case I will definitely show up at one of his classes. They say he is a terrific speaker.