Compute-Intensive Methods in AI: New Opportunities for Reasoning and Search Bart Selman Cornell University selman@cs.cornell.edu
Introduction
Factors in Progress
Applications: Methodology
PPT Slide
Outline
I. Example Application: Planning
Some Applications of Planning
State-space Planning
Abdundance of Negative Complexity Results
Practice
Progression
Approach
SATPLAN
SAT Encodings
Solution to a Planning Problem
Satisfiability Testing Procedures
Walksat Procedure
Planning Benchmark Test Set
Solution of Logistics Problems
What SATPLAN Shows
II. Current Themes in Sat Solvers
SAT Solvers
Background
Preview of Strategy
Cost Distributions
Heavy-Tailed Distributions
Decay of Distributions
How to Check for “Heavy Tails”?
Heavy Tails
Randomized Restarts
Rapid Restart on LOG.D
SATPLAN Results
Heavy-Tailed Distributions in Other Domains
SAT Solvers: Themes, cont.
SAT Solvers: Recent Theory
IV. Current Themes in Encodings
Add Declarative Domain Knowledge
Kinds of Knowledge
Expressing Knowledge
Logical Status of Heuristics
Axiomatic Form
Questions
Experiment: Logistics
ntab solution of logistics
Answers
How to Generate Control Knowledge --- Automatically
Encodings: Themes cont.
Conclusions
Conclusions, cont.
Email: selman@cs.cornell.edu
Home Page: www.cs.cornell.edu/home/selman
Download presentation source