Collaborations: Winning the SAT Race

Managing giant databases, performing complicated calculations, searching data all over the Internet... nowadays computer programs are able to solve a host of problems and sometimes in a very efficient way.

But what is efficiency? When can one say that a program is efficient? Simplifying things to the most, computer scientists consider an algorithm (i.e., a program) to be efficient if it needs a number of steps that is proportional to the number of input data elements it has to process (N). If a problem takes the square of that number, N^2, to be solved, or at most its cube, N^3, or fourth power, N^4, it still can be said that the efficiency of the program is good. For example, the simplest algorithms for sorting lists of numbers typically take N^2 steps. That means that if you want to sort a list of a thousand numbers, the program will need a number of steps that will be proportional to a thousand times a thousand, i.e., it will be in the range of a million steps. If a step needs a microsecond, then the whole operation will take just a second.

Unfortunately, not for all problems efficient algorithms have been found. The world is full of important problems that can take an exponential computation time expressed, for example, as 2^N, that is, 2 times 2 times 2... N times. In this case, if N equals 1000, the calculation would take 2^1000 steps, which amounts to a lot of billions of years!. Just to have an idea of what this means, think that 2^400 is a much bigger number than the total number of atoms in the Universe!.

NP-complete problems are an important subclass of these difficult problems. This class includes thousands of practical problems that one encounters, for example, when designing transportation routes or communication networks, in genetics and biomedicine, when assigning machines or other resources in industrial processes, in the verification of electronic circuits, when preparing time schedules for trains or airlines, etc.. Even things that seem simpler because they are done day after day, like loading a truck or the cargo bay of a boat are, in fact, NP-complete problems.

The good news about NP-complete problems is that they can be "translated" efficiently into one another. That means that if we had an efficient algorithm for just a single NP-complete problem, then we would have it for this whole class of problems!.  That is the reason why finding such an algorithm would be a discovery of the utmost importance and it would have enormous consequences. In fact, this is considered as one of the Challenges of the Millennium by the Clay Mathematics Institute which promises a prize of one million dollars to whoever finds that algorithm or, conversely, to whoever is able to prove that it cannot exists (see "P versus NP" at claymath.org)

The Logic and Programming Group at LSI department has a sizeable experience in this field. It has worked on the theory underlying NP-complete problems and has solved SAT problems in domains such as Linguistics, Biology, Hardware and Software Verification and Planification as, for example, the scheduling of the football matches in the Dutch Professional Football League (see +LSI Newsletter number zero).

Some weeks ago in Guangzhou, China, the World Congress on SAT took place as well as the associated annual contest for SAT solvers,  the "SAT Race". At the SAT Race no athlete runs, no human competes. Instead, computer programs fight against each other. SAT solvers developed by the participating research groups are the contenders here. The contest organizers test each SAT solver against one hundred industrial problems that represent SAT problems of different origins. The winner is the SAT solver that is able to solve the greatest number of problems in a maximum time of 900 seconds per problem.

This year the competition was again a success with more than 47 teams from all over the world. About a half of them came from industry (with Intel and Microsoft teams among others) The rest were universities and research centres. Nineteen teams made it through the classifying rounds. The competition attested to the strong progress in this field: last year's winner would have only made a fifth position in this year's contest.

In the final round the gold medal went to the almost unbeatable MiniSAT solver that solved 81 problems. MiniSAT was developed by a team of researchers form the Cadence Company in Berkeley, USA, and the Chalmers University in Sweden. The second place, with 79 solved problems, went to an iimproved variant of an older version of MiniSat, developed at Melbourne University. The bronze medal, with 77 solved problems, was awarded to the Barcelogic solver, developed at UPC. Among the winners, it was the only one that was not based on MiniSAT.

For further information an details, see : www-sr.informatik.uni-tuebingen.de/sat-race-2008.