|
报告摘要：
SAT, Boolean, or propositional satisfiability, is a central problem in Computer Science, with both theoretical and practical interests. Problem solving in SAT is to encode a problem instance by a propositional formula, and use a SAT solver to determine whether the given problem has a solution. In this seminar, we introduce the basics of SAT, with an emphasis on the state-of-the-art techniques in building fast SAT solvers. As an example, we show how to use SAT to solve the planning problem in artificial intelligence。
报告人简介:
Jia-Huai You is a Professor with the Department of Computer Science, University of Alberta, Canada. He is also the China Advisor to University of Alberta, specially invited overseas evaluation expert of China’s Ministry of Education. His research areas include Constraints, Knowledge Representation and Reasoning, Logic Programming and Nonmonotonic Reasoning. His recent interests are the extension of answer set programing and its relationships to constraints satisfaction programming. Exploring the answer set programming’s application on the Bioinformatics and Abduction reasoning is also his job. He graduated from University of Utah, US with a Ph.D in Computer Science and was once an editor of Journal of Artificial Intelligence Research, which is popular on AI. Since 1984, Professor You has published over 140 papers. Most of them were on the high-level journals and conferences. His Paper on AAAI07 was selected as excellent track(top 5%), paper on IJCAI03 as fast track(top 2%).
个人主页： http://webdocs.cs.ualberta.ca/~you/ |
