MA4

SAT, SMT and QBF and Their Applications in AI
Jussi Rintanen

In the last ten years the efficiency of algorithms for the satisfiability problem of the classical propositional logic has improved by several orders of magnitude. Main technical innovations include clause learning, randomization and new implementation techniques, which have made it possible to apply the algorithms to propositional formulae consisting of millions of clauses and propositional variables. These developments have enabled the large scale application of automated reasoning technology to problems of practical significance, first in the area of computer-aided verification and validation, and increasingly in other areas of computer science, including AI.

Important extensions of SAT include SAT Modulo Theories (SMT) and Quantified Boolean Formulae (QBF). Both of them address theoretical or practical boundaries of the basic SAT framework in solving important problems in AI.

The objective of the tutorial is to present an overview of the algorithmic basis of modern SAT, SMT and QBF solvers, and to outline the main representation techniques when applying them to problems such as planning, diagnosis and related problems. Prerequisite knowledge for attending the tutorial is basics of the propositional logic.

Jussi Rintanen is a principal researcher and the leader of the planning and diagnosis group at NICTA's Canberra laboratory. He obtained PhD at the Helsinki University of Technology in 1997. After 2 years as a project researcher at the University of Ulm, in 1999 he joined the University of Freiburg where he did research and lectured until joining NICTA in 2006. His research interests are in automation of high-level decision-making and reasoning tasks such as planning, supervisory control and diagnosis, by using technology for automated reasoning, especially for propositional logics.

(back)