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:20260423T035606Z UID:OLS/5 DESCRIPTION:Title: The automated-reasoning revolution: From theory to practice and back\nby M oshe Vardi (Rice University) as part of Online logic seminar\n\n\nAbstract \nFor the past 40 years computer scientists generally believed that\nNP-co mplete problems are intractable. In particular\, Boolean\nsatisfiability ( SAT)\, as a paradigmatic automated-reasoning problem\, has\nbeen considere d to be intractable. Over the past 20 years\, however\, there\nhas been a quiet\, but dramatic\, revolution\, and very large SAT instances\nare now being solved routinely as part of software and hardware design.\nIn this t alk I will review this amazing development and show how automated\nreasoni ng is now an industrial reality.\n\nI will then describe how we can levera ge SAT solving to accomplish\nother automated-reasoning tasks. Sampling u niformly at random satisfying\ntruth assignments of a given Boolean formul a or counting the number of such\nassignments are both fundamental computa tional problems in computer\nscience with applications in software testing \, software synthesis\, machine\nlearning\, personalized learning\, and mo re. While the theory of these\nproblems has been thoroughly investigated since the 1980s\, approximation\nalgorithms developed by theoreticians do not scale up to industrial-sized\ninstances. Algorithms used by the indus try offer better scalability\,\nbut give up certain correctness guarantees to achieve scalability. We\ndescribe a novel approach\, based on universa l hashing and Satisfiability\nModulo Theory\, that scales to formulas with hundreds of thousands of\nvariables without giving up correctness guarant ees.\n LOCATION:https://researchseminars.org/talk/OLS/5/ END:VEVENT END:VCALENDAR