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:20260423T035615Z 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 Military A cademy) as part of Online logic seminar\n\n\nAbstract\nFor the past 40 yea rs computer scientists generally believed that\nNP-complete problems are i ntractable. In particular\, Boolean\nsatisfiability (SAT)\, as a paradigma tic automated-reasoning problem\, has\nbeen considered 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 routinel y as part of software and hardware design.\nIn this talk I will review thi s amazing development and show how automated\nreasoning is now an industri al reality.\n\nI will then describe how we can leverage SAT solving to acc omplish\nother automated-reasoning tasks. Sampling uniformly at random sa tisfying\ntruth assignments of a given Boolean formula or counting the num ber of such\nassignments are both fundamental computational problems in co mputer\nscience with applications in software testing\, software synthesis \, machine\nlearning\, personalized learning\, and more. While the theory of these\nproblems has been thoroughly investigated since the 1980s\, app roximation\nalgorithms developed by theoreticians do not scale up to indus trial-sized\ninstances. Algorithms used by the industry offer better scal ability\,\nbut give up certain correctness guarantees to achieve scalabili ty. We\ndescribe a novel approach\, based on universal hashing and Satisfi ability\nModulo Theory\, that scales to formulas with hundreds of thousand s of\nvariables without giving up correctness guarantees.\n LOCATION:https://researchseminars.org/talk/OLS/3/ END:VEVENT END:VCALENDAR