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 in search procedures for SAT. New local search procedures 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. This talk reviews the state of the art for research into satisfiability, and discuss applications like model checking in which algorithms for satisfiability have proved successful.
| Prof. Toby Walsh |
| Knowledge Representation and Reasoning Program National ICT Australia |
| Date: | Wed Jun 15 2005 |
| Time: | 3 to 4pm |
| Location: | Level 1 Seminar Room, CSE Bldg (K17), UNSW Kensington campus |
Last updated by tbourke at Thu Jun 2 19:42:12 2005 GMT+1000