IJCAI'07 Tutorial by Jussi Rintanen

Reasoning about Dynamic Systems by Satisfiability Testing: Planning, Model-Checking and Diagnosis (IJCAI'07 Tutorial)

Tutorial at the International Joint Conference on Artificial Intelligence

January 8, 2007. Hyderabad, India.

Dr. Jussi Rintanen (National ICT Australia, Canberra Research Laboratory)

Motivation

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 as satisfiability testing together with other approaches to propositional constraint satisfaction is emerging as the most important practical framework for automated reasoning in AI, probably in many other areas in the next few years.

The objective of the tutorial is to present a brief overview of the algorithmic basis of modern SAT solvers and to outline the main representation techniques for planning, model-checking and model-based diagnosis/abduction for discrete dynamic systems. The tutorial is based on a transition system model in which different reasoning problems are uniformly represented. Many of these problems can be reduced to finding sequences of actions or events in a transition graph. Each sequence of length n corresponds to an assignment that satisfies a formula which implicitly represents all sequences of length n in the transition system.

Target audience

The target audience consists of a part of the core audience of IJCAI'07.

Researchers interested in applying satisfiability algorithms 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.

The tutorial assumes minimal prerequisite knowledge. Knowledge of the classical propositional logic and of the basic search algorithms in AI are sufficient.

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.

Contents outline

The tutorial outline is as follows.

Introduction
1. Basic questions about a transition system: reachability, existence of paths satisfying a given p roperty, diagnosis
satisfiability algorithms
1. the Davis-Putnam-Logemann-Loveland procedure
2. clause learning
3. incremental SAT solving
4. local search algorithms for satisfiability
5. CNF vs arbitrary formulas vs Boolean circuits
the transition system model
1. transition graphs
2. succinct representation with state variables and formulas
planning as satisfiability
1. translations of actions into the propositional logic
2. translations of planning into the propositional logic
3. partially ordered plans
4. plan search, optimal vs. non-optimal plans
satisfaction of LTL properties: LTL goals / LTL model-checking
1. linear temporal logic LTL
2. transition sequences satisfying an LTL formula
3. representation of infinite sequences by the loop-back construction
4. applications
diagnosis of dynamic systems
1. model-based diagnosis
2. diagnosis of dynamic systems as a satisfiability problem
3. restriction to minimal diagnoses: cardinality constraints
techniques complementary to satisfiability algorithms
1. normal forms: ordered binary decision diagrams (OBDD), deterministic decomposable negation normal form (DNNF)
2. operations on formulas: E and A abstraction
3. manipulation of transition relations (composition, image/preimage operations)
4. symbolic state-space traversal algorithms
extensions of SAT and their applications
1. SAT + arithmetics: mathSAT
2. quantified Boolean formulas QBF
3. stochastic satisfiability SSAT

Course material

slides

Literature

Model-checking

Armin Biere, Alessandro Cimatti, Edmund Clarke and Yunshan Zhu, Symbolic model checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), 1999.

Latvala, T., Biere, A., Heljanko, K., and Junttila, T.: Simple bounded LTL model checking. In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'2004), pages 186-200, Lecture Notes in Computer Science 3312, 2004.

Diagnosis

Planning as satisfiability

Henry Kautz and Bart Selman, Pushing the envelope: planning, propositional logic, and stochastic search, Proceedings of the Thirteenth National Conference on Artificial Intelligence, 1996.

Michael Ernst, Todd Millstein, Daniel S. Weld, Automatic SAT-compilation of planning problems, Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI'97), pages 1169-1177, 1997.

Jussi Rintanen, Keijo Heljanko and Ilkka Niemelä, Planning as satisfiability: parallel plans and algorithms for plan search, revised version appears in Artificial Intelligence Journal, 170(12-13), pages 1031-1080, 2006.

For planning techniques in general see my AAAI'06 tutorial.

M. L. Littman, S. M. Majercik and T. Pitassi, Stochastic Boolean satisfiability, Journal of Automated Reasoning 27:251-296, 2001.

Model-checking with BDDs

J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, D.L. Dill, Symbolic model-checking for sequential circuit verification, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1993.

Randall E. Bryant, Symbolic Boolean manipulation with ordered binary decision diagrams, ACM Computing Surveys, 1992.

R. I. Bahar, E. Frohm, C. Gaona, G. Hachtel, E. Macii, A. Pardo and F. Somenzi, Algebraic decision diagrams and their applications, Proceedings of the International Conference on Computer Aided Design, 1993.

SAT Algorithms

P. Beame, H. Kautz and A. Sabharwal, Towards understanding and harnessing the potential of clause learning, Journal of AI Research 22:319-351, 2004.

David G. Mitchell, A SAT solver primer, 2004.

Applications of SAT+arithmetics

Fränzle, Martin and Herde, Christian, Efficient proof engines for bounded model checking of hybrid systems, Electronic Notes in Theoretical Computer Science 133, pp. 119-137, 2005.

Gilles Audemard, Marco Bozzano, Alessandro Cimatti and Roberto Sebastiani, Verifying industrial hybrid systems with MathSAT, Electronic Notes in Theoretical Computer Science 89, 2004.