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.
Introduction
Historical background
SAT and NP-complete problems in AI
Applications of SAT in Computer Science
Basic SAT algorithms
the Davis-Putnam-Logemann-Loveland procedure, Conflict-Driven Clause Learning, stochastic local search
preprocessing techniques
SAT solvers
SAT applications: Reasoning about actions and change
Planning
Diagnosis
Model-checking
#SAT and model-counting, MAX-SAT, and Stochastic SAT (SSAT)
model-counting, the complexity class #P
MAX-SAT
SSAT and stochastic satisfiability, relation to QBF
#SAT application: Most Probable Explanations with Bayesian networks
SSAT application: Maximum a Posteriori Hypothesis (MAP) with Bayesian networks
MAX-SAT application: structure learning for graphical models
SSAT application: probabilistic planning
SAT modulo Theories
Boolean satisfiability and arithmetic reasoning
extensions of SAT algorithms to SMT
relation to other formalisms: Mixed Integer Linear Programming MILP, ...
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.
Introduce novices to major topics of Artificial Intelligence.
Introduce expert non specialists to an AI subarea.
Motivate and explain a topic of emerging importance for AI.
Provide instruction in established but specialized AI methodologies.
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.