Professor Moshe Vardi, Rice University, TexasSpeaker's Biography
Moshe Y. Vardi yw’r Athro Gwasanaeth Nodedig George mewn Peirianneg Gyfrifiadurol a Chyfarwyddwr Sefydliad Ken Kennedy ar gyfer Technoleg Gwybodaeth ym Mhrifysgol Rice. Mae wedi ennill tair gwobr IBM am arloesedd eithriadol, Gwobr Goedel ACM SIGACT, Gwobr Kanellakis ACM, Gwobr Codd ACM SIGMOD, Medal Blaise Pascal, Gwobr Goode Cymdeithas Gyfrifiaduron IEEE, Gwobr Cyflawniadau Nodedig EATCS, Gwobr Gwyddonydd Nodedig y Southeastern Universities Research Association, a Gwobr Church. Mae’n awdur ac yn gyd-awdur ar dros 500 o bapurau, yn ogystal â dau lyfr: Reasoning about Knowledge a Finite Model Theory and Its Applications. Mae’n un o Gymrodyr yr Association for Computing Machinery, American Association for Artificial Intelligence, American Association for the Advancement of Science, European Association for Theoretical Computer Science, Institute for Electrical and Electronic Engineers, a’r Society for Industrial and Applied Mathematics. Mae’n aelod o’r US National Academy of Engineering a’r National Academy of Science, American Academy of Arts and Science, European Academy of Science, ac Academia Europaea. Mae ganddo ddoethuriaethau er anrhydedd o Brifysgol Saarland yn yr Almaen, Prifysgol Orleans yn Ffrainc, UFRGS ym Mrasil, a Phrifysgol Liege yng Ngwlad Belg. Ar hyn o bryd, mae’n Uwch-olygydd deunydd cyfathrebu yr ACM, wedi degawd yn gwasanaethu fel Prif Olygydd.From: June 27, 2018, noon
Join us for a Founding the Foundry talk by Professor Moshe Vardi on The Automated-Reasoning Revolution: From Theory to Practice and Back. This talk is aimed at a general Computer Science audience and a free lunch is provided.
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 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 variables without giving up correctness guarantees.
Contact: Julia Harrison (Email: email@example.com)