About the series
Bio:
Moshe Y. Vardi is the George Distinguished Service Professor in Computational Engineering and Director of the Ken Kennedy Institute for Information Technology at Rice University. He is the recipient of three IBM Outstanding Innovation Awards, the ACM SIGACT Gödel 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, the Institute for Electrical and Electronic Engineers, and the Society for Industrial and Applied Mathematics. He is a member of the US National Academy of Engineering and National Academy of Science, the American Academy of Arts and Science, the European Academy of Science, and Academia Europaea. He holds honorary doctorates from the Saarland University in Germany, Orleans University in France, and UFRGS in Brazil. He is the Editor-in-Chief of the Communications of the ACM.
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 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, which scales to formulas with hundreds of thousands of variable without giving up correctness guarantees.
To Join the Webinar:
Please register at:
https://nsf.webex.com/nsf/j.php?RGID=r35e52abc8dc1b8d681d1d20b122fe67f
by 11:59pm EST on Tuesday, March 8, 2016.
After your registration is accepted, you will receive an email with a URL to join the meeting. Please be sure to join a few minutes before the start of the webinar. This system does not establish a voice connection on your computer; instead, your acceptance message will have a toll-free phone number that you will be prompted to call after joining. If you are international, please email kgeary@nsf.gov to obtain the appropriate dial in number. Please note that this registration is a manual process; therefore, do not expect an immediate acceptance. In the event the number of requests exceeds the capacity, some requests may have to be denied.
