Could monomials be handled natively from SAT solvers?

SAT,

I recently got a question that intrigued me:

I am new to this SAT solving world but I was wondering whether you thought considerable speedups were possible for crypto type problems (multivariate polys over GF(2)) by simply never converting the problem to cnf at all and thereby avoiding the combinatorial explosion that results in the conversion process. That is using the original xor formulation.

First of all, the question is a follow-up to xor-clauses: they implement XOR-s natively. Using them avoids a number of problems relating to the increase of variables. Why not implement monomials (i.e. “a*b” or “a*b*c”, where “*” is binary AND and variables are binary) natively? They are the only thing left to do. Personally, I am not overly optimistic about them, though. Let me got through some of my reasons here.

Firstly, the “exponential explosion” expressed in the question is in fact much less existent than people tend to think. The reason is that the intelligent variable activity heuristics, unit propagation, and conflict generation tend to take care of a lot of potential problems. Since the propagation of a variable will entail the propagation of many others (it depends, for crypto, around ~100), there is no real explosion, since there is not really 2^n, but more like 2^(n/100) combinations that need to be explored. This argumentation takes away some of the potential benefits that native monomials could bring.

The real problem, though, is the following. By moving monomials into cryptominisat and thus potentially speeding up the solving, conflict generation could become much more complex. So, if moving to an internal monomial representation entails making a mess of conflict generation, then using monomials internally may only make the solving slower.

Another reason that native monomials may not speed up solving so much, is that a lot of clauses inserted when converting monomials are binary clauses, which are extremely well dealt with in the CNF world — it would be hard to do it any better.

As a last, but very minor point, using monomials would increase the complexity of the program, which would mean not only a lot of man-hours lost debugging it, but also a loss of performance due to a (probably non-negligible) increase of instruction cache misses.

Oh well, so those are my reasons. I would be interested if someone has some comments on these, though.

CryptoMiniSat v2

SAT

Lately, I have been working a lot with CryptoMiniSat, to get it up and running for the 2010 SAT Race, held by Carsten Sinz. Getting CryptoMiniSat fast and bug-free has been a long and winding road. I can now understand the difficulty of choosing magic parameters that these SAT solvers make use of regularly. As I have added ~6000 lines of code to a codebase of ~1500, you can probably imagine the number of magic constants that I had to come up with. Worst of all, these constants interact in non-intuitive and sometimes in a fully “magical” manner.

To test my choice of magic constants, I have been running experiments on the Gird5000 project of French universities. It is quite easy to get access to Grid5000 if you work in a French university, and it is surprisingly easy to run experiments. On the other hand, interpreting the results of such experiments is not so easy :) However, CryptoMiniSat is coming along. On crypto examples I think we are unbeatable. When it comes to other examples, we are good, but we will see how the new MiniSat (yes, it’s coming!) and precosat will do. Apparently, the GLUCOSE people are also planning to enter the competition, so the race will be very interesting. Fingers are crossed that CryptoMiniSat will finish somewhere in the top 3 :)

There are some “secret” improvements that I have made the past couple of months, and there are some open secrets. I tried to incorporate the GLUCOSE restart heuristic, and XORs are automatically detected (XOR clauses are no longer neccessary, but they are of course supported!). This means that CryptoMiniSat is now a plug-and-play experience for all the crypto-folks. I have tested the solver with a good number of crypto problems, and the speedup relative to MiniSat is on the order of 2-50x, depending on the problem.

The new CryptoMiniSat will be released when the SAT Race starts and everyone’s executables have been freezed. I will then detail all the new features. Until then, let me just run a couple of more experiments on that cluster :)

Why do I use Linux?

Personal,

I used to be quite an expert on Windows, I even used to hang out on the #windows-help IRC channel. So why do I use Linux uniquely nowadays?

First, I tried Linux out of curiosity. What made me interested initially is that I am a control freak: I like to know what happens with my computer. With windows there were always a billion things running in the background, and I had no clue what they were doing. With linux you always know what does what. “man programname” and you have a complete documentation. This was a real kick for me. I could read these manuals for days, literally. I hate when things “just work” – I want to know *why?*. Simple curiosity. However, this doesn’t explain why I have stuck with Linux for such a long time.

