AAAI'14 Tutorial SA3: SAT in AI: high performance search methods with applications

Tutorial at the AAAI'14 conference

Sunday July 27, 2014 at 9:00am - 1:00pm, Québec City, Québec, Canada

Presenter: Jussi Rintanen

Tutorial presentation (PDF)

Algorithms for the satisfiability problem (SAT) and its close relatives and extensions such as #SAT, MAX-SAT, SAT modulo Theories (SMT) and their quantified variants (QBF, SSAT) are important in solving problems in several subareas of AI, including machine learning, probabilistic reasoning, diagnosis and planning. SAT and its extensions are also a dominant approach to solving central problems in other areas of Computer Science, for example in Computer Aided Verification.

The tutorial presents the most important variants of the SAT problem, the technology behind high-performance solvers for them, and their most important applications in artificial intelligence. Theoretical background for different SAT variants and their use is presented, but the focus of the tutorial is in their concrete application in solving some of the hardest problems arising in constructing and managing intelligent systems.

  1. Introduction
    1. Historical background
    2. SAT and NP-complete problems in AI
    3. Applications of SAT in Computer Science
  2. Basic SAT algorithms
    1. the Davis-Putnam-Logemann-Loveland procedure, Conflict-Driven Clause Learning, stochastic local search
    2. preprocessing techniques
    3. SAT solvers
  3. SAT applications: Reasoning about actions and change
    1. Planning
    2. Diagnosis
    3. Model-checking
  4. #SAT and model-counting, MAX-SAT, and Stochastic SAT (SSAT)
    1. model-counting, the complexity class #P
    2. MAX-SAT
    3. SSAT and stochastic satisfiability, relation to QBF
    4. #SAT application: Most Probable Explanations with Bayesian networks
    5. SSAT application: Maximum a Posteriori Hypothesis (MAP) with Bayesian networks
    6. MAX-SAT application: structure learning for graphical models
    7. SSAT application: probabilistic planning
  5. SAT modulo Theories
    1. Boolean satisfiability and arithmetic reasoning
    2. extensions of SAT algorithms to SMT
    3. relation to other formalisms: Mixed Integer Linear Programming MILP, ...
    4. application: reasoning with time and resources

Target Audience

The target audience consists of AI researchers interested in the state-of-the-art in combinatorial search methods formalized in modern algorithms for SAT and its variants as well as the application of these algorithms in solving important problems in various areas of AI. The tutorial is intended for the general AI community audience and only assumes basic knowledge in AI and the propositional logic. The objectives best served by the proposed tutorial are the following. The tutorial assumes minimal prerequisite knowledge. Knowledge of the classical propositional logic and of the basic search algorithms in AI are sufficient.

Interest to AAAI Audience

Forms of reasoning embodied in SAT and its extensions are fundamental in the constructing and analyzing intelligent systems. The focus of the tutorial is in the algorithmic basis of different SAT variants, as well as their role in efficiently solving a wide range of central problems in AI, stretching from state-space reachability problems such as planning to probabilistic reasoning and machine learning. NP-hard constraint satisfaction and optimization problems arise in most areas of AI, making SAT a reasoning task of a high relevance to a large range of AI researchers.

Supplementary material