OI Bruno. Há 2 meses vi um minicurso do Moshe nessas linhas, cobrindo essa mesma temática, e tive inclusive a oportunidade de almoçar com ele. Aproveite o evento e mande um abraço a ele.
[]s Marcelo On 7 May 2017 at 07:40, Bruno Lopes <blopesvie...@gmail.com> wrote: > Caros, > > No dia 15 de maio, segunda-feira, as 14:30h no auditório Padre Anchieta no > prédio Cardeal Leme da PUC-Rio teremos apalestra do Projeto. Moshe Vardi. > > Dentre os diversos prêmios que o Prof. Moshe Vardi obteve estão o ACM SIGACT > Goedel Prize, ACM SIGMOD Codd Award, IBM Outstanding Innovation Awards e > Blaise Pascal Medal. > Mais detalhes sobre sua contribuição para a área de Ciência de Computação > consulte http://www.cs.rice.edu/~vardi/. > > Atualmente o Prof. Vardi está na Univesridade de Rice e é editor da > Communications of the ACM. > > Sua pesquisa é bastante extensa com trabalhos ligando lógica e computação. > > Segue abaixo o título e resumo da palestra, que visa a uma audiência bem > ampla de pessoas ligadas a área de Ciência de Computação, Lógica e > Matemática. > > > Title and Abstract : > > The Automated-Reasoning Revolution: From Theory to Practice and Back > > Moshe Y. Vardi > Rice University > > 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 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. > > Abraços, > > Bruno. > > -- > Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos > Grupos do Google. > Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie > um e-mail para logica-l+unsubscr...@dimap.ufrn.br. > Para postar nesse grupo, envie um e-mail para logica-l@dimap.ufrn.br. > Acesse esse grupo em > https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. > Para ver essa discussão na Web, acesse > https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAFfvUVhvEsU-Y_iy1-C2dVsfrpzaq79gSiCTu%2BsuDR7hBuDbQg%40mail.gmail.com. -- Marcelo Finger Departament of Computer Science, IME University of Sao Paulo http://www.ime.usp.br/~mfinger -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CABqmzx1VBU1zGaDcSojZnofhbD3QjdUagsj64qKB6c2s2N2f3g%40mail.gmail.com.