The reasons I have stuck with GNU/Linux are the following:

  • No adware/spyware/viruses since all programs in all Linux distributions are installed from signed packages
  • Huge amount of available documentation and a howto for everything. Got stuck? Just read up
  • No vendor lock-in. Wanna change from KDE to GNOME? From KOffice to OpenOffice? No problem.
  • Faster than Windows and accompanying proprietary software (Office, MSN messenger, Adobe PDF reader, etc.)
  • More customisable than Windows. Proprietary applications mean that if you change your colorscheme in Windows, almost none of your applications will have that colorscheme. If you do something different than most people (e.g. keycombinations), in Linux, you can easily change the program to suit your needs.
  • Installing applications is fast and easy: Tired of answering the 20 questions that all installers ask you in Windows? So am I. In Linux, just launch Synaptics, type in what you want to do, e.g. “instant messaging”, and you are presented with all applications offering that service. Double-click on any and you are done (this is not a joke, it’s really that simple) It’s safe, fast, and there are no questions asked.
  • Uninstalling is fast and efficient. Uninstalling AOL messenger is not only terribly difficult, but also leaves a lot of stuff behind. AOL browser? AOL as default webpage? And this not only applies to AOL. Windows messenger will change your default webpage when installed. Uninstalling it doesn’t reverse that.
  • No junk software. Are you, too, tired of all the popups that “The full version of this software offers this-and-that, buy it now!” ?
  • Software upgrades are seamless. One interface for all upgrades. You don’t need 20 upgrade programs running non-stop (Java nags you non-stop? Adobe PDF Reader naggings? Windows upgrade naggings?)
  • Does all that is possible, not all that vendors want to be possible. Print to PDF? No problem. Backup your DVD? No problem.
  • Cheap, or even free. Tired of all the money you have to pay, and still it doesn’t work? Well, in Linux it might not work, either, but if you payed a little bit, you can call the service desk (and they are helpful), or you can ask you local linux geek (he will be all too helpful), or you can just read up on the documentation (it’s good and well-written)
  • If you have found a problem in the program, there are always helpful developers to correct the problem. They listen to what you have to say, and personally thank you for your comments. Try to do that with any proprietary software: they will send you a pre-written “thank you” notice, and promptly ignore you.

Of course there are many other, less practical and more theoretical reasons for why I like linux: Free as in not locked-in, total control, possiblity of tweaking things, the availability of developer discussions through open mailinglists, the number of programs to do the same thing (i.e. choice), and many others.

To use Linux day-to-day takes a bit of courage. Your friends will be annoyed that they can’t use the ultra-cool (but ultra-useless) features of their newest MSN messenger when they talk to you. And there will be other problems. You might be forced to use Windows at work, or you might need to use a software that doesn’t run under the free windows emulator, wine (though most software does), and you will have to find a replacement. And you won’t be able to play the newest game out there (but you can play World of Warcraft, and most other big games, like Diablo, on Linux).

The advantages are huge, however. You simply won’t understand how can your friends get a malware infection every day, why their bankaccounts get overtaken once a year, and why on Earth does it take their computer 5 minutes to boot up. You will sleep tight, knowing full well that your computer is safe from all people who might do you harm, be them malicious (malware writers), or be them proprietary companies restricting the use of the music or video you just bought. And you will know that if some problem comes up, there will be tons and tons of free tools and lots and lots of developers ready and willing to help you out just for the kicks. You are not alone.

How to unload the sound module

Personal

I regularly have a problem with my sound card: it simply stops working, and xine (and everything else) says that it cannot open the sound socket. So, I need to unload and reload the snd_hda_intel module. Most of the time, however, I cannot since it is in use. I try to close all possibly using sound, but most of the time it is a dead process that is using it. But, I have figured out how to find these unruly processes:

1) fuser -a /dev/snd/pcmxxxx (where try all here, xxxx can be anything)
2) for each process ID (PID) listed, do a, do “ps xa | grep PID”, so see what the process is. Close it cleanly, if possible (through the gui), or “kill” it if it is a hanged process. Most of the time, it is a program in a messed-up state – in my case it is sometimes a “kio-exec” process. Killing is simply “kill PID” or, more harshly, “kill -9 PID”.

Now issue “rmmod snd_hda_intel” and then “modprobe snd_hda_intel”. Done! :)

KDE4 composite with intel drivers

Personal

I have been having a hard time getting the composite effects running smoothly on KDE4 with my intel Mobile 945GM graphics card. But I have finally managed to get it up and running! This is how:

  1. Get the latest intel driver from your repository (I have 2.3.2)
  2. Put into xorg.conf at the driver section: 
    Section "Device"
Identifier      "Configured Video Device"
Driver "intel"
Option "DRI" "true"
EndSection
  3. Put at the end of your xorg.conf: 
    Section "DRI"
Mode 0666
EndSection

Section "Extensions"
Option "Composite" "Enable"
Option "DAMAGE" "Enable"
Option "RENDER" "Enable"
Option "RandR" "on"
EndSection
  4. Under the system settings, enable desktop effects and set in the advanced settings to use XRender! (and take out the update thumbnails and the smooth scaling).
  5. Restart X: restart the computer or just do: logout then push “ctrl+alt+backspace”, log in to the console as root, and restart kdm by issuing: “/etc/init.d/kdm restart”.

I have by the way, a Dell D430, so an extremely lightweight, small computer that probably has the worst performance among its peers, and the effects are *fast* I must say that the “coverflow” effect (not enabled by default) isn’t that great, something is wrong with it, but still: scrolling is super-fast, switching windows is super-fast, so you won’t notice any slowdown at all!