BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Moshe Vardi (Rice University) DTSTART:20200521T180000Z DTEND:20200521T190000Z DTSTAMP:20260404T165405Z UID:OLS/5 DESCRIPTION:Title: The automated-reasoning revolution: From theory to practice and back\nby Moshe Vardi (Rice University) as part of Online logic seminar\n\n\nA bstract\nFor the past 40 years computer scientists generally believed that \nNP-complete problems are intractable. In particular\, Boolean\nsatisfiab ility (SAT)\, as a paradigmatic automated-reasoning problem\, has\nbeen co nsidered to be intractable. Over the past 20 years\, however\, there\nhas been a quiet\, but dramatic\, revolution\, and very large SAT instances\na re now being solved routinely as part of software and hardware design.\nIn this talk I will review this amazing development and show how automated\n reasoning is now an industrial reality.\n\nI will then describe how we can leverage SAT solving to accomplish\nother automated-reasoning tasks. Sam pling uniformly at random satisfying\ntruth assignments of a given Boolean formula or counting the number of such\nassignments are both fundamental computational problems in computer\nscience with applications in software testing\, software synthesis\, machine\nlearning\, personalized learning\, and more. While the theory of these\nproblems has been thoroughly invest igated since the 1980s\, approximation\nalgorithms developed by theoretici ans do not scale up to industrial-sized\ninstances. Algorithms used by th e industry offer better scalability\,\nbut give up certain correctness gua rantees to achieve scalability. We\ndescribe a novel approach\, based on u niversal hashing and Satisfiability\nModulo Theory\, that scales to formul as with hundreds of thousands of\nvariables without giving up correctness guarantees.\n LOCATION:https://stable.researchseminars.org/talk/OLS/5/ END:VEVENT END:VCALENDAR