Ian Gent & Toby Walsh
In recent years, there has been an explosion of research in AI into propositional satisfiability (or SAT). There are many factors behind the increased interest in this area. One factor is the improvement of search procedures for SAT. New local search procedures like GSAT and WalkSAT are able to solve SAT problems with thousands of variables. At the same time, implementations of complete search algorithms like Davis-Putnam have been able to solve open mathematical problems. Another factor is the identification of hard SAT problems at a phase transition in solubility. A third factor is the demonstration that we can often solve real-world problems by encoding them into SAT. There has also been an improved theoretical understanding of SAT, particularly in the analysis of such phase transition behaviour. This halfday tutorial will review the state of the art for research in satisfiability and discuss applications in which algorithms for satisfiability have proved successful.
Prerequisite knowledge:
The tutorial will be aimed at the general AI audience, both academic
and industrial. In particular, limited prior knowledge will be assumed
about logic and computational complexity.
Ian Gent is a lecturer in the Department of Computer Science at the University of Strathclyde. He holds an MA in Mathematics from the University of Cambridge, an MSc in Artificial Intelligence from Edinburgh University, and a Ph.D. in Computer Science from University of Warwick.
Toby Walsh is a research fellow in the Department of Computer Science at the University of Strathclyde and an honorary fellow at the Division of Informatics at Edinburgh University. He received a BA in Mathematics and Physics from the University of Cambridge, and a MSc and PhD from the Department of Artificial Intelligence at Edinburgh University. He has been a Marie-Curie postdoctoral fellow at INRIA (Nancy, France) and at IRST (Trento, Italy), and a SERC postdoctoral fellow at the Department of Artificial Intelligence in Edinburgh.
Ian Gent and Toby Walsh are founding members of the APES research group, a cross-university group of researchers dedicated to improving the use of empirical methods within artificial intelligence. For more details, see http://www.cs.strath.ac.uk/~apes.