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.