IJCAI'09 Tutorial on SAT, SMT & QBF and Their Applications in AI

IJCAI'09 Tutorial: SAT, SMT & QBF and Their Applications in AI

Tutorial at the IJCAI'09 conference

July 13, 2009. Pasadena, California

Presenter: Jussi Rintanen

Tutorial presentation (PDF) (0.86 MB)

The tutorial presents the main algorithmic techniques for solving the SAT problem and two of its important extensions, QBF/SSAT and Satisfiability Modulo Theories (SMT), and explains their application to solving problems AI such as planning and diagnosis.

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 atomic propositions. 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 these address theoretical or practical boundaries of the basic SAT framework in solving important problems in AI.

The objective of the tutorial is to present a brief 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 or diagnosis.

Contents

  1. Introduction
  2. SAT and algorithms for solving SAT
    1. theoretical basis: NP-completeness
    2. the Davis-Putnam-Logemann-Loveland procedure
    3. clause learning, heuristics and restarts
  3. Applications of SAT to Planning, Diagnosis, ...
    1. translations of actions into the propositional logic
    2. translations of planning (discrete systems, discrete-time) into the propositional logic
    3. translations of diagnosis (discrete systems, discrete-time) into the propositional logic
  4. SAT modulo Theories
    1. motivation: representation of non-Boolean data types and timed systems (temporal planning)
    2. basic structure of SMT solvers
    3. application: temporal planning, timed and hybrid systems
  5. Quantified Boolean formulae
    1. motivation: alternation / AND-OR trees, NP vs PSPACE
    2. extensions of DPLL to AND-OR trees
    3. algorithms based on quantifier elimination
    4. applications: games, incompleteness in planning
    5. SSAT

Target audience

The target audience is part of the core audience of IJCAI'09.
  1. Researchers interested in applying algorithms for SAT, QBF or SMT in the development of intelligent systems. The tutorial is intended for the general AI community audience and only assumes basic knowledge in AI and the propositional logic. Because of the wide applicability of satisfiability testing and the basic representation techniques presented in the tutorial, potential applications span a wide range of subfields of AI. The tutorial gives an overview of the current state-of-the-art in problem solving with propositional reasoners and provides a basis for assessing the suitability of different techniques for specific applications.
Knowledge of the classical propositional logic and of the basic search algorithms in AI are sufficient prerequisites for attending the tutorial.

Interest to IJCAI audience

Reasoning about the changes that take place in the world is central to intelligence and intelligent behavior. Planning, abduction/diagnosis, explanation and many other central forms of reasoning performed by intelligence agents can be understood in terms of a transition system model of the world, and many of the most efficient approaches to these reasoning tasks are based on the propositional logic and satisfiability algorithms. The very fast development of satisfiability algorithms in the recent years has made it practical to apply them to an increasingly wide range of problems in AI. Some of the main innovation in propositional reasoning takes place outside the AI community which makes this tutorial overview interesting to many AI researchers.