A key goal of Artificial Intelligence is to develop scalable and robust automated reasoning technology that will allow computers to act intelligently in increasingly complex real-world settings and in competitive and uncertain environments. One of the most successful stories in this quest has been that of combinatorial reasoning, in particular for propositional satisfiability (SAT) problems and constraint reasoning. Starting with only a few hundred variable problems in the 1990's, we can now solve interesting problems with over a million variables. I will discuss the first formal study of learning methods used in today's highly engineered inference engines in terms of resolution complexity, and an effective practical approach to exploit a problem's natural symmetric structure by going beyond the limits inherent in resolution-based inference. I will then touch upon new methods for more complex reasoning problems, namely counting and sampling solutions as well as clusters of solutions. These new methods have pushed the limits of scalability by orders of magnitude, and promise to open up a range of new applications in AI and computer science in general, particularly those involving the integration of logical and probabilistic inference.

Ashish Sabharwal is a research associate in Computer Science at Cornell University, and works at the Intelligent Information Systems Institute. He received his M.S. and Ph.D. from the University of Washington, Seattle in 2005 and joined Cornell as a postdoctoral associate. His research interests include combinatorial methods, probabilistic inference, multi-agent reasoning, connections to statistical physics, game theory, algorithm design, and complexity. He has (co-)authored over 30 publications and surveys, including two Best Paper Awards, one runner-up prize, and four best paper nominations.