Transmisión en vivo por youtube.com/dccuchile

Abstract: desde resolver Sudokus hasta demostrar teoremas matemáticos, pasando por verificar la correctitud de un programa, los SAT-solvers permiten resolver una amplia gama de problemas combinatoriales, y tienen aplicaciones en casi todas las áreas de la computación. Si bien los solvers modernos son altamente eficientes y sencillos de utilizar, utilizarlos para demostrar teoremas matemáticos que involucran millones de variables requiere de técnicas avanzadas de razonamiento automático. En esta charla presentaré una introducción al uso de SAT-solvers, pasando luego a explicar las técnicas utilizadas para resolver el problema del empaquetamiento cromático de la grilla infinita, un problema matemático abierto por 20 años que resolví junto a Marijn Heule.

Mini-bio: Bernardo cursa el 3er año del doctorado en computación en Carnegie Mellon University (CMU), donde trabaja en aplicar herramientas de razonamiento automática para resolver problemas matemáticos, bajo la supervisión de Marijn Heule. Antes de eso se graduó del Magíster en Ciencias mención Computación del DCC, supervisado por Pablo Barceló y Jorge Pérez. Su trabajo de magíster obtuvo el premio LA-CCI a la mejor tesis de maestría latinoamericana en temas relacionados a inteligencia artificial.  

--
Comunicaciones DCC