...
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.
| Attachments | ||
|---|---|---|
|