For those who remember the KKK and the wrestling team from early roleplaying cons, Dr Jeem 'Evil' Stuckey won the
Eureka Prize for Innovation in Computer Science last night.
True to form, he won it for Lazy Clause Generation. From the awards page:
The notion of combinatorial optimisation is best illustrated by the famous Travelling Salesman Problem, a mathematical puzzle formulated in 1930. Given a list of cities and the distance between every combination of cities, the task is to find the shortest possible tour for a salesman wishing to visit each city only once.
There are two main approaches to solving such problems. The first is ‘constraint programming', where relations between variables are stated in the form of constraints.
The second approach is called ‘satisfiability programming', which determines if the variables of a given formula can be assigned in such a way as to make the formula true.
In short, constraint programming provides a range of possible solutions to a problem and satisfiability programming chooses logically between those possibilities.
The basic premise behind Professor Stuckey's of ‘lazy clause generation' is to combine the two approaches. The problem with constraint solving systems is that they are bad at learning from mistakes made during the search process. On the other hand, satisfiability solvers are very effective at learning from mistakes. The trick is to pass on the inferences made by the constraint program to the satisfiability program, which can then learn automatically.
The challenge is to find the right balance between telling the satisfiability program ‘too much' or ‘too little'. The key contribution of Professor Stuckey has been to strike the right balance.