In Del Val 1994, the class UC was introduced for efficiently representing knowledge as sets of boolean equations.

A year later, in Schlipf et al 1995, another class SLUR of sets of boolean equations, solvable efficiently via certain simple methods, was introduced. Now, 18 years later, PhD Computer Science student, Matthew Gwynne, and supervisor, Dr Oliver Kullmann, have shown that these two independent approaches coincide, resulting in new perspectives and new ideas for solving such sets of equations.

Finding solutions to systems of boolean equations (the satisfiability [SAT] problem) is perhaps the most important problem in computer science. The Cray Mathematics Institute offers a $1 million prize to the person that can show these problems to be either solvable efficiently, or in general "difficult to solve" (the famous "P vs NP" problem). The reason for such interest lies in the fact that the SAT problem is "NP-complete". This means that thousands of practical problems can be solved by translating into "SAT", and work then focused on a single algorithm to solve this one special type of problem. This $1 million prize remains untouched; there is no (known) general method for solving SAT problems "totally efficiently". However, over the past 20 years, through advances in understanding and SAT algorithms, large industrial SAT problems are now solvable in seconds and problems that previously would have taken millions or billions of years are now solvable using large clusters and supercomputers. For example, advances in computer chip design (Electronic Design Automation), scheduling, decision management, and verification of safety critical systems are today possible due to advances in SAT technology. Gwynne and Kullmann's work focuses on translations of these thousands of different problems to SAT. Translate a problem one way and it might take millions, trillions, or even 10^100 years to solve; translate another way and the problem is solvable in a mere hours.

In recognition of their contribution to research on satisfiability, Matthew and Oliver were awarded the best paper award at SOFSEM 2013, the International Conference on Current Trends in Theory and Practice of Computer Science. The hope is that through further work in this area, more and more currently intractable problems can be brought into the realm of practical SAT solving.

For more information on their work, see http://cs.swan.ac.uk/~csoliver/papers.html#SLUR2012SOFSEM

- Tuesday 26 March 2013 15.26 GMT
- Wednesday 27 March 2013 09.07 GMT
- College of Science