**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.

Webmaster: Sven Olofsson, sveno@dsv.su.se Last modified: Mar 14, 1999