BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Rebecca Coulson (US Military Academy) DTSTART:20200507T180000Z DTEND:20200507T190000Z DTSTAMP:20260404T143402Z UID:OLS/3 DESCRIPTION:Title: The Bipartite Diameter 3 Metrically Homogeneous Graphs of Generic Type: Their Ages and Their Almost Sure Theories\nby Rebecca Coulson (US Mil itary Academy) as part of Online logic seminar\n\n\nAbstract\nFor the past 40 years computer scientists generally believed that\nNP-complete problem s are intractable. In particular\, Boolean\nsatisfiability (SAT)\, as a pa radigmatic automated-reasoning problem\, has\nbeen considered to be intrac table. Over the past 20 years\, however\, there\nhas been a quiet\, but dr amatic\, revolution\, and very large SAT instances\nare now being solved r outinely as part of software and hardware design.\nIn this talk I will rev iew this amazing development and show how automated\nreasoning is now an i ndustrial reality.\n\nI will then describe how we can leverage SAT solving to accomplish\nother automated-reasoning tasks. Sampling uniformly at ra ndom satisfying\ntruth assignments of a given Boolean formula or counting the number of such\nassignments are both fundamental computational problem s in computer\nscience with applications in software testing\, software sy nthesis\, machine\nlearning\, personalized learning\, and more. While the theory of these\nproblems has been thoroughly investigated since the 1980 s\, approximation\nalgorithms developed by theoreticians do not scale up t o industrial-sized\ninstances. Algorithms used by the industry offer bett er scalability\,\nbut give up certain correctness guarantees to achieve sc alability. We\ndescribe a novel approach\, based on universal hashing and Satisfiability\nModulo Theory\, that scales to formulas with hundreds of t housands of\nvariables without giving up correctness guarantees.\n LOCATION:https://stable.researchseminars.org/talk/OLS/3/ END:VEVENT END:VCALENDAR