听后感：
英语不容易听懂，结合看PPT，大概了解了他的工作。影响深刻的是他介绍了所研究问题的历史发展，相关工作，然后介绍自己的工作，这种研究方法的严谨性和条理性值得借鉴。介绍了逻辑发展史、遇到的挑战以及与当下研究热点的结合：可满足问题（SAT）、机器学习、深度学习等等紧密相关。
"Logic for precise meaning of machine "
"Don‘t be scare of worst-case complexity" ---这句话很有启发，不能因为最坏情况而放弃努力。
下面是报告信息：
Title: The Automated-Reasoning Revolution: From Theory to Practice and Back
Speaker: Moshe Vardi (Rice University, USA)
Time: 09:00, March 2nd, 2016
Venue: Seminar Room (334), Level 3, Building 5, Institute of Software,
Chinese Academy of Sciences.
Abstract:
For the past 40 years computer scientists generally believed that
NP-complete problems are intractable. In particular, Boolean
satisfiability (SAT), as a paradigmatic automated-reasoning problem, has
been considered to be intractable. Over the past 20 years, however, there
has been a quiet, but dramatic, revolution, and very large SAT instances
are now being solved routinely as part of software and hardware design.
In this talk I will review this amazing development and show how automated
reasoning is now an industrial reality.
I will then show describe how we can leverage SAT solving to accomplish
other automated-reasoning tasks. Counting the the number of satisfying
truth assignments of a given Boolean formula or sampling such assignments
uniformly at random are fundamental computational problems in computer
science with applications in software testing, software synthesis, machine
learning, personalized learning, and more. While the theory of these
problems has been thoroughly investigated since the 1980s, approximation
algorithms developed by theoreticians do not scale up to industrial-sized
instances. Algorithms used by the industry offer better scalability,
but give up certain correctness guarantees to achieve scalability. We
describe a novel approach, based on universal hashing and Satisfiability
Modulo Theory, that scales to formulas with hundreds of thousands of
variable without giving up correctness guarantees.
The talk is accesible to a general CS audience.
Biography:
Moshe Y. Vardi is the George Distinguished Service Professor in
Computational Engineering and Director of the Ken Kennedy Institute for
Information Technology Institute at Rice University. He is the
co-recipient of three IBM Outstanding Innovation Awards, the ACM SIGACT
Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the
Blaise Pascal Medal, the IEEE Computer Society Goode Award, the EATCS
Distinguished Achievements Award, and the Southeastern Universities
Research Association‘s Distinguished Scientist Award. He is the author
and co-author of over 500 papers, as well as two books: Reasoning about
Knowledge and Finite Model Theory and Its Applications. He is a Fellow
of the Association for Computing Machinery, the American Association for
Artificial Intelligence, the American Association for the Advancement of
Science, the European Association for Theoretical Computer Science, and
the Institute for Electrical and Electronic Engineers. He is a member of
the US National Academy of Engineering, the American Academy of Arts and
Science, the European Academy of Science, and Academia Europea. He holds
honorary doctorates from the Saarland University in Germany and Orleans
University in France. He is the Editor-in-Chief of the Communications of
the ACM.