SAT solving in AI

This lecture will discuss two significant applications of satisfiability and max-sat in AI: planning and probabilistic inference.  The first half of the lecture covers: encoding classic STRIPS-style planning as satisfiability; using planning graphs to prune the encoding; state-transition based encodings; encoding plan recognition; handling costs.  The second half of the lecture covers encoding Bayesian Networks as max-sat; Markov Logic; lazy instantiation; and constraint-propagation for domain pruning.

Henry Kautz, University of Rochester, Rochester, USA

is Chair of the Department of Computer Science at the University of Rochester. He performs research in knowledge representation, satisfiability testing, pervasive computing, and assistive technology. His academic degrees include an A.B. in mathematics from Cornell University, an M.A. in Creative Writing from the Johns Hopkins University, an M.Sc. in Computer Science from the University of Toronto, and a Ph.D. in computer science from the University of Rochester. He was a researcher and department head at Bell Labsand AT&T Laboratories until becoming a Professor in the Department of Computer Science and Engineering of the University of Washington in 2000. He left Seattle in 2006. He is President (2010-2012) of the Association for the Advancement of Artificial Intelligence, Fellow of the AAAI, a Fellow of the American Association for the Advancement of Science, and a recipient of the IJCAI Computers and Thought Award.